rank-axioms.txt

r: 2^E -> Z>=0 について、以下の3つは同値。
1. F := { X | r(X) = |X| } としたときに、(E, F) はマトロイドで r は F のランク関数。
2.
  (R1) r(X) <= |X|
  (R2) X <= Y => r(X) <= r(Y)
  (R3) r(X \/ Y) + r(X /\ Y) <= r(X) + r(Y)
3.
  (R1’) r({}) = 0
  (R2’) r(X) <= r(X \/ {y}) <= r(X) + 1
  (R3’) r(X \/ {x}) = r(X \/ {y}) = r(X) => r(X \/ {x, y}) = r(X)

(証明)

1. -> 2.
(R1), (R2)は全てのind sysで成り立つ。
(R3): X = A \/ B, Y = A \/ C, B /\ C = {} となるように A, B, C をとる。
X /\ Y = A のある basis を D (D <= A), X = A \/ B のある basis を D \/ E (E <= B), D \/ E を拡張してできる X \/ Y = A \/ B \/ C の basis を D \/ E \/ G (G <= C) とする。 (このような E, G は必ず取れる、F はマトロイドであるため)
D \/ G は Y = A \/ C の indep set である。よって、
r(X) + r(Y) >= |D \/ E| + |D \/ G| (basis の大きさは全て等しい)
  = 2 |D| + |E| + |G|
  = |D| + |D \/ E \/ G|
  = r(X /\ Y) + r(X \/ Y)
が成り立つ。
2. -> 3.
(R1'), (R2') は (R1), (R2), (R3) で成り立つ。
(R3'): x = y のときは明らか。
x != y のときは (R3) で X := X \/ {x}, Y := X \/ {y} とすれば r(X \/ {x, y}) <= r(X) が、(R2) から r(X \/ {x, y}) >= r(X) が言える。

3. -> 1.
ind sys であることは (R1'), (R2') から言える。
F := { X | r(X) = |X| } としたときに (E, F) がマトロイドであることを示す。
r(X) = |X|, r(Y) = |Y|, |X| = |Y| + 1 を満たす X, Y に対して、ある x in X - Y が存在して r(Y \/ {x}) = |Y| + 1 であることを示せばよい。
仮に全ての x in X - Y に対して r(Y \/ {x}) = r(Y) であったと仮定する。
X - Y = {x_1, ..., x_k} とする。帰納法で、任意の i, j > i に対して、r(Y \/ {x_1, ..., x_i, x_j}) = r(Y) であることが言えるので、最終的に r(X \/ Y) = r(Y) が言える。これは　r(X \/ Y) >= r(X) と矛盾する。
また、r が F のランク関数であることを示す。r(X) = max { |Y| : Y <= X && r(Y) = |Y|} を示せばよい。
Y を X の最大の独立集合とする。Y の最大性から、任意の x in X - Y に対して r(Y \/ {x}) = r(Y) である。上の議論と同様に r(X) = r(Y) = |Y| が言える。

2. -> 1.
F := { X | r(X) = |X| } としたときに (E, F) がマトロイドであることを示す。
{} in F は自明。X <= Y かつ r(Y) = |Y| なら r(X) = |X| というのは、todo.
r(X) = |X|, r(Y) = |Y|, |X| = |Y| + 1 を満たす X, Y に対して、ある x in X - Y が存在して r(Y \/ {x}) = |Y| + 1 であることを示せばよい。
todo.

1. -> 3.
(R1') は自明。
(R2'): r(X) <= r(X \/ {y}) は明らか。
r(X \/ {y}) <= r(X) + 1 については、X のある basis を H, X \/ {y} のある basis を I とすると、仮に |I| >= |H| + 2 であった場合、増加公理より |I| の要素を 2 個以上 H に含めてより大きい indep set ができることになるが、必然的に y 以外の要素が含まれ X の部分集合の中でより大きい indep set が見つかってしまうことになり、矛盾。
(R3'): todo

3. -> 2.