ModuleActualNormalizationInertiaTopology.lean
Nyll.EtaleFundamentalGroups.Inertia.ActualNormalizationInertiaTopology
4 declarations indexed from sourceView source ↗ Module documentation
Original subgroup topology on native normalization inertia
The native actual inertia group inherits exactly the subspace topology of its literal subgroup in the original Krull Galois group. Its topological group and separation properties are inherited from that same subgroup.
Declarations
EtaleFundamentalGroups.Inertia.actualNormalizationInertiaGroup_topologicalSpace
DocumentationThe topology induced by the literal inclusion into the original Krull Galois group, identical to the existing raw subgroup topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
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]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
EtaleFundamentalGroups.Inertia.actualNormalizationInertiaGroup_isTopologicalGroup
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
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]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
EtaleFundamentalGroups.Inertia.actualNormalizationInertiaGroup_t2Space
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
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]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)
EtaleFundamentalGroups.Inertia.actualNormalizationInertiaGroup_totallyDisconnectedSpace
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
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]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier)