lift_trdeg_eq — Mathlib

English

If e: A ≃_R A' is an isomorphism of R-algebras, then the lifted transcendence degrees are equal.

Русский

Если e: A ≃_R A' является изоморфизмом над R, то поднятая трансцендентная степень совпадает: lift(trdeg R A) = lift(trdeg R A').

LaTeX

$$$\lift(\trdeg R A) = \lift(\trdeg R A').$$$

Lean4

theorem lift_trdeg_eq (e : A ≃ₐ[R] A') : lift.{v'} (trdeg R A) = lift.{v} (trdeg R A') :=
  (lift_trdeg_le_of_injective e.toAlgHom e.injective).antisymm (lift_trdeg_le_of_surjective e.toAlgHom e.surjective)

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