instIsSeparableResidueFieldOfQuotientIdeal

English

Under maximal p and q with LieOver and separability of the quotient extensions, the residue field extension p.ResidueField ⊂ q.ResidueField is separable.

Русский

При максимальных p и q с условием lies-over и рассогласованности над частями, расширение p.ResidueField ⊂ q.ResidueField является разделимым.

LaTeX

$$$\text{If } p, q \text{ maximal and } q.\mathrm{LiesOver} p, \; \text{and } \mathsf{Algebra.IsSeparable}(A/ p, B/ q),\; \mathrm{Algebra.IsSeparable}(p.\mathrmResidueField, q.\mathrmResidueField)$$$

Lean4

instance [p.IsMaximal] [q.IsMaximal] [Algebra.IsSeparable (A ⧸ p) (B ⧸ q)] :
    Algebra.IsSeparable p.ResidueField q.ResidueField :=
  by
  refine
    Algebra.IsSeparable.of_equiv_equiv (.ofBijective _ p.bijective_algebraMap_quotient_residueField)
      (.ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
  ext x
  simp [RingHom.algebraMap_toAlgebra]

Похожие утверждения