Module

AbsoluteDivisorialCyclotomicConjugacy.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteDivisorialCyclotomicConjugacy

2 declarations indexed from sourceView source ↗

Module documentation

Absolute divisorial inertia sources

A prime in the normalization inside one separable closure defines one absolute inertia subgroup. This file maps elements of that single source into the etale fundamental group and compares all of their finite Galois cover images with contraction of the fixed normalization prime.

Imports3

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

theorem

fieldGeometricPoint_comp_genericExtensionMorphism

L32 ↗

EtaleFundamentalGroups.Inertia.fieldGeometricPoint_comp_genericExtensionMorphism

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
open CategoryTheory.PreGaloisCategory
open RamificationTheory.HilbertRamification
namespace EtaleFundamentalGroups.Inertia
universe uA u

Lean source · statement

theorem fieldGeometricPoint_comp_genericExtensionMorphism
    (U : Scheme.{u}) [IsIntegral U]
    (Omega : Type u) [Field Omega] [Algebra U.functionField Omega] :
    ξ U.functionField Omega ≫
        U.genericExtensionMorphism U.functionField =
      U.genericExtensionMorphism Omega

def

IsAbsoluteNormalizationPrimeInertiaSourceElement

L46 ↗

EtaleFundamentalGroups.Inertia.IsAbsoluteNormalizationPrimeInertiaSourceElement

Documentation

Membership in the image of one absolute normalization-prime inertia subgroup. The source element is mapped to the etale fundamental group by the actual generic-point morphism; no family of finite-level source elements is included in the definition.