NYLL
Module

ActualNormalizationRamificationData.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationRamificationData
22 declarations indexed from sourceView source ↗

Module documentation

The actual original DVR ramification diagram

Every stored object, map, action and topology is supplied by its existing original-input owner. The residue-only construction computes exactly the existing actual-degree roots system and group, as the computation theorems below record. No comparison or mathematical conclusion is a data field.

Imports12
Imported by3

Declarations

def

actualNormalizationRamificationResidues

L46 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues
Documentation

The literal residue fields and SAME actual finite tame-degree range.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · full declaration
def actualNormalizationRamificationResidues : NativeRamificationResidues.{u, w} where
  baseResidue := IsLocalRing.ResidueField A
  baseResidueField := inferInstanceAs (Field (IsLocalRing.ResidueField A))
  residue := (normalizationCommAlgCat A L).carrier ⧸ Q
  residueField := inferInstanceAs (Field ((normalizationCommAlgCat A L).carrier ⧸ Q))
  degrees := actualFiniteTameDegreeSet A K L Q
theorem

actualNormalizationRamificationResidues_baseResidue

L54 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_baseResidue
Documentation

The base coefficient field is literally the original DVR residue field.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_baseResidue :
    (actualNormalizationRamificationResidues A K L Q).baseResidue =
      IsLocalRing.ResidueField A
theorem

actualNormalizationRamificationResidues_residue

L59 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_residue
Documentation

The upstairs coefficient field is the literal normalization quotient.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_residue :
    (actualNormalizationRamificationResidues A K L Q).residue =
      ((normalizationCommAlgCat A L).carrier ⧸ Q)
theorem

actualNormalizationRamificationResidues_degrees

L64 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_degrees
Documentation

The stored degrees are the SAME actual range, without reindexing.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_degrees :
    (actualNormalizationRamificationResidues A K L Q).degrees =
      actualFiniteTameDegreeSet A K L Q
theorem

actualNormalizationRamificationResidues_rootsSystem

L69 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_rootsSystem
Documentation

Its intrinsic roots system is the SAME already constructed system.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_rootsSystem :
    (actualNormalizationRamificationResidues A K L Q).rootsSystem =
      actualFiniteTameRootsSystem A K L Q
theorem

actualNormalizationRamificationResidues_rootsGroup

L74 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_rootsGroup
Documentation

Its intrinsic roots group retains the SAME existing group structure.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_rootsGroup :
    (actualNormalizationRamificationResidues A K L Q).rootsGroup =
      actualTameRootsGroup A K L Q
def

actualNormalizationRamificationDiagram

L79 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram
Documentation

All group data and topologies are the SAME original constructions.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · full declaration
def actualNormalizationRamificationDiagram :
    NativeRamificationDiagram (actualNormalizationRamificationResidues A K L Q) where
  decomposition := normalizationDecompositionGroup A K L Q
  inertia := actualNormalizationInertiaGroup A K L Q
  residueAutomorphisms := normalizationResidueAutomorphisms A L Q
  tameQuotient := actualTameQuotientGroup A K L Q
  wild := actualNormalizationWildSubgroup A K L Q
  inertiaInclusion := GrpCat.ofHom (actualNormalizationInertiaToDecomposition A K L Q)
  residueMorphism := normalizationResidueMorphism A K L Q
  quotientProjection := actualTameQuotientProjection A K L Q
  character := actualTameCharacterMorphism A K L Q
  conjugate := originalFiniteNormalizationInertiaConjugate A K L Q
  rootsAction := actualTameRootsAction_apply A K L Q
  inertiaTopology := inferInstanceAs
    (TopologicalSpace (actualNormalizationInertiaGroup A K L Q).carrier)
  tameQuotientTopology := inferInstanceAs
    (TopologicalSpace (actualTameQuotientGroup A K L Q).carrier)
theorem

actualNormalizationRamificationDiagram_decomposition

L98 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_decomposition
Documentation

Decomposition is the SAME original normalization stabilizer.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_decomposition :
    (actualNormalizationRamificationDiagram A K L Q).decomposition =
      normalizationDecompositionGroup A K L Q
theorem

actualNormalizationRamificationDiagram_inertia

L103 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_inertia
Documentation

Inertia is the SAME original normalization inertia group.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_inertia :
    (actualNormalizationRamificationDiagram A K L Q).inertia =
      actualNormalizationInertiaGroup A K L Q
theorem

actualNormalizationRamificationDiagram_inertiaTopology

L108 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_inertiaTopology
Documentation

