ModuleHenselianPair.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.HenselianPair
2 declarations indexed from sourceView source ↗ Module documentation
Finite étale covers of a Henselian pair
The affine equivalence identifies pullback of finite étale covers with tensor-product base change of finite étale algebras. The algebraic Henselian equivalence therefore gives Stacks Project, Tag 09ZS. The public statement uses the canonical intersection of the finite and étale morphism properties.
Declarations
AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeHenselian
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_henselian
DocumentationPullback from Spec R to Spec (R / I) is an equivalence on finite étale covers whenever (R, I) is a Henselian pair.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeHenselian :
MorphismProperty.IsStableUnderBaseChange
((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
MorphismProperty.IsStableUnderBaseChange.inf