Module

ActualNormalizationResidueExactness.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationResidueExactness

2 declarations indexed from sourceView source ↗

Module documentation

Exactness at the original decomposition group

The actual inclusion is injective. Mapping into the original Galois group identifies its range with the original inertia subgroup; the already proved residue-kernel image then gives literal equality of subgroups of D.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.NormalizationResidueDVR
Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationInertiaDecomposition
Nyll.EtaleFundamentalGroups.Inertia.NativeIdealInertiaInclusion
Mathlib.Algebra.Group.Subgroup.Ker

Imported by4

theorem

actualNormalizationInertiaToDecomposition_injective

L35 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaToDecomposition_injective

Documentation

Original inertia includes injectively into original decomposition.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing 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)

Lean source · statement

theorem actualNormalizationInertiaToDecomposition_injective :
    Function.Injective (actualNormalizationInertiaToDecomposition A K L Q).toFun

theorem

actualNormalizationResidueMorphism_ker

L40 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationResidueMorphism_ker