English
If p.ResidueField ⊂ q.ResidueField is separable, then the quotients HasQuotient (A/p) and (B/q) are separable as well.
Русский
Если расширение p.ResidueField ⊂ q.ResidueField разделимо, то и квартирами (A/p) и (B/q) разделимы.
LaTeX
$$$\text{If }\mathrm{Algebra.IsSeparable}(p.\mathrmResidueField, q.\mathrmResidueField) \text{ then } \mathrm{Algebra.IsSeparable}(\mathrmHasQuotient(A,p), \mathrmHasQuotient(B,q))$$$
Lean4
instance [p.IsMaximal] [q.IsMaximal] [Algebra.IsSeparable p.ResidueField q.ResidueField] :
Algebra.IsSeparable (A ⧸ p) (B ⧸ q) :=
by
refine
Algebra.IsSeparable.of_equiv_equiv (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
(.symm <| .ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
ext x
obtain ⟨x, rfl⟩ := (RingEquiv.ofBijective _ p.bijective_algebraMap_quotient_residueField).surjective x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
apply (RingEquiv.ofBijective _ q.bijective_algebraMap_quotient_residueField).injective
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, RingEquiv.symm_apply_apply,
RingEquiv.apply_symm_apply]
simp [RingHom.algebraMap_toAlgebra]
