English
In a tower of algebras with faithful scalar actions, the transcendence degrees satisfy lift(trdeg R S) + lift(trdeg S A) ≤ lift(trdeg R A).
Русский
В башне алгебр с верно действующим тождеством скаляров выполняется неравенство: lift(trdeg_R S) + lift(trdeg S A) ≤ lift(trdeg R A).
LaTeX
$$$\\text{lift}(\\mathrm{trdeg}\,R S) + \\text{lift}(\\mathrm{trdeg}\,S A) \\le \\text{lift}(\\mathrm{trdeg}\\,R A)$$$
Lean4
theorem lift_trdeg_add_le [Nontrivial R] [FaithfulSMul R S] [FaithfulSMul S A] :
lift.{v} (trdeg R S) + lift.{u} (trdeg S A) ≤ lift.{u} (trdeg R A) :=
by
simp_rw [trdeg, lift_iSup (bddAbove_range _)]
simp_rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _), add_comm (lift.{v, u} _), ← mk_sum]
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
have := hs.sumElim_comp ht
refine le_ciSup_of_le (bddAbove_range _) ⟨_, this.to_subtype_range⟩ ?_
rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']
