ModulePuncturedHypersurfaceGerms.lean
Nyll.EtaleFundamentalGroups.Purity.PuncturedHypersurfaceGerms
3 declarations indexed from sourceView source ↗ Module documentation
Faithfulness on germs along a punctured hypersurface
The category of germs is the concrete localization of finite etale models on open neighbourhoods at their cartesian transition arrows. Restriction is the actual base-change functor from this localization to the punctured hypersurface, using the constructed cone over the diagram of open neighbourhoods.
For a Noetherian local ring and an element of its maximal ideal, equality of restricted morphisms is detected on a smaller neighbourhood. The calculus of fractions therefore makes the restriction functor faithful. This is the final categorical assertion of Stacks Project, Lemma 58.22.1. The geometric faithful neighbourhood is constructed from the original ring hypotheses; no eventual-equality or faithfulness hypothesis remains in the final theorem.
Declarations
AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.projection_pullback_faithful
DocumentationFaithfulness over the actual hypersurface pullback is preserved by its constructed identification with the fixed punctured hypersurface.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)
AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.exists_stage_map_eq
DocumentationEquality of restrictions is detected on a genuine smaller neighbourhood. The new stage is the intersection with the constructed faithful open.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)
variable [IsNoetherianRing R] (hf : f ∈ IsLocalRing.maximalIdeal R)
include hf
AlgebraicGeometry.FiniteEtale.PuncturedHypersurface.restriction_faithful
DocumentationThe actual restriction from the cartesian model localization of all open neighbourhoods to the punctured hypersurface is faithful. This is the neighbourhood-colimit assertion of Stacks 58.22.1, with the original local Noetherian hypotheses and an element of the maximal ideal.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.FiniteEtale.PuncturedHypersurface
universe u
attribute [local instance] finiteEtaleOverCategoryCoherence
finiteEtaleHasPullbacksAlongCoherence finiteEtaleStableUnderBaseChangeAlongCoherence
variable (R : Type u) [CommRing R] [IsLocalRing R] (f : R)
variable [IsNoetherianRing R] (hf : f ∈ IsLocalRing.maximalIdeal R)
include hf