English
Given a function f that is injective on M.E, the copy of M in β has independent sets that are the images of those in M. If β is nonempty, then a matroid N on β is a map of M exactly when M and N are isomorphic.
Русский
При наличии отображения f, инъектного на M.E, копия M в β имеет независимые множества, являющиеся образами независимых множеств M. Если β не пуст, тогда матроид N на β является отображением M тогда и только тогда, когда M и N изоморфны.
LaTeX
$$$\mathrm{map}(M,f,hf) := \mathrm{Matroid\ ofExistsMatroid} \left(E := f''M.E,\ Indep := \lambda I, \exists I_0, M.Indep I_0 \land I = f''I_0\right)$$$
Lean4
/-- Given a function `f` that is injective on `M.E`, the copy of `M` in `β` whose independent sets
are the images of those in `M`. If `β` is a nonempty type, then `N : Matroid β` is a map of `M`
if and only if `M` and `N` are isomorphic. -/
def map (M : Matroid α) (f : α → β) (hf : InjOn f M.E) : Matroid β :=
Matroid.ofExistsMatroid (E := f '' M.E) (Indep := fun I ↦ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀) (hM :=
by
refine ⟨M.mapSetEmbedding ⟨_, hf.injective⟩, by simp, fun I ↦ ?_⟩
simp_rw [mapSetEmbedding_indep_iff', Embedding.coeFn_mk, restrict_apply, ← image_image f Subtype.val,
Subtype.exists_set_subtype (p := fun J ↦ M.Indep J ∧ I = f '' J)]
exact ⟨fun ⟨I₀, _, hI₀⟩ ↦ ⟨I₀, hI₀⟩, fun ⟨I₀, hI₀⟩ ↦ ⟨I₀, hI₀.1.subset_ground, hI₀⟩⟩)
