Lean4
/-- The pullback of a matroid on `β` by a function `f : α → β` to a matroid on `α`.
Elements with the same (nonloop) image are parallel and the ground set is `f ⁻¹' M.E`.
The matroids `M.comap f` and `M ↾ range f` have isomorphic simplifications;
the preimage of each nonloop of `M ↾ range f` is a parallel class. -/
def comap (N : Matroid β) (f : α → β) : Matroid α :=
IndepMatroid.matroid <|
{ E := f ⁻¹' N.E
Indep := fun I ↦ N.Indep (f '' I) ∧ InjOn f I
indep_empty := by simp
indep_subset := fun _ _ h hIJ ↦ ⟨h.1.subset (image_mono hIJ), InjOn.mono hIJ h.2⟩
indep_aug := by
rintro I B ⟨hI, hIinj⟩ hImax hBmax
obtain ⟨I', hII', hI', hI'inj⟩ := (not_maximal_subset_iff ⟨hI, hIinj⟩).1 hImax
have h₁ : ¬(N ↾ range f).IsBase (f '' I) :=
by
refine fun hB ↦ hII'.ne ?_
have h_im := hB.eq_of_subset_indep (by simpa) (image_mono hII'.subset)
rwa [hI'inj.image_eq_image_iff hII'.subset Subset.rfl] at h_im
have h₂ : (N ↾ range f).IsBase (f '' B) :=
by
refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_
rintro _ ⟨⟨e, heB, rfl⟩, hfe⟩ hi
rw [restrict_indep_iff, ← image_insert_eq] at hi
have hinj : InjOn f (insert e B) :=
by
rw [injOn_insert (fun heB ↦ hfe (mem_image_of_mem f heB))]
exact ⟨hBmax.1.2, hfe⟩
refine hBmax.not_prop_of_ssuperset (t := insert e B) (ssubset_insert ?_) ⟨hi.1, hinj⟩
exact fun heB ↦ hfe <| mem_image_of_mem f heB
obtain ⟨_, ⟨⟨e, he, rfl⟩, he'⟩, hei⟩ := Indep.exists_insert_of_not_isBase (by simpa) h₁ h₂
have heI : e ∉ I := fun heI ↦ he' (mem_image_of_mem f heI)
rw [← image_insert_eq, restrict_indep_iff] at hei
exact ⟨e, ⟨he, heI⟩, hei.1, (injOn_insert heI).2 ⟨hIinj, he'⟩⟩
indep_maximal := by
rintro X - I ⟨hI, hIinj⟩ hIX
obtain ⟨J, hJ⟩ :=
(N ↾ range f).existsMaximalSubsetProperty_indep (f '' X) (by simp) (f '' I) (by simpa) (image_mono hIX)
simp only [restrict_indep_iff, image_subset_iff, maximal_subset_iff, and_imp, and_assoc] at hJ ⊢
obtain ⟨hIJ, hJ, hJf, hJX, hJmax⟩ := hJ
obtain ⟨J₀, hIJ₀, hJ₀X, hbj⟩ :=
hIinj.bijOn_image.exists_extend_of_subset hIX (image_mono hIJ) (image_subset_iff.2 <| preimage_mono hJX)
obtain rfl : f '' J₀ = J := by rw [← image_preimage_eq_of_subset hJf, hbj.image_eq]
refine ⟨J₀, hIJ₀, hJ, hbj.injOn, hJ₀X, fun K hK hKinj hKX hJ₀K ↦ ?_⟩
rw [← hKinj.image_eq_image_iff hJ₀K Subset.rfl,
hJmax hK (image_subset_range _ _) (image_mono hKX) (image_mono hJ₀K)]
subset_ground := fun _ hI e heI ↦ hI.1.subset_ground ⟨e, heI, rfl⟩ }
