English
For a matroid M on β and a map f: α → β, the closure in the pulled-back matroid (M.comap f) of X equals the preimage under f of the closure of the image of X in M.
Русский
Для матроида M на β и отображения f: α → β замыкание в тянутом назад матроидe (M.comap f) множества X равно прообразу подстановки f от замыкания образа X в M.
LaTeX
$$$ (M.\\mathrm{comap} f).closure X = f^{-1} \\; M.closure (f '' X) $$$
Lean4
@[simp]
theorem comap_closure_eq {β : Type*} (M : Matroid β) (f : α → β) (X : Set α) :
(M.comap f).closure X = f ⁻¹' M.closure (f '' X) := by
-- Use a choice of basis and extensionality to change the goal to a statement about independence.
obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
obtain ⟨hI', hIinj, -⟩ := comap_isBasis'_iff.1 hI
simp_rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, Set.ext_iff, hI.indep.mem_closure_iff', comap_ground_eq,
mem_preimage, hI'.indep.mem_closure_iff', comap_indep_iff, and_imp, mem_image, and_congr_right_iff, ←
image_insert_eq]
-- the lemma now easily follows by considering elements/non-elements of `I` separately.
intro x hxE
by_cases hxI : x ∈ I
· simp [hxI, show ∃ y ∈ I, f y = f x from ⟨x, hxI, rfl⟩]
simp [hxI, injOn_insert hxI, hIinj]
