EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalizationPrime_ne_bot
The literal contracted prime of the actual finite normalization is nonzero, derived from the original DVR and the original maximal prime.
Source context 6 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)) [Q.IsMaximal]
omit [IsGalois K L] inLean source · statement
theorem finiteAbsoluteNormalizationPrime_ne_bot
(E : FiniteGaloisIntermediateField K L) :
finiteAbsoluteNormalizationPrime A K L Q E ≠ ⊥