Essential smallness of pointed étale neighbourhoods

Retaining the point gives a fully faithful embedding into the category of finite-type algebras equipped with a map to the chosen commutative algebra.

References

• Stacks Project, Tag 04GW, for pointed étale neighbourhoods.
• Tau Ceti, TauCeti.RingTheory.Henselization.SmallModel, for finite-type-algebra essential smallness.
• Taylor Dupuy, Thomas Tucker, and Zhuoran Wang, pcfawd-formalization at 9a20b3f, StrictHenselizationConstruction.lean, PointedEtaleNeighborhood.

instance TauCeti.StrictHenselization.neighbourhood_essentiallySmall (R : Type u) (Ω : Type v) [CommRing R] [CommRing Ω] [Algebra R Ω] : CategoryTheory.EssentiallySmall.{max u v, max u v, max (v + 1) (u + 1)} (Neighbourhood R Ω)

Pointed étale neighbourhoods have a small model.