NYLL
Module

IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
18 declarations indexed from sourceView source ↗

Module documentation

Is Integrally Closed integral Closure eq adjoin root X pow sub C of is Unit

Imports3
Imported by2

Declarations

theorem

mem_range_includeLeft_of_isIntegral

L34 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.mem_range_includeLeft_of_isIntegral
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
omit [IsDomain A] in
Lean source · statement
theorem mem_range_includeLeft_of_isIntegral {S : Type*} [CommRing S] [Algebra A S] [Algebra.Smooth
  A S]
    (y : S ⊗[A] K) (hy : IsIntegral S y) :
    y ∈ (Algebra.TensorProduct.includeLeftRingHom : S →+* S ⊗[A] K).range
abbrev

fA

L64 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.fA
Documentation

The Kummer polynomial X ^ n - C u over the original ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
Lean source · statement
abbrev fA (n : ℕ) (u : A) : A[X]
abbrev

fK

L67 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.fK
Documentation

The Kummer polynomial after extending coefficients to the fraction field.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
Lean source · statement
abbrev fK (n : ℕ) (u : A) : K[X]
theorem

root_fK_pow

L72 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.root_fK_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem root_fK_pow (n : ℕ) (u : A) :
    (AdjoinRoot.root (fK K n u)) ^ n = algebraMap A (AdjoinRoot (fK K n u)) u
theorem

root_fA_pow

L81 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.root_fA_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] in
Lean source · statement
theorem root_fA_pow (n : ℕ) (u : A) :
    (AdjoinRoot.root (fA n u)) ^ n = algebraMap A (AdjoinRoot (fA n u)) u
def

ψ₁

L90 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψ₁
Documentation

The map of Kummer root algebras induced by extending the coefficient ring.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
def ψ₁ (n : ℕ) (u : A) : AdjoinRoot (fA n u) →ₐ[A] AdjoinRoot (fK K n u)
theorem

ψ₁_root

L97 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψ₁_root
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem ψ₁_root (n : ℕ) (u : A) : ψ₁ (K := K) n u (AdjoinRoot.root (fA n u)) = AdjoinRoot.root (fK
  K n u)
def

ψ

L102 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψ
Documentation

The scalar extension map from the original Kummer algebra to the root algebra over K.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
def ψ (n : ℕ) (u : A) : AdjoinRoot (fA n u) ⊗[A] K →ₐ[A] AdjoinRoot (fK K n u)
theorem

ψ_tmul

L107 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψ_tmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem ψ_tmul (n : ℕ) (u : A) (s : AdjoinRoot (fA n u)) (k : K) :
    ψ n u (s ⊗ₜ[A] k) = ψ₁ n u s * algebraMap K (AdjoinRoot (fK K n u)) k
def

θ

L112 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.θ
Documentation

The map sending the Kummer root over K to the original root tensored with one.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
def θ (n : ℕ) (u : A) : AdjoinRoot (fK K n u) →+* AdjoinRoot (fA n u) ⊗[A] K
theorem

θ_of

L122 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.θ_of
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem θ_of (n : ℕ) (u : A) (k : K) :
    θ n u (AdjoinRoot.of (fK K n u) k) = (1 : AdjoinRoot (fA n u)) ⊗ₜ[A] k
theorem

θ_root

L127 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.θ_root
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem θ_root (n : ℕ) (u : A) :
    θ n u (AdjoinRoot.root (fK K n u)) = AdjoinRoot.root (fA n u) ⊗ₜ[A] (1 : K)
def

θₐ

L132 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.θₐ
Documentation

The inverse scalar extension map, viewed as an algebra homomorphism over A.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
def θₐ (n : ℕ) (u : A) : AdjoinRoot (fK K n u) →ₐ[A] AdjoinRoot (fA n u) ⊗[A] K
def

ψθ

L144 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψθ
Documentation

The composite of the two scalar extension maps as an endomorphism over K.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
def ψθ (n : ℕ) (u : A) : AdjoinRoot (fK K n u) →ₐ[K] AdjoinRoot (fK K n u)
theorem

ψθ_eq_id

L155 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψθ_eq_id
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem ψθ_eq_id (n : ℕ) (u : A) : ψθ (K := K) n u = AlgHom.id K (AdjoinRoot (fK K n u))
theorem

ψ_θ

L161 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.ψ_θ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
omit [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] in
Lean source · statement
theorem ψ_θ (n : ℕ) (u : A) (x : AdjoinRoot (fK K n u)) : ψ n u (θ n u x) = x
theorem

integralClosure_eq_adjoin

L166 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit.KummerIntegralClosureKa.integralClosure_eq_adjoin
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
namespace KummerIntegralClosureKa
variable {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field K] [Algebra A K] [IsFractionRing A K]
variable (K)
variable {K}
Lean source · statement
theorem integralClosure_eq_adjoin (n : ℕ) (u : A) (hn : IsUnit ((n : ℕ) : A)) (hu : IsUnit u) :
    integralClosure A (AdjoinRoot (fK K n u)) = Algebra.adjoin A {AdjoinRoot.root (fK K n u)}
theorem

integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit

L202 ↗
IsIntegrallyClosed.integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
open Polynomial TensorProduct
open KummerIntegralClosureKa in
Lean source · statement
theorem _root_.IsIntegrallyClosed.integralClosure_eq_adjoin_root_X_pow_sub_C_of_isUnit
    {A K : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    (n : ℕ) (u : A) (hn : IsUnit (n : A)) (hu : IsUnit u) :
    integralClosure A (AdjoinRoot (X ^ n - C (algebraMap A K u) : K[X])) =
      Algebra.adjoin A {AdjoinRoot.root (X ^ n - C (algebraMap A K u) : K[X])}

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