Filtered pointed étale neighbourhoods

Tensor products give common refinements of pointed étale algebras. The unramified diagonal and localization at an idempotent equalize parallel pointed maps.

References

• Stacks Project, Tag 04GW.
• Tau Ceti, TauCeti.RingTheory.Henselization.Filtered, for the tensor-product and idempotent-localization filteredness method.
• Taylor Dupuy, Thomas Tucker, and Zhuoran Wang, pcfawd-formalization at 9a20b3f, StrictHenselizationConstruction.lean, PointedEtaleNeighborhood.

instance TauCeti.StrictHenselization.neighbourhood_isFiltered (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.IsFiltered (Neighbourhood R Ω)

The pointed étale neighbourhood category is filtered.