NYLL
Module

DVR.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Normalization.DVR
12 declarations indexed from sourceView source ↗

Module documentation

Normalizations over an arbitrary discrete valuation ring

For a DVR the contraction of every maximal prime in a finite normalization is the unique maximal ideal of the base. Consequently, all residue fields in a normalization tower have the same exponential characteristic as the fixed residue field of the DVR.

Imports2
Imported by2

Declarations

theorem

isDedekindDomain_of_isDiscreteValuationRing

L31 ↗
TameAbhyankar.SGA1.isDedekindDomain_of_isDiscreteValuationRing
Documentation

A discrete valuation ring is a Dedekind domain. This named helper is useful when specializing results whose base is stated as an arbitrary Dedekind domain.

Source context 4 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
Lean source · statement
theorem isDedekindDomain_of_isDiscreteValuationRing
    (V : Type uV) [CommRing V] [IsDomain V] [IsDiscreteValuationRing V] :
    IsDedekindDomain V
instance

dvrNormalizationDedekind

L48 ↗
TameAbhyankar.SGA1.dvrNormalizationDedekind
Source context 13 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
Lean source · statement
instance dvrNormalizationDedekind : IsDedekindDomain V
instance

dvrNormalizationAlgebra

L51 ↗
TameAbhyankar.SGA1.dvrNormalizationAlgebra
Source context 14 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
Lean source · statement
instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E)
instance

dvrNormalizationScalarTower

L55 ↗
TameAbhyankar.SGA1.dvrNormalizationScalarTower
Source context 15 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
Lean source · statement
instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E)
instance

dvrLowerPrime_liesOver

L59 ↗
TameAbhyankar.SGA1.dvrLowerPrime_liesOver
Source context 16 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
Lean source · full declaration
instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

dvrBasePrime_liesOver

L65 ↗
TameAbhyankar.SGA1.dvrBasePrime_liesOver
Source context 17 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
Lean source · full declaration
instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

dvrLowerPrime_isMaximal

L71 ↗
TameAbhyankar.SGA1.dvrLowerPrime_isMaximal
Source context 18 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
Lean source · statement
instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

dvrBasePrime_isMaximal

L76 ↗
TameAbhyankar.SGA1.dvrBasePrime_isMaximal
Source context 19 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
Lean source · statement
instance dvrBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal
theorem

normalizationBasePrime_eq_maximalIdeal

L86 ↗
TameAbhyankar.SGA1.normalizationBasePrime_eq_maximalIdeal
Documentation

The base contraction of every maximal prime of the top normalization is the unique maximal ideal of the DVR.

Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance dvrBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
omit [Algebra V K] [IsFractionRing V K] [IsScalarTower V K E]
  [IsScalarTower V K M] [FiniteDimensional K E] [IsGalois K E]
  [IsGalois K M] in
Lean source · statement
theorem normalizationBasePrime_eq_maximalIdeal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    normalizationBasePrime (V := V) (K := K) (E := E) M Q =
      IsLocalRing.maximalIdeal V
theorem

normalizationBase_ringExpChar_eq_lower

L98 ↗
TameAbhyankar.SGA1.normalizationBase_ringExpChar_eq_lower
Documentation

The residue field of the contraction in the normalization in M has the same exponential characteristic as the fixed residue field of the DVR.

Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance dvrBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
omit [Algebra V K] [IsFractionRing V K] [IsScalarTower V K E]
  [IsScalarTower V K M] [FiniteDimensional K E] [IsGalois K E]
  [IsGalois K M] in
Lean source · statement
theorem normalizationBase_ringExpChar_eq_lower
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    ringExpChar (V ⧸ IsLocalRing.maximalIdeal V) =
      ringExpChar
        (integralClosure V M ⧸
          normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
theorem

normalizationBase_ringExpChar_eq_top

L121 ↗
TameAbhyankar.SGA1.normalizationBase_ringExpChar_eq_top
Documentation

The residue field at a maximal prime of the top normalization has the same exponential characteristic as the fixed residue field of the DVR.

Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance dvrBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
omit [Algebra V K] [IsFractionRing V K] [Algebra K E]
  [IsScalarTower V K E] [Algebra V M] [IsScalarTower V K M]
  [IsScalarTower V M E] [FiniteDimensional K E] [IsGalois K E]
  [IsGalois K M] in
Lean source · statement
theorem normalizationBase_ringExpChar_eq_top
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    ringExpChar (V ⧸ IsLocalRing.maximalIdeal V) =
      ringExpChar (integralClosure V E ⧸ Q)
theorem

normalizationResidue_ringExpChar_eq_of_base

L143 ↗
TameAbhyankar.SGA1.normalizationResidue_ringExpChar_eq_of_base
Documentation

A fixed exponential residue characteristic of the DVR transports to the lower and top residue fields for every maximal top prime Q.

Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
section GaloisTower
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance dvrNormalizationDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance dvrNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance dvrNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance dvrLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrBasePrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance dvrLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance dvrBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
omit [Algebra V K] [IsFractionRing V K] [IsScalarTower V K E]
  [IsScalarTower V K M] [FiniteDimensional K E] [IsGalois K E]
  [IsGalois K M] in
Lean source · statement
theorem normalizationResidue_ringExpChar_eq_of_base
    (q : ℕ)
    (hchar : ringExpChar (V ⧸ IsLocalRing.maximalIdeal V) = q)
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    ringExpChar
          (integralClosure V M ⧸
            normalizationLowerPrime (V := V) (K := K) (E := E) M Q) = q ∧
      ringExpChar (integralClosure V E ⧸ Q) = q

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.