English
Let M be a matroid on α and f: α → β be a function that is injective on the ground set of M. Then a subset B of β is a base of the mapped matroid M.map f if and only if there exists a base B0 of M such that B is exactly the image of B0 under f; i.e., B = f''B0.
Русский
Пусть M — матроид на множестве α и f: α → β — отображение, строго инъективное относительно множества оснований M. Тогда множество B ⊆ β является базисом матроида M.map f тогда и только тогда, когда существует базис B0 матроида M такой, что B совпадает с образом B0 под действием f; то есть B = f(B0).
LaTeX
$$$(M\map f\; hf).IsBase\; B \;\iff\; \exists B_0,\; M.IsBase\; B_0 \land B = f''B_0$$$
Lean4
@[simp]
theorem map_isBase_iff (M : Matroid α) (f : α → β) (hf) {B : Set β} :
(M.map f hf).IsBase B ↔ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀ :=
by
rw [isBase_iff_maximal_indep]
refine ⟨fun h ↦ ?_, ?_⟩
· obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map
refine ⟨B₀, hB₀.isBase_of_maximal fun J hJ hB₀J ↦ ?_, hbij.image_eq.symm⟩
rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]
exact h.eq_of_subset (hJ.map f hf) (hbij.image_eq ▸ image_mono hB₀J)
rintro ⟨B, hB, rfl⟩
rw [maximal_subset_iff]
refine ⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩
obtain ⟨I₀, hI₀, hbij⟩ := hI.exists_bijOn_of_map
rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at hBI
rw [hB.eq_of_subset_indep hI₀ hBI, hbij.image_eq]
