English
A complex lifting formula for comap: lift((M.comap f).cRk X) equals lift(M.cRk(f''X)).
Русский
Сложная формула подъёма для comap: lift((M.comap f).cRk X) = lift(M.cRk(f''X)).
LaTeX
$$$\\mathrm{lift}((M.\\mathrm{comap} f).\\mathrm{cRk} X) = \\mathrm{lift}(M.\\mathrm{cRk}(f''X))$$$
Lean4
@[simp]
theorem cRk_comap_lift (M : Matroid β) (f : α → β) (X : Set α) :
lift.{v, u} ((M.comap f).cRk X) = lift (M.cRk (f '' X)) :=
by
nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]
nth_rw 2 [lift_iSup (bddAbove_range _)]
simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, isBase_restrict_iff', comap_isBasis'_iff,
and_imp]
refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
· rw [← mk_image_eq_of_injOn_lift _ _ hfI, lift_le]
exact hI.cardinalMk_le_cRk
obtain ⟨I₀, hI₀X, rfl, hfI₀⟩ :=
show ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀
by
obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]
rw [mk_image_eq_of_injOn_lift _ _ hfI₀, lift_le]
exact IsBasis'.cardinalMk_le_cRk <| comap_isBasis'_iff.2 ⟨hIX, hfI₀, hI₀X⟩
