NYLL
Module

Residue.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Normalization.Residue
22 declarations indexed from sourceView source ↗

Module documentation

Residue separability in a tower of normalization rings

This file specializes the tame-inertia residue criterion to the integral closures of a Dedekind domain in a finite Galois tower. It supplies the two residue-separability inputs used by the normalization form of Abhyankar's lemma.

Imports2
Imported by2

Declarations

instance

residueNormalizationAlgebra

L40 ↗
TameAbhyankar.SGA1.residueNormalizationAlgebra
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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
Lean source · statement
instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E)
instance

residueNormalizationScalarTower

L44 ↗
TameAbhyankar.SGA1.residueNormalizationScalarTower
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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
Lean source · statement
instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E)
instance

residueLowerPrime_liesOver

L48 ↗
TameAbhyankar.SGA1.residueLowerPrime_liesOver
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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
Lean source · full declaration
instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

residueBasePrime_liesOver

L54 ↗
TameAbhyankar.SGA1.residueBasePrime_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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_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 residueBasePrime_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

residueTopPrime_liesOverBase

L60 ↗
TameAbhyankar.SGA1.residueTopPrime_liesOverBase
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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
instance

residueLowerPrime_isMaximal

L68 ↗
TameAbhyankar.SGA1.residueLowerPrime_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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
Lean source · statement
instance residueLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

residueBasePrime_isMaximal

L73 ↗
TameAbhyankar.SGA1.residueBasePrime_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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

residueLowerToTopFieldAlgebra

L78 ↗
TameAbhyankar.SGA1.residueLowerToTopFieldAlgebra
Source context 20 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
Lean source · statement
instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E
instance

residueLowerToTopFieldTower

L82 ↗
TameAbhyankar.SGA1.residueLowerToTopFieldTower
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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
Lean source · statement
instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E
instance

residueNormalizationToTopFieldTower

L86 ↗
TameAbhyankar.SGA1.residueNormalizationToTopFieldTower
Source context 22 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
Lean source · statement
instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E
instance

residueLowerDedekind

L90 ↗
TameAbhyankar.SGA1.residueLowerDedekind
Source context 23 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
Lean source · statement
instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M)
instance

residueLowerFinite

L94 ↗
TameAbhyankar.SGA1.residueLowerFinite
Source context 24 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
Lean source · statement
instance residueLowerFinite :
    Module.Finite V (integralClosure V M)
instance

residueLowerFractionRing

L98 ↗
TameAbhyankar.SGA1.residueLowerFractionRing
Source context 25 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
Lean source · statement
instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M
instance

residueLowerTorsionFree

L103 ↗
TameAbhyankar.SGA1.residueLowerTorsionFree
Source context 26 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
Lean source · statement
instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M)
instance

residueLowerGaloisFinite

L120 ↗
TameAbhyankar.SGA1.residueLowerGaloisFinite
Source context 27 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
Lean source · statement
instance residueLowerGaloisFinite : Finite Gal(M/K)
instance

residueTopGaloisFinite

L123 ↗
TameAbhyankar.SGA1.residueTopGaloisFinite
Source context 28 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
Lean source · statement
instance residueTopGaloisFinite : Finite Gal(E/K)
instance

residueTopNormalizationAction

L126 ↗
TameAbhyankar.SGA1.residueTopNormalizationAction
Source context 29 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
Lean source · statement
instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E)
instance

residueLowerNormalizationAction

L130 ↗
TameAbhyankar.SGA1.residueLowerNormalizationAction
Source context 30 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
noncomputable local instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
Lean source · statement
instance residueLowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M)
instance

residueLowerIsGaloisGroup

L134 ↗
TameAbhyankar.SGA1.residueLowerIsGaloisGroup
Source context 31 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
noncomputable local instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance residueLowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
instance residueLowerIsGaloisGroup :
    IsGaloisGroup Gal(M/K) V (integralClosure V M)
theorem

normalizationLowerResidue_isSeparable_of_inertia_card_coprime

L143 ↗
TameAbhyankar.SGA1.normalizationLowerResidue_isSeparable_of_inertia_card_coprime
Documentation

If lower inertia is prime to the exponential characteristic of the base residue field, then the residue extension from the base to the contraction in the normalization in M is separable.

Source context 33 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
noncomputable local instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance residueLowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
local instance residueLowerIsGaloisGroup :
    IsGaloisGroup Gal(M/K) V (integralClosure V M) :=
  IsGaloisGroup.of_isFractionRing Gal(M/K)
    V (integralClosure V M) K M
