NYLL
Module

ActualNormalizationInertiaCompact.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationInertiaCompact
2 declarations indexed from sourceView source ↗

Module documentation

Compactness of original normalization inertia

The topology is the original Krull topology restricted to the literal normalization inertia subgroup. Closedness comes from the already proved openness of the original coefficient stabilizers.

Imports8
Imported by5

Declarations

theorem

actualNormalizationInertia_isClosed

L38 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationInertia_isClosed
Documentation

Actual normalization inertia is closed for the original Krull topology.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem actualNormalizationInertia_isClosed (Q : Ideal (integralClosure A L)) :
    IsClosed (Q.inertia Gal(L/K)).carrier
theorem

actualNormalizationInertia_compactSpace

L46 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationInertia_compactSpace
Documentation

The actual original inertia group is compact in its inherited topology.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem actualNormalizationInertia_compactSpace
    (Q : Ideal (normalizationCommAlgCat A L).carrier) :
    CompactSpace (actualNormalizationInertiaGroup 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.