English
If M has invariant cardinal rank and f is injective on M.E, then M.map f hf has invariant cardinal rank.
Русский
Если у M инвариантная кардинальная ранга и f инъективен на M.E, то M.map f hf сохраняет инвариантную кардинальную ранг.
LaTeX
$$InvariantCardinalRank (M.map f hf)$$
Lean4
instance invariantCardinalRank_map (M : Matroid α) [InvariantCardinalRank M] (hf : InjOn f M.E) :
InvariantCardinalRank (M.map f hf) := by
refine ⟨fun I J X hI hJ ↦ ?_⟩
obtain ⟨I, X, hIX, rfl, rfl⟩ := map_isBasis_iff'.1 hI
obtain ⟨J, X', hJX, rfl, h'⟩ := map_isBasis_iff'.1 hJ
obtain rfl : X = X' := by rwa [InjOn.image_eq_image_iff hf hIX.subset_ground hJX.subset_ground] at h'
have hcard := hIX.cardinalMk_diff_comm hJX
rwa [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hf.mono ((hIX.indep.diff _).subset_ground)), ←
mk_image_eq_of_injOn_lift _ _ (hf.mono ((hJX.indep.diff _).subset_ground)), lift_inj,
(hf.mono hIX.indep.subset_ground).image_diff, (hf.mono hJX.indep.subset_ground).image_diff, inter_comm,
hf.image_inter hJX.indep.subset_ground hIX.indep.subset_ground, diff_inter_self_eq_diff, diff_self_inter] at hcard
