Module

Algebra_levelSet_finite_free_finrank_of_flat_polynomial.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.Algebra_levelSet_finite_free_finrank_of_flat_polynomial

16 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Coordinate level sets of a flat polynomial algebra are finite and free with the prescribed finrank.

Imports2

Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.RingHom.Flat

Imported by2

abbrev

lsIdeal

L44 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.lsIdeal

Documentation

The ideal imposing equality between the two specified coordinate elements in the base- ring tensor product.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

abbrev lsIdeal : Ideal (S ⊗[R] A)

def

fwd

L47 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.fwd

Documentation

The forward map from the base-ring tensor product to the polynomial-ring tensor product.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def fwd : S ⊗[R] A →ₐ[S] S ⊗[R[X]] A

theorem

fwd_tmul

L51 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.fwd_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

theorem fwd_tmul (x : S) (a : A) : fwd R A S (x ⊗ₜ[R] a) = x ⊗ₜ[R[X]] a

theorem

fwd_rel

L55 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.fwd_rel

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)
include hf hs in

Lean source · statement

theorem fwd_rel : fwd R A S ((1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)) = 0

def

fwdQ

L60 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.fwdQ

Documentation

The forward map descended to the quotient by the coordinate level-set relation.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def fwdQ : (S ⊗[R] A ⧸ lsIdeal R A S f s) →ₐ[S] S ⊗[R[X]] A

theorem

fwdQ_mk

L68 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.fwdQ_mk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

theorem fwdQ_mk (t : S ⊗[R] A) :
    fwdQ R A S f s hf hs (Ideal.Quotient.mk _ t) = fwd R A S t

def

bwdA₀

L72 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwdA₀

Documentation

The right inclusion into the coordinate-relation quotient as a base-ring algebra map.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def bwdA₀ : A →ₐ[R] (S ⊗[R] A ⧸ lsIdeal R A S f s)

theorem

bwdA₀_apply

L76 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwdA₀_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)
omit [Algebra R[X] A] [IsScalarTower R R[X] A] [Algebra R[X] S] [IsScalarTower R R[X] S] in

Lean source · statement

theorem bwdA₀_apply (a : A) :
    bwdA₀ R A S f s a = Ideal.Quotient.mk _ ((1 : S) ⊗ₜ[R] a)

theorem

bwdA₀_comp

L79 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwdA₀_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)
include hf hs in

Lean source · statement

theorem bwdA₀_comp :
    (bwdA₀ R A S f s).comp (IsScalarTower.toAlgHom R R[X] A) =
      IsScalarTower.toAlgHom R R[X] (S ⊗[R] A ⧸ lsIdeal R A S f s)

def

bwdA

L91 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwdA

Documentation

The right inclusion into the coordinate-relation quotient as a polynomial-ring algebra map.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def bwdA : A →ₐ[R[X]] (S ⊗[R] A ⧸ lsIdeal R A S f s)

theorem

bwdA_apply

L97 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwdA_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

theorem bwdA_apply (a : A) :
    bwdA R A S f s hf hs a = Ideal.Quotient.mk _ ((1 : S) ⊗ₜ[R] a)

def

bwd

L102 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwd

Documentation

The backward map from the polynomial-ring tensor product to the coordinate-relation quotient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def bwd : S ⊗[R[X]] A →ₐ[S] (S ⊗[R] A ⧸ lsIdeal R A S f s)

theorem

bwd_tmul

L105 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.bwd_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

theorem bwd_tmul (x : S) (a : A) :
    bwd R A S f s hf hs (x ⊗ₜ[R[X]] a) = Ideal.Quotient.mk _ (x ⊗ₜ[R] a)

def

levelSetEquiv

L115 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.levelSetEquiv

Documentation

The algebra equivalence between the coordinate-relation quotient and the polynomial-ring tensor product.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b
section Identification
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  [Algebra R[X] A] [IsScalarTower R R[X] A]
  (S : Type u) [CommRing S] [Algebra R S] [Algebra R[X] S] [IsScalarTower R R[X] S]
  (f : A) (s : S) (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s)

Lean source · statement

def levelSetEquiv : (S ⊗[R] A ⧸ lsIdeal R A S f s) ≃ₐ[S] S ⊗[R[X]] A

theorem

main

L130 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_levelSet_finite_free_finrank_of_flat_polynomial.U4b.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
namespace U4b

Lean source · statement

theorem main
    (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (f : A) (d : ℕ)
    (hfin : (Polynomial.aeval f : R[X] →ₐ[R] A).toRingHom.Finite)
    (hflat : (Polynomial.aeval f : R[X] →ₐ[R] A).toRingHom.Flat)
    (hrank : ∀ (L : Type u) [Field L] [Algebra R L] (x : L),
      Module.finrank L (L ⊗[R] A ⧸ Ideal.span {(1 : L) ⊗ₜ[R] f - x ⊗ₜ[R] (1 : A)}) = d)
    (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] (s : S) :
    Module.Finite S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
      Module.Free S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
      Module.finrank S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) = d

theorem

levelSet_finite_free_finrank_of_flat_polynomial

L188 ↗

Algebra.levelSet_finite_free_finrank_of_flat_polynomial

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_levelSet_finite_free_finrank_of_flat_polynomial
universe u
open _root_.Polynomial
open scoped TensorProduct
open _root_.Polynomial in
open scoped TensorProduct in

Lean source · statement

theorem _root_.Algebra.levelSet_finite_free_finrank_of_flat_polynomial
    (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (f : A) (d : ℕ)
    (hfin : (Polynomial.aeval f : R[X] →ₐ[R] A).toRingHom.Finite)
    (hflat : (Polynomial.aeval f : R[X] →ₐ[R] A).toRingHom.Flat)
    (hrank : ∀ (L : Type u) [Field L] [Algebra R L] (x : L),
      Module.finrank L (L ⊗[R] A ⧸ Ideal.span {(1 : L) ⊗ₜ[R] f - x ⊗ₜ[R] (1 : A)}) = d) :
    ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] (s : S),
      Module.Finite S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.Free S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.finrank S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) = d

Module documentation

Algebra, divisors, and base change

Declarations