NYLL
Module

ActualNormalizationWildTopology.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationWildTopology
7 declarations indexed from sourceView source ↗

Module documentation

Compact wild inertia in the original topology

Every finite wild condition is closed because its actual restriction is locally constant. The original wild subgroup is their intersection, hence compact in the existing Krull/subgroup topology.

Imports13
Imported by6

Declarations

instance

actualNormalizationWildGroup_topologicalSpace

L45 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_topologicalSpace
Documentation

The original wild group has precisely the subtype topology induced by its literal inclusion into the existing original inertia group.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildGroup_topologicalSpace :
    TopologicalSpace (actualNormalizationWildGroup A K L Q).carrier
instance

actualNormalizationWildGroup_isTopologicalGroup

L53 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_isTopologicalGroup
Documentation

The same canonical subgroup group law is continuous for that induced topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildGroup_isTopologicalGroup :
    IsTopologicalGroup (actualNormalizationWildGroup A K L Q).carrier
theorem

actualNormalizationWildSubgroup_isClosed

L58 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildSubgroup_isClosed
Documentation

The independent global wild subgroup is closed in original inertia.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildSubgroup_isClosed :
    IsClosed (actualNormalizationWildSubgroup A K L Q).carrier
theorem

actualNormalizationWildGroup_compactSpace

L70 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_compactSpace
Documentation

The same original wild group is compact, with its inherited topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildGroup_compactSpace :
    CompactSpace (actualNormalizationWildGroup A K L Q).carrier
theorem

actualNormalizationWildRestriction_isLocallyConstant

L78 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildRestriction_isLocallyConstant
Documentation

Its actual finite wild coordinates are locally constant in that topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildRestriction_isLocallyConstant
    (E : FiniteGaloisIntermediateField K L) :
    IsLocallyConstant (actualNormalizationWildRestriction A K L Q E).hom'.toFun
theorem

actualNormalizationWildGroup_t2Space

L90 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_t2Space
Documentation

The SAME independent wild group is Hausdorff in its inherited topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildGroup_t2Space :
    T2Space (actualNormalizationWildGroup A K L Q).carrier
theorem

actualNormalizationWildGroup_totallyDisconnectedSpace

L97 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationWildGroup_totallyDisconnectedSpace
Documentation

The SAME independent wild group is totally disconnected in that topology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
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 actualNormalizationWildGroup_totallyDisconnectedSpace :
    TotallyDisconnectedSpace (actualNormalizationWildGroup A K L Q).carrier

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