EtaleFundamentalGroups.Inertia.actualFiniteStageTameOrder_exists_primitiveRoot_finiteResidue
The finite residue field itself contains a primitive root of the SAME actual finite tame degree. No ambient residue field is opened here.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
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]
(E : FiniteGaloisIntermediateField K L)Lean source · full declaration
theorem actualFiniteStageTameOrder_exists_primitiveRoot_finiteResidue :
let : (finiteAbsoluteNormalizationPrime A K L Q E).IsPrime :=
finiteAbsoluteNormalizationPrime_isPrime A K L Q E
∃ ζ : (finiteAbsoluteNormalizationPrime A K L Q E).ResidueField,
IsPrimitiveRoot ζ (actualFiniteStageTameOrder A K L Q E) := by
intro qPrime
have : IsDedekindDomain (finiteAbsoluteNormalizationAlgebra A K L E).carrier :=
finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L E
have : Finite ((finiteAbsoluteNormalizationAlgebra A K L E).carrier ≃ₐ[A]
(finiteAbsoluteNormalizationAlgebra A K L E).carrier) :=
finiteAbsoluteNormalizationAutomorphisms_finite A K L E
exact commAlgIdealTameOrder_exists_primitiveRoot A
(finiteAbsoluteNormalizationAlgebra A K L E) (finiteAbsoluteNormalizationPrime A K L Q E)
(finiteAbsoluteNormalizationPrime_ne_bot A K L Q E)