NYLL
Module

Equiv.lean

Nyll.SchemeTheory.Normalization.IntegralClosure.IntegralBase.Equiv
7 declarations indexed from sourceView source ↗

Module documentation

Integral closure after an integral enlargement of the base

If A → B is integral and both rings act compatibly on the same ambient ring L, an element of L is integral over A exactly when it is integral over B. Thus the two literal integral-closure types are canonically equivalent. This is the comparison used when a radical root ring has already been embedded in a chosen normalization factor.

Imports2
  • Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
  • Mathlib.RingTheory.RingHom.Etale
Imported by8

Declarations

def

integralClosureIntegralBaseAlgebra

L34 ↗
EtaleFundamentalGroups.integralClosureIntegralBaseAlgebra
Documentation

The canonical B-algebra structure on the A-integral closure inside L. Integrality of B / A makes the lift land in the integral closure.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · statement
def integralClosureIntegralBaseAlgebra :
    Algebra B (integralClosure A L)
theorem

integralClosureIntegralBase_isScalarTower

L40 ↗
EtaleFundamentalGroups.integralClosureIntegralBase_isScalarTower
Documentation

The canonical lift of B into the A-integral closure is compatible with the original map A → B.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
theorem integralClosureIntegralBase_isScalarTower :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    IsScalarTower A B (integralClosure A L) := by
  let : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  exact IsScalarTower.of_algebraMap_eq fun a ↦
    (IsIntegralClosure.lift A (integralClosure A L) L).commutes a |>.symm
theorem

integralClosureIntegralBase_toAmbient_isScalarTower

L51 ↗
EtaleFundamentalGroups.integralClosureIntegralBase_toAmbient_isScalarTower
Documentation

The canonical lift into the integral closure has the expected composite map to the ambient ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
theorem integralClosureIntegralBase_toAmbient_isScalarTower :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    IsScalarTower B (integralClosure A L) L := by
  let : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  exact IsScalarTower.of_algebraMap_eq fun b ↦
    (IsIntegralClosure.algebraMap_lift A (integralClosure A L) L b).symm
def

integralClosureIntegralBaseAlgEquiv

L62 ↗
EtaleFundamentalGroups.integralClosureIntegralBaseAlgEquiv
Documentation

Enlarging a base integrally does not change its integral closure inside one fixed ambient ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
def integralClosureIntegralBaseAlgEquiv :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    integralClosure B L ≃ₐ[B] integralClosure A L := by
  letI : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  letI : IsScalarTower A B (integralClosure A L) :=
    integralClosureIntegralBase_isScalarTower
  letI : IsScalarTower B (integralClosure A L) L :=
    integralClosureIntegralBase_toAmbient_isScalarTower
  letI : IsIntegralClosure (integralClosure A L) B L :=
    IsIntegralClosure.tower_top (R := A) (A := B) (B := L)
      (C := integralClosure A L)
  exact IsIntegralClosure.equiv B (integralClosure B L) L
    (integralClosure A L)
theorem

moduleFinite_integralClosure_of_integralBase

L80 ↗
EtaleFundamentalGroups.moduleFinite_integralClosure_of_integralBase
Documentation

Module finiteness over the enlarged base is unchanged by writing the same normalization as the integral closure over the original base.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
theorem moduleFinite_integralClosure_of_integralBase
    [Module.Finite B (integralClosure B L)] :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    Module.Finite B (integralClosure A L) := by
  let : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  exact Module.Finite.equiv
    integralClosureIntegralBaseAlgEquiv.toLinearEquiv
theorem

integralClosure_etale_of_integralBase

L92 ↗
EtaleFundamentalGroups.integralClosure_etale_of_integralBase
Documentation

Etaleness over the enlarged integral base transports to the same normalization written as the integral closure over the original base.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
theorem integralClosure_etale_of_integralBase
    (hEtale : Algebra.Etale B (integralClosure B L)) :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    Algebra.Etale B (integralClosure A L) := by
  let : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  let : Algebra.Etale B (integralClosure B L) := hEtale
  exact Algebra.Etale.of_equiv integralClosureIntegralBaseAlgEquiv
theorem

algebraMap_integralClosureIntegralBaseAlgEquiv

L105 ↗
EtaleFundamentalGroups.algebraMap_integralClosureIntegralBaseAlgEquiv
Documentation

The preceding equivalence is the identity after coercion to the common ambient ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uB uL
variable {A : Type uA} {B : Type uB} {L : Type uL}
variable [CommRing A] [CommRing B] [CommRing L]
variable [Algebra A B] [Algebra A L] [Algebra B L]
variable [IsScalarTower A B L] [Algebra.IsIntegral A B]
Lean source · full declaration
theorem algebraMap_integralClosureIntegralBaseAlgEquiv
    (x : integralClosure B L) :
    letI : Algebra B (integralClosure A L) :=
      integralClosureIntegralBaseAlgebra
    algebraMap (integralClosure A L) L
        (integralClosureIntegralBaseAlgEquiv x) =
      algebraMap (integralClosure B L) L x := by
  let : Algebra B (integralClosure A L) :=
    integralClosureIntegralBaseAlgebra
  let : IsScalarTower A B (integralClosure A L) :=
    integralClosureIntegralBase_isScalarTower
  let : IsScalarTower B (integralClosure A L) L :=
    integralClosureIntegralBase_toAmbient_isScalarTower
  let : IsIntegralClosure (integralClosure A L) B L :=
    IsIntegralClosure.tower_top (R := A) (A := B) (B := L)
      (C := integralClosure A L)
  exact IsIntegralClosure.algebraMap_equiv B (integralClosure B L) L
    (integralClosure A L) x

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