Module

ActualFiniteTameScalarData.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameScalarData

2 declarations indexed from sourceView source ↗

Module documentation

The canonical scalar action at the actual finite normalization

The factory closes the finite root interface before original inertia and decomposition elements occur. Every field is the already constructed map.

Imports3

Imported by2

def

actualFiniteTameScalarData

L33 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameScalarData

Documentation

The SAME normalized finite scalar character, conjugation and 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) (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 actualFiniteTameScalarData (E : FiniteGaloisIntermediateField K L) :
    ScalarInertiaActionData.{w}

theorem

actualFiniteTameScalarData_equivariant

L47 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameScalarData_equivariant