English
A subset B is a base of the sigma matroid if and only if each component M_i has B_i as a base after taking appropriate preimages.
Русский
Подмножество B является основанием σ-матроида тогда и только тогда, когда каждый компонент M_i имеет соответствующий предобраз B_i как основание.
LaTeX
$$$ (\\mathrm{sigma}\n M).IsBasis B X \\iff \\forall i, (M_i).IsBasis (\\Sigma.mk i)^{-1} B (\\Sigma.mk i)^{-1} X $$$
Lean4
@[simp]
theorem sigma_isBasis_iff {I X} :
(Matroid.sigma M).IsBasis I X ↔ ∀ i, (M i).IsBasis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X) :=
by
simp only [IsBasis, sigma_indep_iff, maximal_subset_iff, and_imp, and_assoc, sigma_ground_eq, forall_and,
and_congr_right_iff]
refine fun hI ↦
⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩, fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩
· refine hII₀.antisymm ?_
specialize h (t := I ∪ Sigma.mk i '' I₀)
simp only [preimage_union, union_subset_iff, hIX, image_subset_iff, hI₀X, and_self, subset_union_left,
true_implies] at h
rw [h, preimage_union, sigma_mk_preimage_image_eq_self]
· exact subset_union_right
intro j
obtain (rfl | hij) := eq_or_ne i j
· rwa [sigma_mk_preimage_image_eq_self, union_eq_self_of_subset_left hII₀]
rw [sigma_mk_preimage_image' hij, union_empty]
apply hI
· exact fun i ↦ by simpa using preimage_mono (f := Sigma.mk i) h'
· exact fun ⟨i, x⟩ hx ↦ by simpa using hIX i hx
· refine fun J hJ hJX hIJ ↦ hIJ.antisymm fun ⟨i, x⟩ hx ↦ ?_
simpa using (h' i (hJ i) (preimage_mono hJX) (preimage_mono hIJ)).symm.subset hx
exact fun ⟨i, x⟩ hx ↦ by simpa using h'' i hx
