English
Define mapSetEmbedding to transport a matroid M along an embedding f : M.E ↪ β to a matroid on β, with ground range(f) and independent sets characterized by existence of an I0 with M.Indep(I0) and I = f''I0.
Русский
Определим mapSetEmbedding для переноса матроида M вдоль вложения f: M.E ↪ β на матроид на β; множество оснований равно range(f), независимости задаются существованием I0 с M.Indep(I0) и I = f''I0.
LaTeX
$$$ (M.mapSetEmbedding f).E = \mathrm{range}(f) \quad\text{and}\quad (M.mapSetEmbedding f).Indep(I) \iff \exists I_0, M.Indep(I_0) \land I = f'' I_0 $$$
Lean4
/-- Map a matroid `M` to an isomorphic copy in `β` using an embedding `M.E ↪ β`. -/
def mapSetEmbedding (M : Matroid α) (f : M.E ↪ β) : Matroid β :=
Matroid.ofExistsMatroid (E := range f) (Indep := fun I ↦ M.Indep ↑(f ⁻¹' I) ∧ I ⊆ range f) (hM := by
classical
obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
· refine ⟨emptyOn β, ?_⟩
simp only [emptyOn_ground] at f
simp [range_eq_empty f, subset_empty_iff]
have _ : Nonempty M.E := ⟨⟨e, he⟩⟩
have _ : Nonempty α := ⟨e⟩
refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]
rintro _ ⟨I, rfl⟩
rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _), preimage_image_eq _ f.injective,
and_iff_left_iff_imp]
rintro - x hx y hy
simp only [Subtype.val_inj]
exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx) (image_mono (subset_univ I) hy))