The stored inertia topology is the existing Krull-subgroup topology.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_inertiaTopology :
    (actualNormalizationRamificationDiagram A K L Q).inertiaTopology =
      actualNormalizationInertiaGroup_topologicalSpace A K L Q
theorem

actualNormalizationRamificationDiagram_tameQuotientTopology

L113 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_tameQuotientTopology
Documentation

The stored tame topology is the existing literal quotient topology.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_tameQuotientTopology :
    (actualNormalizationRamificationDiagram A K L Q).tameQuotientTopology =
      actualTameQuotientGroup_topologicalSpace A K L Q
theorem

actualNormalizationRamificationDiagram_wildTopology

L118 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_wildTopology
Documentation

The inherited wild topology is the SAME independent subgroup topology.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · full declaration
theorem actualNormalizationRamificationDiagram_wildTopology :
    TopologicalSpace.induced
        (fun σ : Subtype (actualNormalizationRamificationDiagram A K L Q).wild.carrier =>
          (show (actualNormalizationRamificationDiagram A K L Q).inertia.carrier from σ.val))
        (actualNormalizationRamificationDiagram A K L Q).inertiaTopology =
      actualNormalizationWildGroup_topologicalSpace A K L Q := rfl
theorem

actualNormalizationRamificationResidues_rootsTopology

L126 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationResidues_rootsTopology
Documentation

The intrinsic root target retains the SAME inverse-limit topology.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationResidues_rootsTopology :
    NativeRamificationResidues.rootsGroup_topologicalSpace
        (actualNormalizationRamificationResidues A K L Q) =
      actualTameRootsGroup_topologicalSpace A K L Q
theorem

actualNormalizationRamificationDiagram_residueAutomorphisms

L132 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_residueAutomorphisms
Documentation

The residue target is the actual automorphism group over the base residue field.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_residueAutomorphisms :
    (actualNormalizationRamificationDiagram A K L Q).residueAutomorphisms =
      normalizationResidueAutomorphismsOverResidueField A L Q
theorem

actualNormalizationRamificationDiagram_wild

L138 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_wild
Documentation

The stored wild subgroup is the SAME independent principal-unit limit.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_wild :
    (actualNormalizationRamificationDiagram A K L Q).wild =
      actualNormalizationWildSubgroup A K L Q
theorem

actualNormalizationRamificationDiagram_tameQuotient

L143 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_tameQuotient
Documentation

The stored tame quotient is literally the existing I/P.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_tameQuotient :
    (actualNormalizationRamificationDiagram A K L Q).tameQuotient =
      actualTameQuotientGroup A K L Q
theorem

actualNormalizationRamificationDiagram_character

L148 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_character
Documentation

The stored character is exactly the existing canonical tame character.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_character :
    (actualNormalizationRamificationDiagram A K L Q).character =
      actualTameCharacterMorphism A K L Q
theorem

actualNormalizationRamificationDiagram_quotientProjection

L153 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_quotientProjection
Documentation

The stored quotient map is the literal quotient projection.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_quotientProjection :
    (actualNormalizationRamificationDiagram A K L Q).quotientProjection =
      actualTameQuotientProjection A K L Q
theorem

actualNormalizationRamificationDiagram_inertiaInclusion

L158 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_inertiaInclusion
Documentation

The inclusion is the existing literal inclusion I into D.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_inertiaInclusion :
    (actualNormalizationRamificationDiagram A K L Q).inertiaInclusion.hom' =
      actualNormalizationInertiaToDecomposition A K L Q
theorem

actualNormalizationRamificationDiagram_residueMorphism

L163 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_residueMorphism
Documentation

The stored residue map is the existing original normalization residue map.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_residueMorphism :
    (actualNormalizationRamificationDiagram A K L Q).residueMorphism =
      normalizationResidueMorphism A K L Q
theorem

actualNormalizationRamificationDiagram_conjugate

L168 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_conjugate
Documentation

Stored conjugation is original decomposition conjugation.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_conjugate
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    (actualNormalizationRamificationDiagram A K L Q).conjugate d σ =
      originalFiniteNormalizationInertiaConjugate A K L Q d σ
theorem

actualNormalizationRamificationDiagram_rootsAction

L175 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationRamificationDiagram_rootsAction
Documentation

The root action is the SAME actual residue action on the SAME limit.

Source context 6 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] Ideal.Quotient.field
variable (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]
Lean source · statement
theorem actualNormalizationRamificationDiagram_rootsAction
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (x : (actualTameRootsGroup A K L Q).carrier) :
    (actualNormalizationRamificationDiagram A K L Q).rootsAction d x =
      actualTameRootsAction_apply A K L Q d x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.