The closed fibre of a standard étale algebra #
Let P be a standard étale pair over a ring A and let J be an ideal of A. If the defining
equations of P hold modulo J at an element a of A, and the generator of P.Ring is
congruent to a modulo the extended ideal, then P.Ring has the same closed fibre as A: the
canonical map A ⧸ J → P.Ring ⧸ J P.Ring is bijective
(StandardEtalePair.algebraMap_quotient_bijective_of_hasMap).
References #
- Mathlib's
Mathlib.RingTheory.Etale.StandardEtale, forStandardEtalePairand its universal mapping API.
theorem
StandardEtalePair.algebraMap_quotient_bijective_of_hasMap
{A : Type u_1}
[CommRing A]
(P : StandardEtalePair A)
(J : Ideal A)
{a : A}
(ha : P.HasMap ((Ideal.Quotient.mk J) a))
(hX : P.X - (algebraMap A P.Ring) a ∈ Ideal.map (algebraMap A P.Ring) J)
:
Function.Bijective ⇑(algebraMap (A ⧸ J) (P.Ring ⧸ Ideal.map (algebraMap A P.Ring) J))
A standard étale algebra has the same closed fibre as its base along an ideal J, provided
its defining equations hold modulo J at an element a of the base and its generator is
congruent to a modulo the extended ideal.