ModuleCompactificationAbelianization.lean
Nyll.AnabelianGeometry.WeightFiltration.CompactificationAbelianization
4 declarations indexed from sourceView source ↗ Module documentation
The actual compactification map on abelianized fundamental groups
Restriction of finite étale covers defines the map. For a normal locally Noetherian integral compactification, this map is surjective; its kernel is the image of the kernel before abelianization. Identifying this kernel with the boundary Tate module is a further geometric calculation.
Declarations
AnabelianGeometry.WeightFiltration.compactificationAbelianizationMap
DocumentationThe map induced by the actual open immersion and actual fiber functor.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open ProCGroups.Abelian
namespace AnabelianGeometry.WeightFiltration
variable {X U : Scheme} [IsIntegral X] [IsIntegral U]
(j : U ⟶ X) [IsOpenImmersion j]
{Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U)
AnabelianGeometry.WeightFiltration.compactificationAbelianizationMap_mk
DocumentationThe map on abelianizations retains the original fundamental-group map.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open ProCGroups.Abelian
namespace AnabelianGeometry.WeightFiltration
variable {X U : Scheme} [IsIntegral X] [IsIntegral U]
(j : U ⟶ X) [IsOpenImmersion j]
{Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U)
omit [IsIntegral X] [IsIntegral U] [IsOpenImmersion j] [IsSepClosed Ω] in
AnabelianGeometry.WeightFiltration.compactificationAbelianizationMap_surjective
DocumentationEvery abelianized proper-curve class lifts to the open curve.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open ProCGroups.Abelian
namespace AnabelianGeometry.WeightFiltration
variable {X U : Scheme} [IsIntegral X] [IsIntegral U]
(j : U ⟶ X) [IsOpenImmersion j]
{Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U)
variable [IsNormalIntegral X] [IsLocallyNoetherian X]
AnabelianGeometry.WeightFiltration.compactificationAbelianizationMap_ker
DocumentationThe boundary kernel after abelianization is exactly the image of the actual compactification kernel, rather than an additional chosen subgroup.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open ProCGroups.Abelian
namespace AnabelianGeometry.WeightFiltration
variable {X U : Scheme} [IsIntegral X] [IsIntegral U]
(j : U ⟶ X) [IsOpenImmersion j]
{Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U)
variable [IsNormalIntegral X] [IsLocallyNoetherian X]