English
Let B be a base of M. Then an element e belongs to the fundamental cocircuit of f with respect to B if and only if f belongs to the fundamental circuit of e with respect to B.
Русский
Пусть B — основание матроида M. Тогда e принадлежит фундаментальной кококартe f относительно B тогда и только тогда, когда f принадлежит фундаментальной цепи e относительно B.
LaTeX
$$$M.IsBase B \rightarrow (e \in M.fundCocircuit f B \leftrightarrow f \in M.fundCircuit e B)$$$
Lean4
/-- Fundamental circuits and cocircuits of a base `B` play dual roles;
`e` belongs to the fundamental cocircuit for `B` and `f` if and only if
`f` belongs to the fundamental circuit for `e` and `B`.
This statement isn't so reasonable unless `f ∈ B` and `e ∉ B`,
but holds due to junk values even without these assumptions. -/
theorem mem_fundCocircuit_iff_mem_fundCircuit {e f : α} (hB : M.IsBase B) :
e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B := by
-- By symmetry and duality, it suffices to show the implication in one direction.
suffices aux :
∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
⟨fun h ↦ aux hB h, fun h ↦
aux hB.compl_isBase_dual <| by simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩
clear! B M e f
intro M B hB e f he
obtain rfl | hne := eq_or_ne e f
· simp [mem_fundCircuit]
have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual
obtain hfE | hfE := em' <| f ∈ M.E
· rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
contradiction
obtain hfB | hfB := em' <| f ∈ B
· rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he
contradiction
obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he
rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]
have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ { e })) :=
(hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual
refine hB'.indep.subset ?_
simp only [dual_ground, diff_singleton_subset_iff]
rw [diff_diff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm, ←
union_singleton (s := M.E \ B), ← diff_diff, diff_diff_cancel_left hB.subset_ground]
simp [hfB]
