Nyll.EtaleFundamentalGroups.Inertia.NativeRamificationDiagram

Module documentation

The native data of the two ramification sequences

This stores group objects, their actual maps, the independent wild subgroup, and existing topologies. It stores no exactness, normality, surjectivity, comparison or other conclusion. The roots target is computed from the residue data, so it cannot be replaced by an unrelated abstract group.

structure

NativeRamificationDiagram

L26 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationDiagram

Documentation

Data of the original ramification diagram, with its intrinsic 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 NativeRamificationDiagram (R : NativeRamificationResidues.{u, w}) where
  /-- Original decomposition. -/
  decomposition : GrpCat.{w}
  /-- Original inertia. -/
  inertia : GrpCat.{w}
  /-- The automorphisms of the residue extension. -/
  residueAutomorphisms : GrpCat.{w}
  /-- The actual quotient of inertia by its independent wild subgroup. -/
  tameQuotient : GrpCat.{w}
  /-- Independently defined wild inertia inside original inertia. -/
  wild : Subgroup inertia.carrier
  /-- The literal inclusion of inertia into decomposition. -/
  inertiaInclusion : GrpCat.Hom inertia decomposition
  /-- The actual residue action. -/
  residueMorphism : GrpCat.Hom decomposition residueAutomorphisms
  /-- The literal quotient projection. -/
  quotientProjection : GrpCat.Hom inertia tameQuotient
  /-- The canonical character into the computed root limit. -/
  character : GrpCat.Hom inertia R.rootsGroup
  /-- Original decomposition conjugation on inertia. -/
  conjugate : decomposition.carrier → inertia.carrier → inertia.carrier
  /-- Original residue action on the same root limit. -/
  rootsAction : decomposition.carrier → R.rootsGroup.carrier → R.rootsGroup.carrier
  /-- The original inertia topology. -/
  inertiaTopology : TopologicalSpace inertia.carrier
  /-- The literal quotient topology. -/
  tameQuotientTopology : TopologicalSpace tameQuotient.carrier

Module documentation

The native data of the two ramification sequences

Declarations

NativeRamificationDiagram