NYLL
Module

IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.lean

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

Module documentation

Is Integrally Closed integral Closure eq adjoin and etale and finite of eq mul pow

Imports2
Imported by3

Declarations

abbrev

fv

L34 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.fv
Documentation

The Kummer polynomial after extension 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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
abbrev fv (k : ℕ) (v : B) : F[X]
abbrev

fB

L37 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.fB
Documentation

The Kummer polynomial over the base 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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
abbrev fB (k : ℕ) (v : B) : B[X]
abbrev

fg

L40 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.fg
Documentation

The Kummer polynomial with a coefficient in 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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
abbrev fg (k : ℕ) (g : F) : F[X]
theorem

root_fv_pow

L43 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.root_fv_pow
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem root_fv_pow (k : ℕ) (v : B) :
    (AdjoinRoot.root (fv F k v)) ^ k = algebraMap F (AdjoinRoot (fv F k v)) (algebraMap B F v)
theorem

root_fg_pow

L50 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.root_fg_pow
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
theorem root_fg_pow (k : ℕ) (g : F) :
    (AdjoinRoot.root (fg k g)) ^ k = algebraMap F (AdjoinRoot (fg k g)) g
def

ψ₁

L58 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.ψ₁
Documentation

The coefficient extension map between the two root algebras.

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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
def ψ₁ (k : ℕ) (v : B) : AdjoinRoot (fB k v) →ₐ[B] AdjoinRoot (fv F k v)
theorem

ψ₁_root

L66 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.ψ₁_root
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem ψ₁_root (k : ℕ) (v : B) : ψ₁ (F := F) k v (AdjoinRoot.root (fB k v)) = AdjoinRoot.root (fv
  F k v)
theorem

ψ₁_mk

L71 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.ψ₁_mk
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem ψ₁_mk (k : ℕ) (v : B) (p : B[X]) :
    ψ₁ (F := F) k v (AdjoinRoot.mk (fB k v) p) = AdjoinRoot.mk (fv F k v) (p.map (algebraMap B F))
theorem

ψ₁_injective

L78 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.ψ₁_injective
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
omit [IsIntegrallyClosed B] in
Lean source · statement
theorem ψ₁_injective (k : ℕ) (v : B) (hk0 : k ≠ 0) : Function.Injective (ψ₁ (F := F) k v)
theorem

ψ₁_range

L104 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.ψ₁_range
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem ψ₁_range (k : ℕ) (v : B) :
    (ψ₁ (F := F) k v).range = Algebra.adjoin B {AdjoinRoot.root (fv F k v)}
def

α

L114 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.α
Documentation

Rescale the root by the inverse of the twisting parameter.

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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
Lean source · statement
def α (hh : h ≠ 0) (hg : g = algebraMap B F v * h ^ k) :
    AdjoinRoot (fv F k v) →ₐ[F] AdjoinRoot (fg k g)
def

β

L126 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.β
Documentation

Rescale the root by the twisting parameter.

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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
Lean source · statement
def β (hg : g = algebraMap B F v * h ^ k) :
    AdjoinRoot (fg k g) →ₐ[F] AdjoinRoot (fv F k v)
theorem

α_root

L135 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.α_root
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem α_root (hh : h ≠ 0) (hg : g = algebraMap B F v * h ^ k) :
    α k v h g hh hg (AdjoinRoot.root (fv F k v)) =
      algebraMap F (AdjoinRoot (fg k g)) h⁻¹ * AdjoinRoot.root (fg k g)
theorem

β_root

L141 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.β_root
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem β_root (hg : g = algebraMap B F v * h ^ k) :
    β k v h g hg (AdjoinRoot.root (fg k g)) =
      algebraMap F (AdjoinRoot (fv F k v)) h * AdjoinRoot.root (fv F k v)
def

τ

L147 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.τ
Documentation

The root algebra equivalence induced by rescaling the 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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
Lean source · statement
def τ (hh : h ≠ 0) (hg : g = algebraMap B F v * h ^ k) :
    AdjoinRoot (fv F k v) ≃ₐ[F] AdjoinRoot (fg k g)
theorem

τ_root

L160 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.τ_root
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
section Twist
variable (k : ℕ) (v : B) (h : F) (g : F)
omit [IsDomain B] [IsIntegrallyClosed B] [IsFractionRing B F] in
Lean source · statement
theorem τ_root (hh : h ≠ 0) (hg : g = algebraMap B F v * h ^ k) :
    τ k v h g hh hg (AdjoinRoot.root (fv F k v)) =
      algebraMap F (AdjoinRoot (fg k g)) h⁻¹ * AdjoinRoot.root (fg k g)
theorem

main

L167 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow.KummerLocalKb.main
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_and_etale_and_finite_of_eq_mul_pow
open Polynomial
namespace KummerLocalKb
variable {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
  [Field F] [Algebra B F] [IsFractionRing B F]
variable (F) in
Lean source · statement
theorem main (k : ℕ) (hk : IsUnit ((k : ℕ) : B)) (v : B) (hv : IsUnit v) (h : F) (hh : h ≠ 0) (g :
  F)
    (hg : g = algebraMap B F v * h ^ k) :
    integralClosure B (AdjoinRoot (fg k g)) =
        Algebra.adjoin B {algebraMap F (AdjoinRoot (fg k g)) h⁻¹ * AdjoinRoot.root (fg k g)} ∧
      Algebra.Etale B (integralClosure B (AdjoinRoot (fg k g))) ∧
      Module.Finite B (integralClosure B (AdjoinRoot (fg k g)))
theorem

integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow

L207 ↗
IsIntegrallyClosed.integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
open Polynomial
Lean source · statement
theorem _root_.IsIntegrallyClosed.integralClosure_eq_adjoin_and_etale_and_finite_of_eq_mul_pow
    {B F : Type*} [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Field F] [Algebra B F] [IsFractionRing B F]
    (k : ℕ) (hk : IsUnit (k : B)) (v : B) (hv : IsUnit v) (h : F) (hh : h ≠ 0) (g : F)
    (hg : g = algebraMap B F v * h ^ k) :
    integralClosure B (AdjoinRoot (X ^ k - C g : F[X])) =
        Algebra.adjoin B {algebraMap F (AdjoinRoot (X ^ k - C g : F[X])) h⁻¹ * AdjoinRoot.root (X ^
          k - C g : F[X])} ∧
      Algebra.Etale B (integralClosure B (AdjoinRoot (X ^ k - C g : F[X]))) ∧
      Module.Finite B (integralClosure B (AdjoinRoot (X ^ k - C g : F[X])))

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