NYLL
Module

ActualTameScalarRestrictionData.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameScalarRestrictionData
9 declarations indexed from sourceView source ↗

Module documentation

The literal actual scalar restriction diagram

Each data function is the underlying function of an existing actual map. The coefficient and conjugation comparisons are proved separately; none is a hypothesis or a field of the diagram.

Imports4
Imported by2

Declarations

structure

ScalarInertiaRestrictionData

L29 ↗
EtaleFundamentalGroups.Inertia.ScalarInertiaRestrictionData
Documentation

Restriction functions and coefficient inclusion only, with no asserted laws.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · full declaration
structure ScalarInertiaRestrictionData
    (source : ScalarInertiaActionData.{u}) (target : ScalarInertiaActionData.{v}) where
  /-- The underlying function of the actual inertia restriction. -/
  inertiaMap : source.inertia → target.inertia
  /-- The underlying function of the actual decomposition restriction. -/
  decompositionMap : source.decomposition → target.decomposition
  /-- The underlying function of the literal residue embedding. -/
  residueMap : target.residue → source.residue
def

actualTameCoordinateScalarData

L45 ↗
EtaleFundamentalGroups.Inertia.actualTameCoordinateScalarData
Documentation

The SAME original finite coordinate and the SAME original actions.

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) (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 actualTameCoordinateScalarData (E : FiniteGaloisIntermediateField K L) :
    ScalarInertiaActionData.{w} where
  inertia := (actualNormalizationInertiaGroup A K L Q).carrier
  decomposition := (normalizationDecompositionGroup A K L Q).carrier
  residue := Q.ResidueField
  character σ := ((actualFiniteTameCoordinate A K L Q E).hom'.toFun σ).val.val
  conjugate := originalFiniteNormalizationInertiaConjugate A K L Q
  action d := (actualNormalizationResidueFieldMap A K L Q d).toFun
def

actualScalarInertiaRestriction

L55 ↗
EtaleFundamentalGroups.Inertia.actualScalarInertiaRestriction
Documentation

Store the actual inertia restriction with its native source and target closed.

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) (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 actualScalarInertiaRestriction (E : FiniteGaloisIntermediateField K L) :
    (actualTameCoordinateScalarData A K L Q E).inertia →
      (actualFiniteTameScalarData A K L Q E).inertia
def

actualScalarDecompositionRestriction

L61 ↗
EtaleFundamentalGroups.Inertia.actualScalarDecompositionRestriction
Documentation

Store the actual decomposition restriction with the SAME closed carriers.

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) (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 actualScalarDecompositionRestriction (E : FiniteGaloisIntermediateField K L) :
    (actualTameCoordinateScalarData A K L Q E).decomposition →
      (actualFiniteTameScalarData A K L Q E).decomposition
def

actualScalarResidueInclusion

L67 ↗
EtaleFundamentalGroups.Inertia.actualScalarResidueInclusion
Documentation

Store the literal finite residue embedding, with no action comparison assumed.

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) (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 actualScalarResidueInclusion (E : FiniteGaloisIntermediateField K L) :
    (actualFiniteTameScalarData A K L Q E).residue →
      (actualTameCoordinateScalarData A K L Q E).residue
def

actualTameScalarRestrictionData

L73 ↗
EtaleFundamentalGroups.Inertia.actualTameScalarRestrictionData
Documentation

Assemble only the three independently constructed actual functions.

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) (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 actualTameScalarRestrictionData (E : FiniteGaloisIntermediateField K L) :
    ScalarInertiaRestrictionData (actualTameCoordinateScalarData A K L Q E)
      (actualFiniteTameScalarData A K L Q E) where
  inertiaMap := actualScalarInertiaRestriction A K L Q E
  decompositionMap := actualScalarDecompositionRestriction A K L Q E
  residueMap := actualScalarResidueInclusion A K L Q E
theorem

actualTameScalarRestrictionData_character

L81 ↗
EtaleFundamentalGroups.Inertia.actualTameScalarRestrictionData_character
Documentation

This diagram's character equation is the existing actual coordinate composition.

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) (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 actualTameScalarRestrictionData_character
    (E : FiniteGaloisIntermediateField K L)
    (σ : (actualTameCoordinateScalarData A K L Q E).inertia) :
    (actualTameCoordinateScalarData A K L Q E).character σ =
      (actualTameScalarRestrictionData A K L Q E).residueMap
        ((actualFiniteTameScalarData A K L Q E).character
          ((actualTameScalarRestrictionData A K L Q E).inertiaMap σ))
theorem

actualTameScalarRestrictionData_conjugate

L90 ↗
EtaleFundamentalGroups.Inertia.actualTameScalarRestrictionData_conjugate
Documentation

The diagram uses the proved actual original-to-finite conjugation comparison.

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) (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 actualTameScalarRestrictionData_conjugate
    (E : FiniteGaloisIntermediateField K L)
    (d : (actualTameCoordinateScalarData A K L Q E).decomposition)
    (σ : (actualTameCoordinateScalarData A K L Q E).inertia) :
    (actualTameScalarRestrictionData A K L Q E).inertiaMap
        ((actualTameCoordinateScalarData A K L Q E).conjugate d σ) =
      (actualFiniteTameScalarData A K L Q E).conjugate
        ((actualTameScalarRestrictionData A K L Q E).decompositionMap d)
        ((actualTameScalarRestrictionData A K L Q E).inertiaMap σ)
theorem

actualTameScalarRestrictionData_residue

L102 ↗
EtaleFundamentalGroups.Inertia.actualTameScalarRestrictionData_residue
Documentation

Its residue-action equation is the independently proved literal inclusion square.

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) (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 actualTameScalarRestrictionData_residue
    (E : FiniteGaloisIntermediateField K L)
    (d : (actualTameCoordinateScalarData A K L Q E).decomposition)
    (x : (actualFiniteTameScalarData A K L Q E).residue) :
    (actualTameScalarRestrictionData A K L Q E).residueMap
        ((actualFiniteTameScalarData A K L Q E).action
          ((actualTameScalarRestrictionData A K L Q E).decompositionMap d) x) =
      (actualTameCoordinateScalarData A K L Q E).action d
        ((actualTameScalarRestrictionData A K L Q E).residueMap x)

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