Module

ActualTameRootsGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsGroup

9 declarations indexed from sourceView source ↗

Module documentation

The SAME tame roots limit as its native group object

The carrier, group, and topology are exactly those of the existing actual roots limit. This native object is shared by the quotient isomorphism and the original decomposition action, so neither must reopen the raw index.

Imports4

Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsTopology
Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacter
Nyll.EtaleFundamentalGroups.Inertia.ActualTameCharacterContinuity
Mathlib.Algebra.Category.Grp.Basic

Imported by7

def

actualTameRootsGroup

L37 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsGroup

Documentation

The existing actual limit, retaining its existing coordinatewise group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

def actualTameRootsGroup : GrpCat.{w}

instance

actualTameRootsGroup_topologicalSpace

L41 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsGroup_topologicalSpace

Documentation

The topology is literally the topology of the existing actual limit.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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 actualTameRootsGroup_topologicalSpace :
    TopologicalSpace (actualTameRootsGroup A K L Q).carrier

instance

actualTameRootsGroup_t2Space

L45 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsGroup_t2Space

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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 actualTameRootsGroup_t2Space :
    T2Space (actualTameRootsGroup A K L Q).carrier

instance

actualTameRootsGroup_isTopologicalGroup

L49 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsGroup_isTopologicalGroup

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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 actualTameRootsGroup_isTopologicalGroup :
    IsTopologicalGroup (actualTameRootsGroup A K L Q).carrier

def

actualTameCharacterMorphism

L54 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacterMorphism

Documentation

The SAME constructed character as a morphism of the native group objects.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

def actualTameCharacterMorphism :
    actualNormalizationInertiaGroup A K L Q ⟶ actualTameRootsGroup A K L Q

def

actualTameRootsScalar

L59 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsScalar

Documentation

The literal coefficient of an element of the SAME actual roots group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

def actualTameRootsScalar
    (n : Subtype (actualFiniteTameDegreeSet A K L Q))
    (x : (actualTameRootsGroup A K L Q).carrier) :
    (normalizationCommAlgCat A L).carrier ⧸ Q

theorem

actualTameRootsScalar_ext

L66 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsScalar_ext

Documentation

Literal scalar coordinates jointly separate points of the native group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

theorem actualTameRootsScalar_ext
    (x y : (actualTameRootsGroup A K L Q).carrier)
    (h : ∀ n : Subtype (actualFiniteTameDegreeSet A K L Q),
      actualTameRootsScalar A K L Q n x = actualTameRootsScalar A K L Q n y) :
    x = y

theorem

actualTameCharacterMorphism_continuous

L77 ↗

EtaleFundamentalGroups.Inertia.actualTameCharacterMorphism_continuous

Documentation

Continuity of the exact stored character between the two native groups.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

theorem actualTameCharacterMorphism_continuous :
    Continuous (actualTameCharacterMorphism A K L Q).hom'.toFun

theorem

actualTameRootsScalar_character

L82 ↗

EtaleFundamentalGroups.Inertia.actualTameRootsScalar_character

Documentation

Native scalar evaluation of the SAME character is its existing actual coordinate.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
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

theorem actualTameRootsScalar_character
    (n : Subtype (actualFiniteTameDegreeSet A K L Q))
    (σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
    actualTameRootsScalar A K L Q n
        ((actualTameCharacterMorphism A K L Q).hom'.toFun σ) =
      ((actualTameCoordinate A K L Q n).toFun σ).val.val

Module documentation

The SAME tame roots limit as its native group object

Declarations