The closed fibre of a henselization

The henselization of a pair has the same quotient by its extended ideal as the original ring. This identifies the closed fibre before proving that the colimit pair is henselian, by applying Ideal.quotientColimitEquiv to the small-model neighbourhood diagram.

References

• Stacks Project, Tag 0A02

theorem TauCeti.Henselization.quotient_bijective {R : Type u} [CommRing R] (I : Ideal R) : Function.Bijective ⇑(reducedMap I ↑(algebra I))

The canonical map from the quotient of a ring by an ideal to the quotient of its henselization by the extended ideal is bijective.

theorem TauCeti.Henselization.mem_extended_iff_exists_stage {R : Type u} [CommRing R] (I : Ideal R) (x : ↑(algebra I)) : x ∈ extended I ↔ ∃ (B : Neighbourhood I), ∃ b ∈ Ideal.map (algebraMap R ↑B.obj) I, (stage I B) b = x

An element belongs to the extended ideal of the henselization exactly when it comes from the extended ideal at some étale neighbourhood.

@[simp]

theorem TauCeti.Henselization.comap_extended {R : Type u} [CommRing R] (I : Ideal R) : Ideal.comap (algebraMap R ↑(algebra I)) (extended I) = I

An element of R maps into the extended ideal of the henselization exactly when it lies in I.

instance TauCeti.Henselization.isMaximal_extended {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] : (extended I).IsMaximal

The extension of a maximal ideal to the henselization is a maximal ideal: the quotient by it is the residue field R ⧸ I.