ModuleOrdinaryHenselizationComparison.lean
Nyll.EtaleFundamentalGroups.StrictHenselian.OrdinaryHenselizationComparison
4 declarations indexed from sourceView source ↗ Module documentation
The actual ordinary-to-pointed-stalk comparison
The ordinary universal lift gives the map into the existing pointed étale stalk. Uniqueness proves the literal triangle with its existing Henselian target map. This also applies to the original strict stalk inside a normalization-prime localization.
Declarations
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToGeometricStalk
DocumentationThe actual ordinary universal lift into the existing pointed étale stalk.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
section Point
variable {A Ω : Type u} [CommRing A] [IsLocalRing A] [Field Ω]
(φ : A →+* Ω) [IsLocalHom φ]
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToGeometricStalk_isLocalHom
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
section Point
variable {A Ω : Type u} [CommRing A] [IsLocalRing A] [Field Ω]
(φ : A →+* Ω) [IsLocalHom φ]
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToGeometricStalk_comp_map
DocumentationThe comparison preserves the original map from the base ring.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
section Point
variable {A Ω : Type u} [CommRing A] [IsLocalRing A] [Field Ω]
(φ : A →+* Ω) [IsLocalHom φ]
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToGeometricStalk_comp_toHenselian
DocumentationThe ordinary-to-pointed comparison and the existing actual Henselian target map compose to the original ordinary universal lift.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {A S : Type u} [CommRing A] [IsLocalRing A]
[CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]