ModuleActualTameRootsTopology.lean
Nyll.EtaleFundamentalGroups.Inertia.ActualTameRootsTopology
3 declarations indexed from sourceView source ↗ Module documentation
Topology of the SAME actual tame roots limit
The existing roots system already chooses the discrete topology at every stage. Its existing inverse-limit topology is therefore Hausdorff, and the existing coordinatewise group operations are continuous.
Declarations
EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem_discreteTopology
DocumentationEach actual stage has precisely its already assigned discrete topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
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]
EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem_t2Space
DocumentationThe SAME actual roots limit is Hausdorff in its existing topology.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
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]
EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem_isTopologicalGroup
DocumentationThe SAME actual roots limit has continuous existing group operations.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
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]