ModuleActualTameQuotientGroup.lean
Nyll.EtaleFundamentalGroups.Inertia.ActualTameQuotientGroup
7 declarations indexed from sourceView source ↗ Module documentation
The literal original inertia quotient by the independent wild subgroup
The group, topology and quotient projection are the existing quotient constructions on the SAME original inertia and SAME independent subgroup. No character or kernel definition enters this native data owner.
Declarations
EtaleFundamentalGroups.Inertia.actualTameQuotientGroup
DocumentationThe literal quotient I/P, retaining the independently defined P.
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]
EtaleFundamentalGroups.Inertia.actualTameQuotientGroup_topologicalSpace
DocumentationThe same quotient carries the quotient of the original inertia 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]
EtaleFundamentalGroups.Inertia.actualTameQuotientProjection
DocumentationThe actual quotient projection from 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]
EtaleFundamentalGroups.Inertia.actualTameQuotientProjection_isQuotientMap
DocumentationThis native projection has exactly the existing quotient 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]
EtaleFundamentalGroups.Inertia.actualTameQuotientGroup_compactSpace
DocumentationCompactness is inherited from the proved compact 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]
EtaleFundamentalGroups.Inertia.actualTameQuotientProjection_surjective
DocumentationThe literal quotient projection is onto the SAME tame quotient.
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]
EtaleFundamentalGroups.Inertia.actualTameQuotientProjection_ker
DocumentationThe literal quotient projection has exactly the independent wild kernel.
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]