Lean4
/-- The sum of an indexed collection of matroids, as a matroid on the sigma-type. -/
protected def sigma (M : (i : ι) → Matroid (α i)) : Matroid ((i : ι) × α i)
where
E := univ.sigma (fun i ↦ (M i).E)
Indep I := ∀ i, (M i).Indep (Sigma.mk i ⁻¹' I)
IsBase B := ∀ i, (M i).IsBase (Sigma.mk i ⁻¹' B)
indep_iff'
I := by
refine ⟨fun h ↦ ?_, fun ⟨B, hB, hIB⟩ i ↦ (hB i).indep.subset (preimage_mono hIB)⟩
choose Bs hBs using fun i ↦ (h i).exists_isBase_superset
refine ⟨univ.sigma Bs, fun i ↦ by simpa using (hBs i).1, ?_⟩
rw [← univ_sigma_preimage_mk I]
refine sigma_mono rfl.subset fun i ↦ (hBs i).2
exists_isBase := by
choose B hB using fun i ↦ (M i).exists_isBase
exact ⟨univ.sigma B, by simpa⟩
isBase_exchange B₁ B₂ h₁
h₂ := by
simp only [mem_diff, Sigma.exists, and_imp, Sigma.forall]
intro i e he₁ he₂
have hf_ex := (h₁ i).exchange (h₂ i) ⟨he₁, by simpa⟩
obtain ⟨f, ⟨hf₁, hf₂⟩, hfB⟩ := hf_ex
refine ⟨i, f, ⟨hf₁, hf₂⟩, fun j ↦ ?_⟩
rw [← union_singleton, preimage_union, preimage_diff]
obtain (rfl | hne) := eq_or_ne i j
·
simpa only [show ∀ x, {⟨i, x⟩} = Sigma.mk i '' { x } by simp, preimage_image_eq _ sigma_mk_injective,
union_singleton]
rw [preimage_singleton_eq_empty.2 (by simpa), preimage_singleton_eq_empty.2 (by simpa), diff_empty, union_empty]
exact h₁ j
maximality X _ I hI
hIX := by
choose Js hJs using fun i ↦ (hI i).subset_isBasis'_of_subset (preimage_mono (f := Sigma.mk i) hIX)
use univ.sigma Js
simp only [maximal_subset_iff', mem_univ, mk_preimage_sigma, and_imp]
refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
· rw [← univ_sigma_preimage_mk I]
exact sigma_mono rfl.subset fun i ↦ (hJs i).2
· rw [← univ_sigma_preimage_mk X]
exact sigma_mono rfl.subset fun i ↦ (hJs i).1.subset
rw [← univ_sigma_preimage_mk S]
refine sigma_mono rfl.subset fun i ↦ ?_
rw [sigma_subset_iff] at hJS
rw [(hJs i).1.eq_of_subset_indep (hS i) (hJS <| mem_univ i)]
exact preimage_mono hSX
subset_ground B
hB := by
rw [← univ_sigma_preimage_mk B]
apply sigma_mono Subset.rfl fun i ↦ (hB i).subset_ground
