lift_rank_comap — Mathlib

English

For a field homomorphism f, the lift of Module.rank(A.comap f over L) equals the lift of relrank(A, f.fieldRange).

Русский

Для отображения f подъём модуля ранга A.comap f над L равен подъёму relrank(A, f.fieldRange).

LaTeX

$$$ \operatorname{lift}(\operatorname{Module.rank}(A.comap f, L)) = \operatorname{lift}(\operatorname{relrank}(A, f.fieldRange))$$$

Lean4

theorem lift_rank_comap (f : L →+* E) : lift.{v} (Module.rank (A.comap f) L) = lift.{w} (relrank A f.fieldRange) := by
  simpa only [relrank_top_right, ← RingHom.fieldRange_eq_map] using lift_relrank_comap A f ⊤

Похожие утверждения