Module

ActualSeparableRootsAction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualSeparableRootsAction

4 declarations indexed from sourceView source ↗

Module documentation

The original decomposition action on the full separable roots target

This is the coefficient action of the SAME original absolute residue morphism. Its scalar square is obtained from the concrete residue square and the coordinate formula of the full roots action.

Imports3

Imported by5

def

actualSeparableRootsAction

L34 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsAction

Documentation

The original decomposition action factors through the original absolute residue map.

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
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def actualSeparableRootsAction :
    (normalizationDecompositionGroup A K Ω Q).carrier →*
      Equiv.Perm (normalizationSeparableRootsGroup A Ω Q).carrier

def

actualSeparableRootsAction_apply

L41 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsAction_apply

Documentation

Plain application retains the exact original residue action.

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
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

def actualSeparableRootsAction_apply
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    (normalizationSeparableRootsGroup A Ω Q).carrier

theorem

actualSeparableRootsAction_scalar

L48 ↗

EtaleFundamentalGroups.Inertia.actualSeparableRootsAction_scalar

Documentation

Every full scalar coordinate is acted on by the SAME literal quotient automorphism.

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
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualSeparableRootsAction_scalar
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (n : InvertibleExponent (IsLocalRing.ResidueField A))
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    normalizationSeparableRootsScalar A Ω Q n
      (actualSeparableRootsAction_apply A K Ω Q d x) =
      actualNormalizationQuotientActionScalar A K Ω Q d
        (normalizationSeparableRootsScalar A Ω Q n x)

theorem

actualTameRootsAction_scalar

L65 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsAction_scalar

Documentation

The current actual tame action has that same closed scalar computation.

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
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualTameRootsAction_scalar
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (n : Subtype (actualFiniteTameDegreeSet A K Ω Q))
    (x : (actualTameRootsGroup A K Ω Q).carrier) :
    actualTameRootsScalar A K Ω Q n (actualTameRootsAction_apply A K Ω Q d x) =
      actualNormalizationQuotientActionScalar A K Ω Q d
        (actualTameRootsScalar A K Ω Q n x)

Module documentation

The original decomposition action on the full separable roots target

Declarations

actualSeparableRootsAction

actualSeparableRootsAction_apply

actualSeparableRootsAction_scalar

actualTameRootsAction_scalar