NYLL
Module

Compositum.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Normalization.Compositum
14 declarations indexed from sourceView source ↗

Module documentation

Abhyankar's cyclic argument for normalization rings

This file combines the two restriction maps from a compositum with the ideal-theoretic cyclic projection argument. The resulting relative inertia group is trivial, and hence the right normalization is unramified in the top normalization at every chosen maximal prime.

Imports4
Imported by2

Declarations

instance

leftNormalizationAlgebra

L44 ↗
TameAbhyankar.SGA1.leftNormalizationAlgebra
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
Lean source · statement
instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E)
instance

rightNormalizationAlgebra

L48 ↗
TameAbhyankar.SGA1.rightNormalizationAlgebra
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
Lean source · statement
instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E)
instance

leftPrime_liesOver

L52 ↗
TameAbhyankar.SGA1.leftPrime_liesOver
Source context 17 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable (M N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
Lean source · statement
instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q)
instance

rightPrime_liesOver

L57 ↗
TameAbhyankar.SGA1.rightPrime_liesOver
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
Lean source · statement
instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q)
instance

leftBasePrime_liesOver

L62 ↗
TameAbhyankar.SGA1.leftBasePrime_liesOver
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
Lean source · statement
instance leftBasePrime_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)
instance

rightBasePrime_liesOver

L67 ↗
TameAbhyankar.SGA1.rightBasePrime_liesOver
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
Lean source · statement
instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q)
instance

leftPrime_isMaximal

L72 ↗
TameAbhyankar.SGA1.leftPrime_isMaximal
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
Lean source · statement
instance leftPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

rightPrime_isMaximal

L77 ↗
TameAbhyankar.SGA1.rightPrime_isMaximal
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal
instance

leftBasePrime_isMaximal

L82 ↗
TameAbhyankar.SGA1.leftBasePrime_isMaximal
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
Lean source · statement
instance leftBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

rightBasePrime_isMaximal

L87 ↗
TameAbhyankar.SGA1.rightBasePrime_isMaximal
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance leftBasePrime_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 rightBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal
instance

compositumTopNormalizationAction

L92 ↗
TameAbhyankar.SGA1.compositumTopNormalizationAction
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance leftBasePrime_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 rightBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
Lean source · statement
instance compositumTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E)
instance

compositumLeftNormalizationAction

L96 ↗
TameAbhyankar.SGA1.compositumLeftNormalizationAction
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance leftBasePrime_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 rightBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance compositumTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
Lean source · statement
instance compositumLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M)
instance

compositumRightNormalizationAction

L100 ↗
TameAbhyankar.SGA1.compositumRightNormalizationAction
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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance leftBasePrime_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 rightBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance compositumTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance compositumLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
instance compositumRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N)
theorem

normalizationRelativeInertia_card_eq_one_and_isUnramifiedAt

L108 ↗
TameAbhyankar.SGA1.normalizationRelativeInertia_card_eq_one_and_isUnramifiedAt
Documentation

The cyclic step of Abhyankar's lemma for the normalizations in two normal subextensions which generate the top field. Separability of the four residue-field steps supplies both restriction surjections. Thus no surjectivity or joint-injectivity hypothesis remains in the statement.

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 N : IntermediateField K E)
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
section GaloisCompositum
variable [IsDedekindDomain V]
variable [FiniteDimensional K E] [IsGalois K E]
variable [IsGalois K M] [IsGalois K N]
local instance leftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance rightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance leftPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) :=
  normalizationLowerPrime_liesOver (V := V) M Q
local instance rightPrime_liesOver (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) :=
  normalizationLowerPrime_liesOver (V := V) N Q
local instance leftBasePrime_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) :=
  normalizationBasePrime_liesOver (V := V) M Q
local instance rightBasePrime_liesOver (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) :=
  normalizationBasePrime_liesOver (V := V) N Q
local instance leftPrime_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 rightPrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance leftBasePrime_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 rightBasePrime_isMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance compositumTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance compositumLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance compositumRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
Lean source · statement
theorem normalizationRelativeInertia_card_eq_one_and_isUnramifiedAt
    (hsup : M ⊔ N = ⊤)
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal]
    (hV : ¬ IsField V)
    [IsCyclic (Q.toAddSubgroup.inertia Gal(E/K))]
    [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)]
    [Algebra.IsSeparable
      (V ⧸ normalizationBasePrime (V := V) (K := K) (E := E) N Q)
      (integralClosure V N ⧸
        normalizationLowerPrime (V := V) (K := K) (E := E) N Q)]
    [Algebra.IsSeparable
      (integralClosure V N ⧸
        normalizationLowerPrime (V := V) (K := K) (E := E) N Q)
      (integralClosure V E ⧸ Q)]
    (hcard :
      Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
            Gal(M/K)) ∣
        Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) N Q).toAddSubgroup.inertia
            Gal(N/K))) :
    Nat.card
          (Q.toAddSubgroup.inertia
            (normalizationRestrictionHom N).ker) = 1 ∧
      Algebra.IsUnramifiedAt (integralClosure V N) Q

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