Module

ActualNormalizationInertiaDecomposition.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationInertiaDecomposition

2 declarations indexed from sourceView source ↗

Module documentation

The actual original inertia inside decomposition

The two original action names use the identical normalization action value. The inclusion is the standard inclusion supplied by ideal inertia stability.

Imports3

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteNormalizationInertiaConjugate
Nyll.EtaleFundamentalGroups.Inertia.NativeIdealInertiaInclusion
Mathlib.Algebra.Group.Subgroup.Map

Imported by5

def

actualNormalizationInertiaToDecomposition

L33 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaToDecomposition

Documentation

The actual inertia includes into the SAME original decomposition group.

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

def actualNormalizationInertiaToDecomposition :
    (actualNormalizationInertiaGroup A K L Q).carrier →*
      (normalizationDecompositionGroup A K L Q).carrier

theorem

actualNormalizationInertiaToDecomposition_conjugate

L39 ↗

EtaleFundamentalGroups.Inertia.actualNormalizationInertiaToDecomposition_conjugate