NYLL
Module

Inertia.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Normalization.Inertia
25 declarations indexed from sourceView source ↗

Module documentation

Inertia in a tower of normalization rings

This file instantiates the ideal-theoretic inertia tower for the integral closures of a Dedekind domain in a finite Galois tower of fields.

Imports3
Imported by5

Declarations

def

normalizationMap

L36 ↗
TameAbhyankar.SGA1.normalizationMap
Documentation

The canonical map from the normalization in M to the normalization in E, induced by the inclusion M ⊆ E.

Source context 11 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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]
Lean source · statement
def normalizationMap :
    integralClosure V M →ₐ[V] integralClosure V E
theorem

normalizationMap_coe

L42 ↗
TameAbhyankar.SGA1.normalizationMap_coe
Source context 12 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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]
omit [Algebra V K] [IsFractionRing V K] [IsScalarTower V K E]
  [IsScalarTower V K M] in
Lean source · statement
theorem normalizationMap_coe (x : integralClosure V M) :
    ((normalizationMap (V := V) (K := K) (E := E) M x :
      integralClosure V E) : E) = ((x : M) : E)
def

normalizationLowerPrime

L48 ↗
TameAbhyankar.SGA1.normalizationLowerPrime
Documentation

Contraction of a top normalization prime to the normalization in M.

Source context 11 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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]
Lean source · statement
def normalizationLowerPrime (Q : Ideal (integralClosure V E)) :
    Ideal (integralClosure V M)
def

normalizationBasePrime

L53 ↗
TameAbhyankar.SGA1.normalizationBasePrime
Documentation

Further contraction of a top normalization prime to the base ring.

Source context 11 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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]
Lean source · statement
def normalizationBasePrime (Q : Ideal (integralClosure V E)) : Ideal V
instance

normalizationAlgebra

L62 ↗
TameAbhyankar.SGA1.normalizationAlgebra
Source context 14 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E)
instance

normalizationScalarTower

L66 ↗
TameAbhyankar.SGA1.normalizationScalarTower
Source context 15 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
Lean source · statement
instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E)
instance

normalizationLowerPrime_liesOver

L74 ↗
TameAbhyankar.SGA1.normalizationLowerPrime_liesOver
Source context 16 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
Lean source · full declaration
instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

normalizationBasePrime_liesOver

L80 ↗
TameAbhyankar.SGA1.normalizationBasePrime_liesOver
Source context 17 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_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 normalizationBasePrime_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

lowerNormalizationToTopFieldAlgebra

L86 ↗
TameAbhyankar.SGA1.lowerNormalizationToTopFieldAlgebra
Source context 18 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E
instance

lowerNormalizationToFractionFieldTower

L91 ↗
TameAbhyankar.SGA1.lowerNormalizationToFractionFieldTower
Source context 19 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
Lean source · statement
instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M
instance

topNormalizationToFractionFieldTower

L95 ↗
TameAbhyankar.SGA1.topNormalizationToFractionFieldTower
Source context 20 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E
instance

lowerNormalizationToTopFieldTower

L99 ↗
TameAbhyankar.SGA1.lowerNormalizationToTopFieldTower
Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E
instance

baseNormalizationToTopFieldTower

L103 ↗
TameAbhyankar.SGA1.baseNormalizationToTopFieldTower
Source context 22 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E
instance

normalizationToTopFieldTower

L110 ↗
TameAbhyankar.SGA1.normalizationToTopFieldTower
Source context 23 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
Lean source · statement
instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E
instance

topOverLowerNormalization

L116 ↗
TameAbhyankar.SGA1.topOverLowerNormalization
Source context 24 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
Lean source · statement
instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E
instance

topOverLowerIntegral

L122 ↗
TameAbhyankar.SGA1.topOverLowerIntegral
Source context 25 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
Lean source · statement
instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E)
instance

normalizationLowerPrime_isMaximal

L128 ↗
TameAbhyankar.SGA1.normalizationLowerPrime_isMaximal
Source context 26 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
Lean source · statement
instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

normalizationBasePrime_isMaximal

L137 ↗
TameAbhyankar.SGA1.normalizationBasePrime_isMaximal
Source context 27 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
Lean source · statement
instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

topNormalizationAction

L146 ↗
TameAbhyankar.SGA1.topNormalizationAction
Source context 28 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
Lean source · statement
instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E)
instance

lowerNormalizationAction

L150 ↗
TameAbhyankar.SGA1.lowerNormalizationAction
Source context 29 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
Lean source · statement
instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M)
def

normalizationRestrictionHom

L155 ↗
TameAbhyankar.SGA1.normalizationRestrictionHom
Documentation

Restriction from the top Galois group to the normal intermediate field.

Source context 30 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
def normalizationRestrictionHom : Gal(E/K) →* Gal(M/K)
theorem

