English
If x is a transcendence basis over R in S and y is a transcendence basis over S in A, then the combination Sum.elim y (algebraMap S A ∘ x) is a transcendence basis over R in A.
Русский
Если x — база трансцендентности над R в S, а y — база над S в A, то сумма Sum.elim y (algebraMap S A ∘ x) образует базис трансцендентности над R в A.
LaTeX
$$$ IsTranscendenceBasis R x \to IsTranscendenceBasis S y \to IsTranscendenceBasis R (Sum.elim y (algebraMap S A \circ x))$$$
Lean4
theorem sumElim_comp [NoZeroDivisors A] {x : ι → S} {y : ι' → A} (hx : IsTranscendenceBasis R x)
(hy : IsTranscendenceBasis S y) : IsTranscendenceBasis R (Sum.elim y (algebraMap S A ∘ x)) :=
by
cases subsingleton_or_nontrivial R
· rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢; infer_instance
rw [(hx.1.sumElim_comp hy.1).isTranscendenceBasis_iff_isAlgebraic]
set Rx := adjoin R (range x)
let Rxy := adjoin Rx (range y)
rw [show adjoin R (range <| Sum.elim y (algebraMap S A ∘ x)) = Rxy.restrictScalars R by
rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]]
change Algebra.IsAlgebraic Rxy A
have := hx.1.algebraMap_injective.nontrivial
have := hy.1.algebraMap_injective.nontrivial
have := hy.isAlgebraic
set Sy := adjoin S (range y)
let _ : Algebra Rxy Sy :=
by
refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra
rintro _ ⟨i, rfl⟩; exact subset_adjoin (s := range y) ⟨i, rfl⟩
have : IsScalarTower Rxy Sy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
have : IsScalarTower Rx Rxy Sy := .of_algebraMap_eq fun ⟨a, _⟩ ↦ Subtype.ext rfl
have : Algebra.IsAlgebraic Rxy Sy :=
by
refine
⟨fun ⟨a, ha⟩ ↦
adjoin_induction ?_ (fun _ ↦ .extendScalars (R := Rx) ?_ ?_) (fun _ _ _ _ ↦ .add) (fun _ _ _ _ ↦ .mul) ha⟩
· rintro _ ⟨i, rfl⟩; exact isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)
· exact fun _ _ ↦ (Subtype.ext <| hy.1.algebraMap_injective <| Subtype.ext_iff.mp ·)
· exact (hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)
exact .trans _ Sy _
