Filteredness of étale neighbourhoods

The étale neighbourhoods of a ring–ideal pair form a filtered category. In addition to tensor products providing common targets, parallel maps are equalized after localizing the target at the complement of the idempotent that cuts out their equalizer. This filtered category indexes the construction of the henselization of a pair.

References

• Stacks Project, Tag 0A02

theorem TauCeti.Henselization.parallel_equalization {R : Type u} [CommRing R] (I : Ideal R) {B C : Neighbourhood I} (f g : B ⟶ C) : ∃ (D : Neighbourhood I) (h : C ⟶ D), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

Two parallel maps of étale neighbourhoods become equal after a further étale neighbourhood.

instance TauCeti.Henselization.neighbourhood_isFiltered {R : Type u} [CommRing R] (I : Ideal R) : CategoryTheory.IsFiltered (Neighbourhood I)

The category of étale neighbourhoods of a ring–ideal pair is filtered.