ModuleActualFiniteWildImage.lean
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteWildImage
3 declarations indexed from sourceView source ↗ Module documentation
Actual finite wild subgroup images
Actual intrinsic finite inertia restriction is onto. The SAME actual wild subgroups have proved primary cardinalities, prime-to-characteristic indices and target normality. The original field environment is closed before the finite-group Sylow image theorem is applied.
Declarations
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_map_of_baseResidue_charP
DocumentationActual intrinsic inertia restriction has exactly the actual wild image in positive residue characteristic.
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)
[rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
[fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
[aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
(E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_map_of_baseResidue_charZero
DocumentationIn residue characteristic zero both actual wild subgroups are trivial, so the same inertia restriction has exactly the actual wild image.
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)
[rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
[fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
[aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
(E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_map
DocumentationActual finite inertia restriction maps the SAME intrinsic wild subgroup onto the target wild subgroup in every residue characteristic.
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)
[rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
[fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
[aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
(E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)