NYLL
Module

NativeAbsoluteRamificationDiagram.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeAbsoluteRamificationDiagram
4 declarations indexed from sourceView source ↗

Module documentation

The native absolute ramification diagram

The group data are shared with the existing original DVR diagram. This retains its independent P, literal I/P and existing subgroup/quotient topologies once. The absolute diagram adds exactly the residue map and full-target character. Its roots action is computed from that SAME residue map and the existing coefficient action, rather than stored arbitrarily. No exactness, closure, normality, continuity or comparison fact is input data.

Imports6
Imported by3

Declarations

structure

NativeAbsoluteRamificationGroups

L30 ↗
EtaleFundamentalGroups.Inertia.NativeAbsoluteRamificationGroups
Documentation

The unchanged original D, I, P and I/P data, independent of the roots target.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u w
Lean source · full declaration
structure NativeAbsoluteRamificationGroups where
  /-- The original decomposition group. -/
  decomposition : GrpCat.{w}
  /-- The original inertia group. -/
  inertia : GrpCat.{w}
  /-- The literal quotient of inertia by its independent wild subgroup. -/
  tameQuotient : GrpCat.{w}
  /-- The independently defined wild subgroup. -/
  wild : Subgroup inertia.carrier
  /-- Original inclusion of inertia into decomposition. -/
  inertiaInclusion : GrpCat.Hom inertia decomposition
  /-- The literal quotient projection. -/
  quotientProjection : GrpCat.Hom inertia tameQuotient
  /-- Original decomposition conjugation on inertia. -/
  conjugate : decomposition.carrier → inertia.carrier → inertia.carrier
  /-- The existing inertia topology. -/
  inertiaTopology : TopologicalSpace inertia.carrier
  /-- The existing quotient topology. -/
  tameQuotientTopology : TopologicalSpace tameQuotient.carrier
def

nativeAbsoluteRamificationGroupsOfDiagram

L51 ↗
EtaleFundamentalGroups.Inertia.nativeAbsoluteRamificationGroupsOfDiagram
Documentation

Share actual group objects and topologies from the existing DVR diagram.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u w
Lean source · full declaration
def nativeAbsoluteRamificationGroupsOfDiagram
    (R : NativeRamificationResidues.{u, w}) (D : NativeRamificationDiagram R) :
    NativeAbsoluteRamificationGroups.{w} where
  decomposition := D.decomposition
  inertia := D.inertia
  tameQuotient := D.tameQuotient
  wild := D.wild
  inertiaInclusion := D.inertiaInclusion
  quotientProjection := D.quotientProjection
  conjugate := D.conjugate
  inertiaTopology := D.inertiaTopology
  tameQuotientTopology := D.tameQuotientTopology
structure

NativeAbsoluteRamificationDiagram

L65 ↗
EtaleFundamentalGroups.Inertia.NativeAbsoluteRamificationDiagram
Documentation

The two actual absolute maps into intrinsically computed full targets.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u w
Lean source · full declaration
structure NativeAbsoluteRamificationDiagram
    (R : NativeAbsoluteRamificationResidues.{u, w}) (G : NativeAbsoluteRamificationGroups.{w}) where
  /-- The SAME canonical absolute residue action. -/
  residueMorphism : GrpCat.Hom G.decomposition R.residueAutomorphisms
  /-- The SAME canonical character, postcomposed into the literal full roots group. -/
  character : GrpCat.Hom G.inertia R.rootsGroup
def

rootsAction

L78 ↗
EtaleFundamentalGroups.Inertia.NativeAbsoluteRamificationDiagram.rootsAction
Documentation

Decomposition acts by the SAME stored residue map on the full root coefficients.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u w
namespace NativeAbsoluteRamificationDiagram
variable {R : NativeAbsoluteRamificationResidues.{u, w}}
  {G : NativeAbsoluteRamificationGroups.{w}} (D : NativeAbsoluteRamificationDiagram R G)
Lean source · statement
def rootsAction (d : G.decomposition.carrier) (x : R.rootsGroup.carrier) :
    R.rootsGroup.carrier

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