English
For rings R, S, A with the stated structure, the lift of trdeg satisfies a + b = c, i.e., lift(trdeg R S) + lift(trdeg S A) = lift(trdeg R A).
Русский
Для колец R, S, A с указанной структурой, операция lift сохраняет аддитивность для числа трансцендентности: lift(trdeg R S) + lift(trdeg S A) = lift(trdeg R A).
LaTeX
$$$lift(\operatorname{trdeg} R S) + lift(\operatorname{trdeg} S A) = lift(\operatorname{trdeg} R A)$$
Lean4
@[stacks 030H]
theorem lift_trdeg_add_eq [Nontrivial R] [NoZeroDivisors A] [FaithfulSMul R S] [FaithfulSMul S A] :
lift.{w} (trdeg R S) + lift.{v} (trdeg S A) = lift.{v} (trdeg R A) :=
by
have ⟨s, hs⟩ := exists_isTranscendenceBasis R S
have ⟨t, ht⟩ := exists_isTranscendenceBasis S A
have := (FaithfulSMul.algebraMap_injective S A).noZeroDivisors _ (map_zero _) (map_mul _)
have := (FaithfulSMul.algebraMap_injective R S).nontrivial
rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm, ←
(hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]
