Module

ActualTameRootsGroupSystem.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsGroupSystem

2 declarations indexed from sourceView source ↗

Module documentation

The existing actual roots system as a group system

Supplies the exact stage-group family and group-system class on the existing actual roots system. Both are the original prime-to-roots groups and their literal restriction; no group operation or inverse system is replaced.

Imports3

Imported by3

instance

actualFiniteTameRootsSystem_groups

L34 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem_groups

Documentation

The SAME existing prime-to-roots stage-group family at the actual degrees.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
universe u v w
attribute [local instance] Ideal.Quotient.field
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

instance actualFiniteTameRootsSystem_groups :
    ∀ n : Subtype (actualFiniteTameDegreeSet A K L Q),
      Group ((actualFiniteTameRootsSystem A K L Q).X n)

instance

actualFiniteTameRootsSystem_isGroupSystem

L42 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem_isGroupSystem