ModuleNativeGaloisGroupTopology.lean
Nyll.EtaleFundamentalGroups.Inertia.NativeGaloisGroupTopology
4 declarations indexed from sourceView source ↗ Module documentation
Original Krull topology on native Galois group owners
The native group objects retain exactly Mathlib's original Krull topology. The finite native owner inherits its already proved discrete Krull topology. No normalization ring or inertia subgroup is opened in this field-only scope.
Declarations
EtaleFundamentalGroups.Inertia.galoisGroupObject_topologicalSpace
DocumentationThe original Krull topology on the native ambient Galois 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
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
EtaleFundamentalGroups.Inertia.galoisGroupObject_isTopologicalGroup
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
EtaleFundamentalGroups.Inertia.finiteGaloisGroupObject_topologicalSpace
DocumentationThe finite group retains its own original Krull 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
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
EtaleFundamentalGroups.Inertia.finiteGaloisGroupObject_discreteTopology
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]