Module

FiniteNormalizationTameProperties.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationTameProperties

2 declarations indexed from sourceView source ↗

Module documentation

Tame orders of finite normalizations

Proves positivity of finite-normalization tame orders and their invertibility in the original local coefficient ring.

Imports2

Imported by2

theorem

finiteNormalizationTameOrder_pos

L29 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationTameOrder_pos

Documentation

Positivity for all actual finite-normalization primes, before an upper normalization prime is brought into the scope.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Inertia
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDedekindDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (E : FiniteGaloisIntermediateField K L)

Lean source · full declaration

theorem finiteNormalizationTameOrder_pos
    (q : Ideal (finiteAbsoluteNormalizationAlgebra A K L E)) [q.IsPrime] (hq : q ≠ ⊥) :
    let : IsDedekindDomain (finiteAbsoluteNormalizationAlgebra A K L E) :=
      finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K L E
    0 < commAlgIdealTameOrder A (finiteAbsoluteNormalizationAlgebra A K L E) q hq :=
  by
    let q' : Ideal (SchemeTheory.normalizationCommAlgCat A (finiteLevelFieldAlgebra A K L E)) := q
    have : q'.IsPrime := ‹q.IsPrime›
    exact nativeFiniteNormalizationTameOrder_pos A K (finiteLevelFieldAlgebra A K L E)
      (Field.toIsField (finiteLevelFieldAlgebra A K L E)) q' hq

theorem

finiteNormalizationTameOrder_isUnit

L42 ↗

EtaleFundamentalGroups.Inertia.finiteNormalizationTameOrder_isUnit