Module

NativeRamificationResidues.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeRamificationResidues

6 declarations indexed from sourceView source ↗

Module documentation

Native residue data for the ramification diagram

Only the two coefficient fields and the actual set of invertible natural exponents are stored. The target is computed as the literal root inverse limit over these degrees. No root group or comparison is supplied separately.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.PrimeToRootsInverseSystem
Nyll.EtaleFundamentalGroups.Inertia.RestrictedPrimeToRootsGroupSystem
Nyll.ProCGroups.InverseSystems.Basic
Mathlib.Algebra.Category.Grp.Basic

Imported by3

structure

NativeRamificationResidues

L29 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues

Documentation

The coefficient fields and degrees underlying a literal tame-root limit.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w

Lean source · full declaration

structure NativeRamificationResidues where
  /-- The original base residue field. -/
  baseResidue : Type u
  /-- Its retained field structure. -/
  [baseResidueField : Field baseResidue]
  /-- The residue field containing the roots. -/
  residue : Type w
  /-- Its retained field structure. -/
  [residueField : Field residue]
  /-- The actual residue-invertible natural degrees. -/
  degrees : Set (InvertibleExponent baseResidue)

def

rootsSystem

L47 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues.rootsSystem

Documentation

The literal power-transition roots system on the stored degrees.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w
attribute [local instance] NativeRamificationResidues.baseResidueField
  NativeRamificationResidues.residueField
namespace NativeRamificationResidues

Lean source · statement

def rootsSystem (R : NativeRamificationResidues.{u, w}) :
    InverseSystem.{0, w} (I := {n : InvertibleExponent R.baseResidue // R.degrees n})

instance

rootsSystem_groups

L52 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues.rootsSystem_groups

Documentation

The same canonical coordinatewise root groups.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w
attribute [local instance] NativeRamificationResidues.baseResidueField
  NativeRamificationResidues.residueField
namespace NativeRamificationResidues

Lean source · statement

instance rootsSystem_groups (R : NativeRamificationResidues.{u, w}) :
    ∀ n : {n : InvertibleExponent R.baseResidue // R.degrees n}, Group ((rootsSystem R).X n)

instance

rootsSystem_isGroupSystem

L56 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues.rootsSystem_isGroupSystem

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w
attribute [local instance] NativeRamificationResidues.baseResidueField
  NativeRamificationResidues.residueField
namespace NativeRamificationResidues

Lean source · statement

instance rootsSystem_isGroupSystem (R : NativeRamificationResidues.{u, w}) :
    IsGroupSystem (rootsSystem R)

def

rootsGroup

L61 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues.rootsGroup

Documentation

The actual inverse limit, retaining its coordinatewise group operations.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w
attribute [local instance] NativeRamificationResidues.baseResidueField
  NativeRamificationResidues.residueField
namespace NativeRamificationResidues

Lean source · statement

def rootsGroup (R : NativeRamificationResidues.{u, w}) : GrpCat.{w}

instance

rootsGroup_topologicalSpace

L65 ↗

EtaleFundamentalGroups.Inertia.NativeRamificationResidues.rootsGroup_topologicalSpace

Documentation

The root limit retains the original inverse-limit topology.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u w
attribute [local instance] NativeRamificationResidues.baseResidueField
  NativeRamificationResidues.residueField
namespace NativeRamificationResidues

Lean source · statement

instance rootsGroup_topologicalSpace (R : NativeRamificationResidues.{u, w}) :
    TopologicalSpace (rootsGroup R).carrier

Module documentation

Native residue data for the ramification diagram

Declarations

NativeRamificationResidues

rootsSystem

rootsSystem_groups

rootsSystem_isGroupSystem

rootsGroup

rootsGroup_topologicalSpace