normalizationMap_smul_restriction

L161 ↗
TameAbhyankar.SGA1.normalizationMap_smul_restriction
Documentation

The normalization map is equivariant for restriction of Galois automorphisms.

Source context 31 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
omit [IsDedekindDomain V] [FiniteDimensional K E] in
Lean source · statement
theorem normalizationMap_smul_restriction
    (sigma : Gal(E/K)) (x : integralClosure V M) :
    normalizationMap (V := V) (K := K) (E := E) M
        (normalizationRestrictionHom M sigma • x) =
      sigma • normalizationMap (V := V) (K := K) (E := E) M x
def

normalizationInertiaRestriction

L194 ↗
TameAbhyankar.SGA1.normalizationInertiaRestriction
Documentation

Restriction on the inertia groups attached to a top normalization prime and its contraction to the normalization in M.

Source context 30 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
def normalizationInertiaRestriction
    (Q : Ideal (integralClosure V E)) :
    Q.toAddSubgroup.inertia Gal(E/K) →*
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
        Gal(M/K)
theorem

normalizationInertiaRestriction_ker_eq_range_relative

L207 ↗
TameAbhyankar.SGA1.normalizationInertiaRestriction_ker_eq_range_relative
Documentation

For every top normalization prime, the kernel of inertia restriction is the relative inertia group of E / M.

Source context 31 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
omit [IsDedekindDomain V] [FiniteDimensional K E] in
Lean source · statement
theorem normalizationInertiaRestriction_ker_eq_range_relative
    (Q : Ideal (integralClosure V E)) :
    MonoidHom.ker (normalizationInertiaRestriction (V := V) M Q) =
      (idealRelativeInertiaInclusion (Q := Q)
        (normalizationRestrictionHom M)).range
theorem

normalizationInertiaRestriction_surjective

L220 ↗
TameAbhyankar.SGA1.normalizationInertiaRestriction_surjective
Documentation

For every maximal prime of the top normalization, restriction on inertia to its contraction in the normalization in M is surjective, provided the two residue-field steps are separable.

Source context 30 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar
namespace 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 normalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  (normalizationMap (V := V) (K := K) (E := E) M).toRingHom.toAlgebra
local instance normalizationScalarTower :
    IsScalarTower V (integralClosure V M) (integralClosure V E) := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  apply IsIntegralClosure.algebraMap_injective (integralClosure V E) V E
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationLowerPrime_liesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance normalizationBasePrime_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 lowerNormalizationToTopFieldAlgebra :
    Algebra (integralClosure V M) E :=
  ((algebraMap M E).comp
    (algebraMap (integralClosure V M) M)).toAlgebra
local instance lowerNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V M) M :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance topNormalizationToFractionFieldTower :
    IsScalarTower V (integralClosure V E) E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance lowerNormalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) M E :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance baseNormalizationToTopFieldTower :
    IsScalarTower V (integralClosure V M) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change algebraMap V E x = algebraMap M E (algebraMap V M x)
  exact IsScalarTower.algebraMap_apply V M E x
local instance normalizationToTopFieldTower :
    IsScalarTower (integralClosure V M) (integralClosure V E) E := by
  apply IsScalarTower.of_algebraMap_eq
  intro x
  rfl
local instance topOverLowerNormalization :
    IsIntegralClosure (integralClosure V E) (integralClosure V M) E := by
  exact @IsIntegralClosure.tower_top
    V (integralClosure V M) _ _ _ E (integralClosure V E)
    _ _ _ _ _ (baseNormalizationToTopFieldTower (V := V) M) _ _
local instance topOverLowerIntegral :
    Algebra.IsIntegral (integralClosure V M) (integralClosure V E) := by
  exact @IsIntegralClosure.isIntegral_algebra
    (integralClosure V M) (integralClosure V E) E
    _ _ _ _ _ _ _ (normalizationToTopFieldTower (V := V) M)
local instance normalizationLowerPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change (Q.comap
    (algebraMap (integralClosure V M) (integralClosure V E))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap (integralClosure V M) (integralClosure V E))
    (fun x ↦ Algebra.IsIntegral.isIntegral x) Q
local instance normalizationBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal := by
  change ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).comap
    (algebraMap V (integralClosure V M))).IsMaximal
  exact Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
    (algebraMap V (integralClosure V M)) (fun x ↦ Algebra.IsIntegral.isIntegral x)
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
noncomputable local instance topNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance lowerNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
theorem normalizationInertiaRestriction_surjective
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal]
    (hV : ¬ IsField V)
    [Algebra.IsSeparable
      (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) M Q)
      (integralClosure V M ⧸
        normalizationLowerPrime (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)] :
    Function.Surjective (normalizationInertiaRestriction (V := V) M Q)

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