Skip to content

Commit

Permalink
feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#…
Browse files Browse the repository at this point in the history
…21145)

We define the fundamental circuit in a matroid for a set `I` and an element `e`, then use it to show that dependent sets all contain circuits, and a circuit-based extensionality lemma.
apnelson1 committed Jan 28, 2025
1 parent 7bf93b8 commit 6ac6869
Showing 1 changed file with 155 additions and 2 deletions.
157 changes: 155 additions & 2 deletions Mathlib/Data/Matroid/Circuit.lean
Original file line number Diff line number Diff line change
@@ -16,6 +16,24 @@ In matroids arising from graphs, circuits correspond to graphical cycles.
# Main Declarations
* `Matroid.Circuit M C` means that `C` is minimally dependent in `M`.
* For an `Indep`endent set `I` whose closure contains an element `e ∉ I`,
`Matroid.fundCircuit M e I` is the unique circuit contained in `insert e I`.
* `Matroid.Indep.fundCircuit_circuit` states that `Matroid.fundCircuit M e I` is indeed a circuit.
* `Circuit.eq_fundCircuit_of_subset` states that `Matroid.fundCircuit M e I` is the
unique circuit contained in `insert e I`.
* `Matroid.dep_iff_superset_circuit` states that the dependent subsets of the ground set
are precisely those that contain a circuit.
* `Matroid.ext_circuit` : a matroid is determined by its collection of circuits.
# Implementation Details
Since `Matroid.fundCircuit M e I` is only sensible if `I` is independent and `e ∈ M.closure I \ I`,
to avoid hypotheses being explicitly included in the definition,
junk values need to be chosen if either hypothesis fails.
The definition is chosen so that the junk values satisfy
`M.fundCircuit e I = {e}` for `e ∈ I` and
`M.fundCircuit e I = insert e I` if `e ∉ M.closure I`.
These make the useful statement `e ∈ M.fundCircuit e I ⊆ insert e I` true unconditionally.
-/

