algebraQuotientOfRamificationIdxNeZero

English

If p is maximal and S is finite over R with P lying over p, then inertiaDeg(p,P) > 0; thus the inertia degree is nontrivial.

Русский

Если p максимален, S конечно над R и P лежит над p, то inertiaDeg(p,P) > 0.

LaTeX

$$$0 < \\operatorname{inertiaDeg} \\, p \\, P$$$

Lean4

/-- If `P` lies over `p`, then `R / p` has a canonical map to `S / P`.

This can't be an instance since the map `f : R → S` is generally not inferable.
-/
def algebraQuotientOfRamificationIdxNeZero [hfp : NeZero e] : Algebra (R ⧸ p) (S ⧸ P) :=
  Quotient.algebraQuotientOfLEComap (le_comap_of_ramificationIdx_ne_zero hfp.out)

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