English
If x is a transcendence basis over R in S, then the composition algebraMap S A ∘ x is a transcendence basis over R in A.
Русский
Если x — базис трансцендентности над R в S, то композиция algebraMap S A ∘ x образует базис трансцендентности над R в A.
LaTeX
$$$ IsTranscendenceBasis R x \Rightarrow IsTranscendenceBasis R (\text{algebraMap } S A \circ x)$$$
Lean4
theorem algebraMap_comp [Nontrivial R] [NoZeroDivisors S] [Algebra.IsAlgebraic S A] [FaithfulSMul S A] {x : ι → S}
(hx : IsTranscendenceBasis R x) : IsTranscendenceBasis R (algebraMap S A ∘ x) :=
by
let f := IsScalarTower.toAlgHom R S A
refine hx.1.map (f := f) (FaithfulSMul.algebraMap_injective S A).injOn |>.isTranscendenceBasis_iff_isAlgebraic.mpr ?_
rw [Set.range_comp, ← AlgHom.map_adjoin]
set Rx := adjoin R (range x)
let e := Rx.equivMapOfInjective f (FaithfulSMul.algebraMap_injective S A)
letI := e.toRingHom.toAlgebra
haveI : IsScalarTower Rx (Rx.map f) A := .of_algebraMap_eq fun x ↦ rfl
have : Algebra.IsAlgebraic Rx S := hx.isAlgebraic
have : Algebra.IsAlgebraic Rx A := .trans _ S _
exact .extendScalars e.injective
