ModulePointedEtaleNeighborhoods.lean
Nyll.EtaleFundamentalGroups.StrictHenselian.PointedEtaleNeighborhoods
2 declarations indexed from sourceView source ↗ Module documentation
Pointed étale neighborhoods over an arbitrary field
The functor of lifts of Spec Ω ⟶ S has an initially small, cofiltered category of elements for any field Ω. It defines a point of the bottom topology, so the existing Point.presheafFiber colimit API applies. No assertion that an arbitrary field lifts étale covers is made. When Ω is separably closed, its fiber functor is literally that of Scheme.pointSmallEtale.
Imports4
- Mathlib.AlgebraicGeometry.Sites.EtalePoint
- Mathlib.AlgebraicGeometry.Sites.AffineEtale
- Mathlib.CategoryTheory.Functor.TypeValuedFlat
- Mathlib.CategoryTheory.Sites.Point.Basic
Imported by2
Declarations
AlgebraicGeometry.Scheme.pointedEtaleNeighborhoods_initiallySmall
DocumentationAffine pointed neighborhoods form a weakly initial essentially small family. The proof uses only that Spec Ω has one point.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
(s : Spec (.of Ω) ⟶ S)
AlgebraicGeometry.Scheme.pointEtaleNeighborhoods
DocumentationThe arbitrary-field pointed-neighborhood functor, packaged as a point of the bottom topology to reuse the existing filtered-colimit implementation.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
(s : Spec (.of Ω) ⟶ S)