Module

ActualTameRootsAction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsAction

5 declarations indexed from sourceView source ↗

Module documentation

The original decomposition action on the SAME actual tame roots group

The action is the original quotient-residue action on every existing root coordinate. Its plain application and scalar law close the action's native permutation data before the original character is compared with it.

Imports2

Imported by6

def

actualTameRootsAction

L35 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction

Documentation

The canonical original decomposition action on the SAME actual roots 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

def actualTameRootsAction :
    (normalizationDecompositionGroup A K L Q).carrier →*
      Equiv.Perm (actualTameRootsGroup A K L Q).carrier

def

actualTameRootsAction_apply

L44 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction_apply

Documentation

Plain application of the SAME constructed decomposition action.

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

def actualTameRootsAction_apply
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (x : (actualTameRootsGroup A K L Q).carrier) :
    (actualTameRootsGroup A K L Q).carrier

theorem

actualTameRootsAction_projection

L51 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction_projection

Documentation

Every literal scalar coordinate carries the original quotient-residue action.

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 actualTameRootsAction_projection
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (x : (actualTameRootsGroup A K L Q).carrier)
    (n : Subtype (actualFiniteTameDegreeSet A K L Q)) :
    actualTameRootsScalar A K L Q n (actualTameRootsAction_apply A K L Q d x) =
      ((actualNormalizationQuotientAction A K L Q).toFun d).toFun
        (actualTameRootsScalar A K L Q n x)

theorem

actualTameRootsAction_one

L60 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction_one

Documentation

The original decomposition action fixes the existing identity element.

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 actualTameRootsAction_one
    (d : (normalizationDecompositionGroup A K L Q).carrier) :
    actualTameRootsAction_apply A K L Q d 1 = 1

theorem

actualTameRootsAction_mul

L67 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction_mul

Documentation

The original decomposition action preserves the existing multiplication.

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 actualTameRootsAction_mul
    (d : (normalizationDecompositionGroup A K L Q).carrier)
    (x y : (actualTameRootsGroup A K L Q).carrier) :
    actualTameRootsAction_apply A K L Q d (x * y) =
      actualTameRootsAction_apply A K L Q d x * actualTameRootsAction_apply A K L Q d y

Module documentation

The original decomposition action on the SAME actual tame roots group

Declarations

actualTameRootsAction

actualTameRootsAction_apply

actualTameRootsAction_projection

actualTameRootsAction_one

actualTameRootsAction_mul