omit [IsScalarTower V K E] in
Lean source · statement
theorem normalizationLowerResidue_isSeparable_of_inertia_card_coprime
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal]
    (hV : ¬ IsField V)
    (hcop : Nat.Coprime
      (Nat.card
        ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
          Gal(M/K)))
      (ringExpChar
        (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q))) :
    Algebra.IsSeparable
      (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q)
      (integralClosure V M ⧸
        normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
theorem

normalizationTopResidue_isSeparable_of_inertia_card_coprime

L169 ↗
TameAbhyankar.SGA1.normalizationTopResidue_isSeparable_of_inertia_card_coprime
Documentation

If top inertia is prime to the exponential characteristic of the base residue field, then the residue extension from the base directly to the top normalization prime is separable.

Source context 33 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
noncomputable local instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance residueLowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
local instance residueLowerIsGaloisGroup :
    IsGaloisGroup Gal(M/K) V (integralClosure V M) :=
  IsGaloisGroup.of_isFractionRing Gal(M/K)
    V (integralClosure V M) K M
omit [IsScalarTower V K M] [IsGalois K M] in
Lean source · statement
theorem normalizationTopResidue_isSeparable_of_inertia_card_coprime
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal]
    (hV : ¬ IsField V)
    (hcop : Nat.Coprime
      (Nat.card (Q.toAddSubgroup.inertia Gal(E/K)))
      (ringExpChar
        (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q))) :
    Algebra.IsSeparable
      (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q)
      (integralClosure V E ⧸ Q)
theorem

normalizationRelativeResidue_isSeparable_of_top_inertia_card_coprime

L206 ↗
TameAbhyankar.SGA1.normalizationRelativeResidue_isSeparable_of_top_inertia_card_coprime
Documentation

The same coprimality condition on top inertia also makes the upper step of the residue tower, from the contraction in M to Q, separable.

Source context 33 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] [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 [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E] [IsGalois K M]
local instance residueNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance residueNormalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) :=
  normalizationScalarTower (V := V) M
local instance residueLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance residueBasePrime_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 residueTopPrime_liesOverBase
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) :=
  Ideal.LiesOver.trans Q
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q)
local instance residueLowerPrime_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 residueBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance residueLowerToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  lowerNormalizationToTopFieldAlgebra (V := V) M
local instance residueLowerToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  lowerNormalizationToTopFieldTower (V := V) M
local instance residueNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E :=
  normalizationToTopFieldTower (V := V) M
local instance residueLowerDedekind :
    IsDedekindDomain (integralClosure V M) :=
  IsIntegralClosure.isDedekindDomain V K M (integralClosure V M)
local instance residueLowerFinite :
    Module.Finite V (integralClosure V M) :=
  IsIntegralClosure.finite V K M (integralClosure V M)
local instance residueLowerFractionRing :
    IsFractionRing (integralClosure V M) M :=
  IsIntegralClosure.isFractionRing_of_finite_extension
    V K M (integralClosure V M)
local instance residueLowerTorsionFree :
    Module.IsTorsionFree V (integralClosure V M) := by
  have hVM : Function.Injective (algebraMap V M) := by
    intro x y hxy
    apply IsFractionRing.injective V K
    apply (algebraMap K M).injective
    calc
      algebraMap K M (algebraMap V K x) = algebraMap V M x :=
        (IsScalarTower.algebraMap_apply V K M x).symm
      _ = algebraMap V M y := hxy
      _ = algebraMap K M (algebraMap V K y) :=
        IsScalarTower.algebraMap_apply V K M y
  exact @IsIntegralClosure.isTorsionFree
    V (integralClosure V M) M _ _ _ _ _ _ _
    (lowerNormalizationToFractionFieldTower (V := V) M)
    (Module.isTorsionFree_iff_algebraMap_injective.mpr hVM)
local instance residueLowerGaloisFinite : Finite Gal(M/K) :=
  IsGaloisGroup.finite Gal(M/K) K M
local instance residueTopGaloisFinite : Finite Gal(E/K) :=
  IsGaloisGroup.finite Gal(E/K) K E
noncomputable local instance residueTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance residueLowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
local instance residueLowerIsGaloisGroup :
    IsGaloisGroup Gal(M/K) V (integralClosure V M) :=
  IsGaloisGroup.of_isFractionRing Gal(M/K)
    V (integralClosure V M) K M
omit [IsScalarTower V K M] [IsGalois K M] in
Lean source · statement
theorem normalizationRelativeResidue_isSeparable_of_top_inertia_card_coprime
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal]
    (hV : ¬ IsField V)
    (hcop : Nat.Coprime
      (Nat.card (Q.toAddSubgroup.inertia Gal(E/K)))
      (ringExpChar
        (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q))) :
    Algebra.IsSeparable
      (integralClosure V M ⧸
        normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
      (integralClosure V E ⧸ Q)

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