Module

OriginalFiniteNormalizationInertiaConjugate.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteNormalizationInertiaConjugate

2 declarations indexed from sourceView source ↗

Module documentation

Conjugation of original finite-field inertia

Defines the original finite-field inertia conjugate and identifies its underlying element with the original field-automorphism expression.

Imports5

Imported by6

def

originalFiniteNormalizationInertiaConjugate

L32 ↗

EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaConjugate

Documentation

The original field-inertia conjugate, with its prescribed action closed inside the original normalization owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

def originalFiniteNormalizationInertiaConjugate
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F))
    (d : normalizationDecompositionGroup A K F Q)
    (σ : actualNormalizationInertiaGroup A K F Q) :
    actualNormalizationInertiaGroup A K F Q

theorem

originalFiniteNormalizationInertiaConjugate_element

L44 ↗

EtaleFundamentalGroups.Inertia.originalFiniteNormalizationInertiaConjugate_element