NYLL
Module

exists_linearEquiv_baseChange_piece_map.lean

Nyll.AlgebraicCurves.Hilbert.exists_linearEquiv_baseChange_piece_map
33 declarations indexed from sourceView source ↗

Module documentation

exists linear Equiv base Change piece map

Imports7
  • Mathlib.RingTheory.MvPolynomial.Homogeneous
  • Mathlib.RingTheory.MvPolynomial.Basic
  • Mathlib.RingTheory.GradedAlgebra.Basic
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.Tactic.SplitIfs
  • Mathlib.Tactic.Conv
  • Nyll.AlgebraicCurves.Hilbert.Functor.Basic
Imported by5

Declarations

theorem

homogeneousComponent_map

L40 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.homogeneousComponent_map
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
omit [Algebra A B] in
Lean source · statement
theorem homogeneousComponent_map (φ : A →+* B) (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    homogeneousComponent d (MvPolynomial.map φ p) = MvPolynomial.map φ (homogeneousComponent d p)
theorem

degree_eq_of_mem_support

L47 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.degree_eq_of_mem_support
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem degree_eq_of_mem_support {R : Type} [CommRing R] {p : MvPolynomial (Fin (n + 1)) R} {d : ℕ}
    (hp : p.IsHomogeneous d) {s : Fin (n + 1) →₀ ℕ} (hs : s ∈ p.support) : s.degree = d
theorem

decompose_eq

L55 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.decompose_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem decompose_eq (q : MvPolynomial (Fin (n + 1)) B) (d : ℕ) :
    (DirectSum.decompose (homogeneousSubmodule (Fin (n + 1)) B) q d : MvPolynomial (Fin (n + 1)) B)
      =
      homogeneousComponent d q
def

T

L63 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.T
Documentation

The span after base change of homogeneous elements of the ideal in the specified degree.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
def T (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (j : ℕ) :
    Submodule B (MvPolynomial (Fin (n + 1)) B)
theorem

map_mem_T

L68 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.map_mem_T
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
theorem map_mem_T {I : Ideal (MvPolynomial (Fin (n + 1)) A)} {j : ℕ} {p : MvPolynomial (Fin (n +
  1)) A}
    (hp : p ∈ I) (hpj : p.IsHomogeneous j) : MvPolynomial.map (algebraMap A B) p ∈ T n A B I j
theorem

mul_mem_T

L73 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.mul_mem_T
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
theorem mul_mem_T (I : Ideal (MvPolynomial (Fin (n + 1)) A)) {i j : ℕ}
    {g : MvPolynomial (Fin (n + 1)) B} (hg : g.IsHomogeneous i)
    {x : MvPolynomial (Fin (n + 1)) B} (hx : x ∈ T n A B I j) : g * x ∈ T n A B I (i + j)
theorem

homogeneousComponent_mem_T

L92 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.homogeneousComponent_mem_T
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
theorem homogeneousComponent_mem_T (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I)
    {q : MvPolynomial (Fin (n + 1)) B} (hq : q ∈ I.map (MvPolynomial.map (algebraMap A B))) (d : ℕ)
      :
    homogeneousComponent d q ∈ T n A B I d
theorem

T_le

L121 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.T_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
theorem T_le (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ) :
    T n A B I d ≤ (I.map (MvPolynomial.map (algebraMap A B))).restrictScalars B
theorem

map_homogeneous

L127 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.map_homogeneous
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
Lean source · statement
theorem map_homogeneous (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) :
    ∀ q ∈ I.map (MvPolynomial.map (algebraMap A B)), ∀ d : ℕ,
      homogeneousComponent d q ∈ I.map (MvPolynomial.map (algebraMap A B))
abbrev

SA

L138 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.SA
Documentation

The homogeneous polynomial submodule over the original base ring in the selected degree.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
abbrev SA : Submodule A (MvPolynomial (Fin (n + 1)) A)
abbrev

SB

L141 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.SB
Documentation

The homogeneous polynomial submodule over the new base ring in the selected degree.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
abbrev SB : Submodule B (MvPolynomial (Fin (n + 1)) B)
abbrev

I'

L144 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.I'
Documentation

The extension of the polynomial ideal along the change of coefficient ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
abbrev I' : Ideal (MvPolynomial (Fin (n + 1)) B)
abbrev

KA

L149 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.KA
Documentation

The degree part of the ideal as a submodule of homogeneous polynomials over the original ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
abbrev KA : Submodule A (SA (n := n) (A := A) d)
abbrev

KB

L153 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.KB
Documentation

The degree part of the extended ideal inside the homogeneous polynomials over the new ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
abbrev KB : Submodule B (SB (n := n) (B := B) d)
def

gd

L157 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.gd
Documentation

The coefficient-change map between homogeneous polynomial submodules.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · full declaration
def gd : SA (n := n) (A := A) d →ₗ[A] SB (n := n) (B := B) d where
  toFun p := ⟨MvPolynomial.map (algebraMap A B) (p : MvPolynomial (Fin (n + 1)) A),
    (show (p : MvPolynomial (Fin (n + 1)) A).IsHomogeneous d from p.2).map (algebraMap A B)⟩
  map_add' p q := by
    ext : 1
    simp
  map_smul' a p := by
    ext : 1
    simp only [RingHom.id_apply, Submodule.coe_smul_of_tower, SetLike.val_smul]
    rw [MvPolynomial.smul_eq_C_mul, map_mul, map_C, Algebra.smul_def, MvPolynomial.algebraMap_apply]
theorem

gd_apply_coe

L168 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.gd_apply_coe
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem gd_apply_coe (p : SA (n := n) (A := A) d) :
    ((gd (B := B) d p : SB (n := n) (B := B) d) : MvPolynomial (Fin (n + 1)) B) =
      MvPolynomial.map (algebraMap A B) (p : MvPolynomial (Fin (n + 1)) A)
def

gbar

L173 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.gbar
Documentation

The induced map between quotient degree pieces under change of coefficients.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def gbar : piece I d →ₗ[A] piece (I' (B := B) I) d
theorem

gbar_mk

L181 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.gbar_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem gbar_mk (p : SA (n := n) (A := A) d) :
    gbar (B := B) I d (Submodule.Quotient.mk p) = Submodule.Quotient.mk (gd (B := B) d p)
def

E

L186 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.E
Documentation

The base-changed map from the tensor product of the original degree piece to the new degree piece.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def E : B ⊗[A] piece I d →ₗ[B] piece (I' (B := B) I) d
theorem

E_tmul

L189 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.E_tmul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem E_tmul (b : B) (p : SA (n := n) (A := A) d) :
    E (B := B) I d (b ⊗ₜ[A] Submodule.Quotient.mk p) = b • Submodule.Quotient.mk (gd (B := B) d p)
def

v

L195 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.v
Documentation

The tensor representing a monomial of the selected degree, and zero for other degrees.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def v : (Fin (n + 1) →₀ ℕ) → B ⊗[A] piece I d
def

Psi'

L202 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi'
Documentation

The linear map from polynomials to the tensor-product degree piece defined on monomials.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def Psi' : MvPolynomial (Fin (n + 1)) B →ₗ[B] B ⊗[A] piece I d
theorem

Psi'_monomial

L205 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi'_monomial
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem Psi'_monomial (s : Fin (n + 1) →₀ ℕ) (b : B) :
    Psi' (B := B) I d (monomial s b) = b • v (B := B) I d s
theorem

Psi'_map

L212 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi'_map
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem Psi'_map (p : MvPolynomial (Fin (n + 1)) A) (hp : p.IsHomogeneous d) :
    Psi' (B := B) I d (MvPolynomial.map (algebraMap A B) p) =
      (1 : B) ⊗ₜ[A] Submodule.Quotient.mk (⟨p, hp⟩ : SA (n := n) (A := A) d)
theorem

Psi'_map_eq_zero

L248 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi'_map_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem Psi'_map_eq_zero (p : MvPolynomial (Fin (n + 1)) A) (hpI : p ∈ I) (hp : p.IsHomogeneous d) :
    Psi' (B := B) I d (MvPolynomial.map (algebraMap A B) p) = 0
theorem

T_le_ker

L256 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.T_le_ker
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem T_le_ker : T n A B I d ≤ LinearMap.ker (Psi' (B := B) I d)
def

Psi

L262 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi
Documentation

The map from the new quotient degree piece back to the tensor-product degree piece.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def Psi (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) :
    piece (I' (B := B) I) d →ₗ[B] B ⊗[A] piece I d
theorem

Psi_mk

L273 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem Psi_mk (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (q : SB (n := n) (B := B) d) :
    Psi (B := B) I d hI (Submodule.Quotient.mk q) = Psi' (B := B) I d (q : MvPolynomial (Fin (n +
      1)) B)
theorem

Psi_E

L278 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.Psi_E
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem Psi_E (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (x : B ⊗[A] piece I d) :
    Psi (B := B) I d hI (E (B := B) I d x) = x
theorem

E_Psi

L287 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.E_Psi
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem E_Psi (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (z : piece (I' (B := B) I) d) :
    E (B := B) I d (Psi (B := B) I d hI z) = z
def

equiv

L324 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.equiv
Documentation

The base-change equivalence for the degree pieces of the homogeneous quotient.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
def equiv (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) :
    B ⊗[A] piece I d ≃ₗ[B] piece (I' (B := B) I) d
theorem

equiv_tmul_mk

L329 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map.HilbPieceBC.equiv_tmul_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbPieceBC
variable {n : ℕ} {A B : Type} [CommRing A] [CommRing B] [Algebra A B]
variable (n A B) in
section Equiv
variable (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (d : ℕ)
Lean source · statement
theorem equiv_tmul_mk (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I)
    (p : MvPolynomial (Fin (n + 1)) A) (hp : p.IsHomogeneous d) :
    equiv (B := B) I d hI ((1 : B) ⊗ₜ[A] Submodule.Quotient.mk ⟨p, hp⟩) =
      Submodule.Quotient.mk ⟨MvPolynomial.map (algebraMap A B) p, hp.map (algebraMap A B)⟩
theorem

exists_linearEquiv_baseChange_piece_map

L344 ↗
AlgebraicGeometry.HilbertFunctor.exists_linearEquiv_baseChange_piece_map
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_linearEquiv_baseChange_piece_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local simp] HilbPieceBC.gd_apply_coe
Lean source · statement
theorem _root_.AlgebraicGeometry.HilbertFunctor.exists_linearEquiv_baseChange_piece_map
    (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B]
    (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) :
    (∀ q ∈ I.map (MvPolynomial.map (algebraMap A B)), ∀ d : ℕ,
        homogeneousComponent d q ∈ I.map (MvPolynomial.map (algebraMap A B))) ∧
    ∀ d : ℕ, ∃ e : B ⊗[A] piece I d ≃ₗ[B] piece (I.map (MvPolynomial.map (algebraMap A B))) d,
      ∀ (p : MvPolynomial (Fin (n + 1)) A) (hp : p.IsHomogeneous d),
        e (1 ⊗ₜ[A] Submodule.Quotient.mk ⟨p, hp⟩) =
          Submodule.Quotient.mk ⟨MvPolynomial.map (algebraMap A B) p, hp.map (algebraMap A B)⟩

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