Module

ActualTameRootsCoefficientMap.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsCoefficientMap

3 declarations indexed from sourceView source ↗

Module documentation

Coefficient maps on the SAME native tame roots group

The coefficient map acts on the existing root coordinates. Its group laws are proved here before an original decomposition element is introduced.

Imports2

Imported by2

def

actualTameRootsCoefficientMap

L34 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsCoefficientMap

Documentation

Apply a coefficient homomorphism to the coordinates of the SAME actual 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

def actualTameRootsCoefficientMap
    (f : (normalizationCommAlgCat A L).carrier ⧸ Q →+*
      (normalizationCommAlgCat A L).carrier ⧸ Q) :
    (actualTameRootsGroup A K L Q).carrier → (actualTameRootsGroup A K L Q).carrier

theorem

actualTameRootsCoefficientMap_one

L42 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsCoefficientMap_one

Documentation

The actual coefficient map preserves 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 actualTameRootsCoefficientMap_one
    (f : (normalizationCommAlgCat A L).carrier ⧸ Q →+*
      (normalizationCommAlgCat A L).carrier ⧸ Q) :
    actualTameRootsCoefficientMap A K L Q f 1 = 1

theorem

actualTameRootsCoefficientMap_mul

L50 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsCoefficientMap_mul

Documentation

The actual coefficient map 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 actualTameRootsCoefficientMap_mul
    (f : (normalizationCommAlgCat A L).carrier ⧸ Q →+*
      (normalizationCommAlgCat A L).carrier ⧸ Q)
    (x y : (actualTameRootsGroup A K L Q).carrier) :
    actualTameRootsCoefficientMap A K L Q f (x * y) =
      actualTameRootsCoefficientMap A K L Q f x * actualTameRootsCoefficientMap A K L Q f y

Module documentation

Coefficient maps on the SAME native tame roots group

Declarations

actualTameRootsCoefficientMap

actualTameRootsCoefficientMap_one

actualTameRootsCoefficientMap_mul