variable {α : Type*} {M : Matroid α} {C C' I X Y R : Set α} {e f x y : α}
@@ -87,6 +105,10 @@ lemma Circuit.not_ssubset (hC : M.Circuit C) (hC' : M.Circuit C') : ¬C' ⊂ C :
lemma Circuit.eq_of_subset_circuit (hC : M.Circuit C) (hC' : M.Circuit C') (h : C ⊆ C') : C = C' :=
hC'.eq_of_dep_subset hC.dep h

lemma Circuit.eq_of_superset_circuit (hC : M.Circuit C) (hC' : M.Circuit C') (h : C' ⊆ C) :
C = C' :=
(hC'.eq_of_subset_circuit hC h).symm

lemma circuit_iff_dep_forall_diff_singleton_indep :
M.Circuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}) := by
wlog hCE : C ⊆ M.E
@@ -155,8 +177,7 @@ lemma Circuit.mem_closure_diff_singleton_of_mem (hC : M.Circuit C) (heC : e ∈

/-! ### Restriction -/

lemma Circuit.circuit_restrict_of_subset (hC : M.Circuit C) (hCR : C ⊆ R) :
(M ↾ R).Circuit C := by
lemma Circuit.circuit_restrict_of_subset (hC : M.Circuit C) (hCR : C ⊆ R) : (M ↾ R).Circuit C := by
simp_rw [circuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
exact ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩

@@ -166,4 +187,136 @@ lemma restrict_circuit_iff (hR : R ⊆ M.E := by aesop_mat) :
simp_rw [circuit_iff, restrict_dep_iff, and_imp, dep_iff]
exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩

/-! ### Fundamental Circuits -/

/-- For an independent set `I` and some `e ∈ M.closure I \ I`,
`M.fundCircuit e I` is the unique circuit contained in `insert e I`.
For the fact that this is a circuit, see `Matroid.Indep.fundCircuit_circuit`,
and the fact that it is unique, see `Matroid.Circuit.eq_fundCircuit_of_subset`.
Has the junk value `{e}` if `e ∈ I` and `insert e I` if `e ∉ M.closure I`. -/
def fundCircuit (M : Matroid α) (e : α) (I : Set α) : Set α :=
insert e (I ∩ (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}))

lemma fundCircuit_eq_sInter (he : e ∈ M.closure I) :
M.fundCircuit e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) := by
rw [fundCircuit, inter_eq_self_of_subset_right]
exact sInter_subset_of_mem ⟨Subset.rfl, he⟩

lemma fundCircuit_subset_insert (M : Matroid α) (e : α) (I : Set α) :
M.fundCircuit e I ⊆ insert e I :=
insert_subset_insert inter_subset_left

lemma fundCircuit_subset_ground (he : e ∈ M.E) (hI : I ⊆ M.E := by aesop_mat) :
M.fundCircuit e I ⊆ M.E :=
(M.fundCircuit_subset_insert e I).trans (insert_subset he hI)

lemma mem_fundCircuit (M : Matroid α) (e : α) (I : Set α) : e ∈ fundCircuit M e I :=
mem_insert ..

/-- The fundamental circuit of `e` and `X` has the junk value `{e}` if `e ∈ X` -/
lemma fundCircuit_eq_of_mem (heX : e ∈ X) (heE : e ∈ M.E := by aesop_mat) :
M.fundCircuit e X = {e} := by
suffices h : ∀ a ∈ X, (∀ I ⊆ X, e ∈ M.closure I → a ∈ I) → a = e by
simpa [subset_antisymm_iff, fundCircuit]
exact fun f hfX h ↦ h {e} (by simpa) (mem_closure_of_mem' _ rfl)

/-- A version of `Matroid.fundCircuit_eq_of_mem` that applies when `X ⊆ M.E` instead of `e ∈ X`.-/
lemma fundCircuit_eq_of_mem' (heX : e ∈ X) (hX : X ⊆ M.E := by aesop_mat) :
M.fundCircuit e X = {e} := by
rwa [fundCircuit_eq_of_mem]

lemma Indep.fundCircuit_circuit (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
M.Circuit (M.fundCircuit e I) := by
apply (hI.inter_right _).insert_circuit_of_forall (by simp [heI])
· rw [(hI.subset _).closure_inter_eq_inter_closure, mem_inter_iff, and_iff_right hecl,
hI.closure_sInter_eq_biInter_closure_of_forall_subset _ (by simp +contextual)]
· simp
· exact ⟨I, rfl.subset, hecl⟩
exact union_subset rfl.subset (sInter_subset_of_mem ⟨rfl.subset, hecl⟩)
simp only [mem_inter_iff, mem_sInter, mem_setOf_eq, and_imp]
exact fun f hfI hf hecl ↦ (hf _ (diff_subset.trans inter_subset_left) hecl).2 rfl

lemma Indep.mem_fundCircuit_iff (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x}) := by
obtain rfl | hne := eq_or_ne x e
· simp [hI.diff, mem_fundCircuit]
suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
simpa [fundCircuit_eq_sInter hecl, hne, ← insert_diff_singleton_comm hne.symm,
(hI.diff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]
refine ⟨fun h hecl ↦ (h _ diff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
exact M.closure_subset_closure (subset_diff_singleton hJ hxJ) heJ

lemma Base.fundCircuit_circuit {B : Set α} (hB : M.Base B) (hxE : x ∈ M.E) (hxB : x ∉ B) :
M.Circuit (M.fundCircuit x B) :=
hB.indep.fundCircuit_circuit (by rwa [hB.closure_eq]) hxB

/-- For `I` independent, `M.fundCircuit e I` is the only circuit contained in `insert e I`. -/
lemma Circuit.eq_fundCircuit_of_subset (hC : M.Circuit C) (hI : M.Indep I) (hCss : C ⊆ insert e I) :
C = M.fundCircuit e I := by
obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCss
· exact (hC.not_indep (hI.subset hCI)).elim
suffices hss : M.fundCircuit e I ⊆ C by
refine hC.eq_of_superset_circuit (hI.fundCircuit_circuit ?_ fun heI ↦ ?_) hss
· rw [hI.mem_closure_iff]
exact .inl (hC.dep.superset hCss (insert_subset (hC.subset_ground heC) hI.subset_ground))
exact hC.not_indep (hI.subset (hCss.trans (by simp [heI])))
refine insert_subset heC (inter_subset_right.trans ?_)
refine (sInter_subset_of_mem (t := C \ {e}) ?_).trans diff_subset
simp [hCss, hC.mem_closure_diff_singleton_of_mem heC]

/-! ### Dependence -/

lemma Dep.exists_circuit_subset (hX : M.Dep X) : ∃ C, C ⊆ X ∧ M.Circuit C := by
obtain ⟨I, hI⟩ := M.exists_basis X
obtain ⟨e, heX, heI⟩ := exists_of_ssubset
(hI.subset.ssubset_of_ne (by rintro rfl; exact hI.indep.not_dep hX))
exact ⟨M.fundCircuit e I, (M.fundCircuit_subset_insert e I).trans (insert_subset heX hI.subset),
hI.indep.fundCircuit_circuit (hI.subset_closure heX) heI⟩

lemma dep_iff_superset_circuit (hX : X ⊆ M.E := by aesop_mat) :
M.Dep X ↔ ∃ C, C ⊆ X ∧ M.Circuit C :=
⟨Dep.exists_circuit_subset, fun ⟨C, hCX, hC⟩ ↦ hC.dep.superset hCX⟩

/-- A version of `Matroid.dep_iff_superset_circuit` that has the supportedness hypothesis
as part of the equivalence, rather than a hypothesis. -/
lemma dep_iff_superset_circuit' : M.Dep X ↔ (∃ C, C ⊆ X ∧ M.Circuit C) ∧ X ⊆ M.E :=
fun h ↦ ⟨h.exists_circuit_subset, h.subset_ground⟩, fun ⟨⟨C, hCX, hC⟩, h⟩ ↦ hC.dep.superset hCX⟩

/-- A version of `Matroid.indep_iff_forall_subset_not_circuit` that has the supportedness hypothesis
as part of the equivalence, rather than a hypothesis. -/
lemma indep_iff_forall_subset_not_circuit' :
M.Indep I ↔ (∀ C, C ⊆ I → ¬M.Circuit C) ∧ I ⊆ M.E := by
simp_rw [indep_iff_not_dep, dep_iff_superset_circuit']
aesop

lemma indep_iff_forall_subset_not_circuit (hI : I ⊆ M.E := by aesop_mat) :
M.Indep I ↔ ∀ C, C ⊆ I → ¬M.Circuit C := by
rw [indep_iff_forall_subset_not_circuit', and_iff_left hI]

/-! ### Extensionality -/

lemma ext_circuit {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
(h : ∀ ⦃C⦄, C ⊆ M₁.E → (M₁.Circuit C ↔ M₂.Circuit C)) : M₁ = M₂ := by
have h' {C} : M₁.Circuit C ↔ M₂.Circuit C :=
(em (C ⊆ M₁.E)).elim (h (C := C)) (fun hC ↦ iff_of_false (mt Circuit.subset_ground hC)
(mt Circuit.subset_ground fun hss ↦ hC (hss.trans_eq hE.symm)))
refine ext_indep hE fun I hI ↦ ?_
simp_rw [indep_iff_forall_subset_not_circuit hI, h',
indep_iff_forall_subset_not_circuit (hI.trans_eq hE)]

/-- A stronger version of `Matroid.ext_circuit`:
two matroids on the same ground set are equal if no circuit of one is independent in the other. -/
lemma ext_circuit_not_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
(h₁ : ∀ C, M₁.Circuit C → ¬ M₂.Indep C) (h₂ : ∀ C, M₂.Circuit C → ¬ M₁.Indep C) :
M₁ = M₂ := by
refine ext_circuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩
· obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_circuit_subset
rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_circuit_subset
rwa [← hC.eq_of_not_indep_subset (h₁ C' hC') hC'C]

lemma ext_iff_circuit {M₁ M₂ : Matroid α} :
M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ C, M₁.Circuit C ↔ M₂.Circuit C :=
fun h ↦ by simp [h], fun h ↦ ext_circuit h.1 fun C hC ↦ h.2 (C := C)⟩

end Matroid

0 comments on commit 6ac6869

Please sign in to comment.