English
If A ⟶ B is integral, then p.ResidueField ⊂ q.ResidueField is algebraic.
Русский
Если A ⟶ B интегрально, то p.ResidueField ⊂ q.ResidueField алгебраично.
LaTeX
$$$\text{[IsIntegral } A B\text{]} \Rightarrow \mathrm{Algebra.IsAlgebraic}(p.\mathrmResidueField, q.\mathrmResidueField)$$$
Lean4
instance [p.IsPrime] [q.IsPrime] [Algebra.IsIntegral A B] : Algebra.IsAlgebraic p.ResidueField q.ResidueField :=
by
have : Algebra.IsIntegral (A ⧸ p) (B ⧸ q) := .tower_top A
letI := ((algebraMap (B ⧸ q) q.ResidueField).comp (algebraMap (A ⧸ p) (B ⧸ q))).toAlgebra
haveI : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField := .of_algebraMap_eq' rfl
haveI : Algebra.IsAlgebraic (A ⧸ p) q.ResidueField := .trans _ (B ⧸ q) _
haveI : IsScalarTower (A ⧸ p) p.ResidueField q.ResidueField :=
by
refine .of_algebraMap_eq fun x ↦ ?_
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
simp [RingHom.algebraMap_toAlgebra]
refine .extendScalars (Ideal.injective_algebraMap_quotient_residueField p)
