Module

NativeCanonicalTameScalarData.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeCanonicalTameScalarData

3 declarations indexed from sourceView source ↗

Module documentation

The actual finite canonical scalar action data

This data-only interface closes the native group and root carriers. It stores actual functions and no propositions. Its sole factory uses the existing canonical normalized character, conjugation and residue action; equivariance is proved separately from the existing finite theorem.

Imports2

Imported by2

structure

ScalarInertiaActionData

L26 ↗

EtaleFundamentalGroups.Inertia.ScalarInertiaActionData

Documentation

The carrier and scalar functions of an actual inertia action. No laws are fields.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · full declaration

structure ScalarInertiaActionData where
  /-- The actual inertia carrier. -/
  inertia : Type v
  /-- The actual decomposition carrier. -/
  decomposition : Type v
  /-- The actual residue coefficient carrier. -/
  residue : Type v
  /-- The scalar projection of the existing canonical character. -/
  character : inertia → residue
  /-- The existing decomposition conjugation on inertia. -/
  conjugate : decomposition → inertia → inertia
  /-- The scalar action of the existing residue automorphism. -/
  action : decomposition → residue → residue

def

commAlgCanonicalTameScalarData

L41 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameScalarData

Documentation

Store exactly the existing native canonical finite scalar maps.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · full declaration

def commAlgCanonicalTameScalarData
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B.carrier] [Finite (B.carrier ≃ₐ[A] B.carrier)]
    (Q : Ideal B.carrier) [Q.IsMaximal] (hQ : Q ≠ ⊥) :
    ScalarInertiaActionData.{v} where
  inertia := (commAlgIdealInertiaGroup A B Q).carrier
  decomposition := (commAlgIdealDecompositionGroup A B Q).carrier
  residue := Q.ResidueField
  character σ := ((commAlgCanonicalTameCharacter A B Q hQ).toFun σ).val.val
  conjugate := commAlgIdealInertiaConjugate A B Q
  action d := (commAlgDecompositionResidueRingHom A B Q d).toFun

theorem

commAlgCanonicalTameScalarData_equivariant

L54 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameScalarData_equivariant

Documentation

The actual stored maps satisfy canonical scalar equivariance.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem commAlgCanonicalTameScalarData_equivariant
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B.carrier] [Finite (B.carrier ≃ₐ[A] B.carrier)]
    (Q : Ideal B.carrier) [Q.IsMaximal] (hQ : Q ≠ ⊥)
    (d : (commAlgCanonicalTameScalarData A B Q hQ).decomposition)
    (σ : (commAlgCanonicalTameScalarData A B Q hQ).inertia) :
    (commAlgCanonicalTameScalarData A B Q hQ).character
        ((commAlgCanonicalTameScalarData A B Q hQ).conjugate d σ) =
      (commAlgCanonicalTameScalarData A B Q hQ).action d
        ((commAlgCanonicalTameScalarData A B Q hQ).character σ)

Module documentation

The actual finite canonical scalar action data

Declarations

ScalarInertiaActionData

commAlgCanonicalTameScalarData

commAlgCanonicalTameScalarData_equivariant