English
Map a matroid M on α to a matroid on β with ground set E, via an equivalence e: M.E ≃ E. The resulting matroid is defined by transporting the independence structure along e.
Русский
Переносим матроид M с множества оснований M.E на множество E через эквивалентность e: M.E ≃ E; полученный матроид определяется переносом структуры независимости по e.
LaTeX
$$$\\text{Matroid}(M)\\mapsto \\text{Matroid with ground } E \\text{ via } e: M.E \\cong E$$$
Lean4
/-- Map `M : Matroid α` to a `Matroid β` with ground set `E` using an equivalence `M.E ≃ E`.
Defined using `Matroid.ofExistsMatroid` for better defeq. -/
def mapSetEquiv (M : Matroid α) {E : Set β} (e : M.E ≃ E) : Matroid β :=
Matroid.ofExistsMatroid E (fun I ↦ (M.Indep ↑(e.symm '' (E ↓∩ I)) ∧ I ⊆ E))
⟨M.mapSetEmbedding (e.toEmbedding.trans <| Function.Embedding.subtype _),
by
have hrw : ∀ I : Set β, Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I := fun I ↦ by ext; simp
simp [Equiv.toEmbedding, Embedding.subtype, Embedding.trans, hrw]⟩
