Module

ActualNormalizationWildCharZero.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildCharZero

2 declarations indexed from sourceView source ↗

Module documentation

Original wild inertia is trivial in residue characteristic zero

The finite principal-unit groups vanish by their actual arithmetic theorem. The proved faithfulness of all actual restrictions then detects the identity in the original inertia group.

Imports7

Imported by3

theorem

actualWild_restriction_eq_one_charZero

L31 ↗

EtaleFundamentalGroups.Inertia.actualWild_restriction_eq_one_charZero

Documentation

The actual finite wild condition becomes the identity before the original subgroup-to-bottom interface is opened.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · statement

theorem actualWild_restriction_eq_one_charZero
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
    [CharZero (IsLocalRing.ResidueField A)]
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier)
    (hσ : σ ∈ actualNormalizationWildSubgroup A K L Q) :
    (actualFiniteInertiaRestriction A K L Q E).hom'.toFun σ = 1

theorem

actualNormalizationWildSubgroup_eq_bot_of_baseResidue_charZero

L49 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationWildSubgroup_eq_bot_of_baseResidue_charZero