circuit-axioms.txt

Prop. CC <= 2^E とする。CC が indep sys (E, F) (F := { X <= E : C <= X なる C in CC が存在しない }) の circuit の集合であることと、(C1)かつ(C2)は同値
(C1): {} not in CC
(C2): C1, C2 in CC, C1 <= C2 => C1 = C2

(証明): (=>): (C1) は {} in F から明らか。
(C2): C1 <= C2 を仮定する。
Circuit は、どの要素を取り除いても indep set になるような dep set だったので、
仮に C1 != C2 だったとすると x in C2 - C1 を任意にとって C2 - {x} (>= C1) が indep set にならず矛盾。
よって C1 = C2 である。

(<=): (M1): (C1) より {} in F なので ok.
(M2): 明らかに lower set である。
(CC が circuit の集合であること): 任意に C in CC をとる。
C が dep set であることは、C <= C より C not in F なので明らか。
あとは任意の x in C に対し、 C - {x} が indep set であることを言えばよい。
仮に C2 <= C - {x} なる C2 in CC が存在したとすると (C2) と矛盾する。よって C - {x} in F である。
また、任意に (E, F) の circuit C をとる。C in CC を示す。
C2 <= C となる C2 in CC が取れる。
任意の x in C に対し、 (C2 <= C - {x} なる C2 in CC は存在しない) が言える。
以上より、C = C2 と結論するよりない。よって C in CC である。

Prop. CC を indep sys (E, F) の circuit の集合とする。以下の4個は同値:
(a): (E, F) は matroid
(b): 任意の X in F と e in E に対し、X \/ {e} が含む circuit は高々1個
(C3): C1, C2 in CC, C1 != C2, e in C1 /\ C2 を仮定する。ある C3 in CC が存在して C3 <= (C1 \/ C2) - {e}
(C3’): C1, C2 in CC, e in C1 /\ C2, f in C1 - C2 を仮定する。ある C3 in CC が存在して f in C3 <= (C1 \/ C2) - {e}

(証明)
(b) => (C3): (C1 \/ C2) - {e} not in F を示せばよい。(C1 \/ C2) - {e} in F を仮定する。(b) より C1 \/ C2 に含まれる circuit は高々 1 個。しかし、C1 \/ C2 は C1 と C2 という異なる 2 個の circuit を含むため、矛盾。
(C3) => (b): X \/ {e} が相異なる 2 個の circuit C1, C2 を含んだと仮定する。(C3) より C3 <= (C1 \/ C2) - {e} <= X なる circuit C3 が存在するが、これは X in F と矛盾する。)
(C3') => (C3): 自明。
(b) => (a): ランク商 = 1 であることを示す。
任意の基 J, K に対し、 |J| >= |K| であることを示せばよい。
K の元を J と交換していくことを考える。 J - K の元を1個追加するために、最大で K - J の元を 1 個取り除く必要がある。((b) より追加によってできるサーキットは最大 1 個で、J /\ K の元は除去しなくてもできるため)
これを繰り返すことで、|K - J| <= |J - K| が言える。よって、|J| >= |K| である。
よってすべての基の大きさが等しい (ランク商 = 1) ので、(E, F) はマトロイドである。