NYLL
Module

free_piece_of_isLocalRing_of_forall_relation_mem_span.lean

Nyll.AlgebraicCurves.Hilbert.free_piece_of_isLocalRing_of_forall_relation_mem_span
42 declarations indexed from sourceView source ↗

Module documentation

free piece of is Local Ring of forall relation mem span

Imports14
Imported by1

Declarations

theorem

finite_homogeneousSubmodule

L50 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.finite_homogeneousSubmodule
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem finite_homogeneousSubmodule (A : Type) [CommRing A] (d : ℕ) :
    Module.Finite A ↥(homogeneousSubmodule (Fin (n + 1)) A d)
theorem

free_homogeneousSubmodule

L58 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.free_homogeneousSubmodule
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem free_homogeneousSubmodule (A : Type) [CommRing A] (d : ℕ) :
    Module.Free A ↥(homogeneousSubmodule (Fin (n + 1)) A d)
theorem

decompose_eq

L64 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.decompose_eq
Source context 10 commands

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

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

proj

L70 ↗
GotzLocalLift.proj
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
def _root_.GotzLocalLift.proj (A : Type) [CommRing A] (d : ℕ) :
    MvPolynomial (Fin (n + 1)) A →ₗ[A] ↥(homogeneousSubmodule (Fin (n + 1)) A d)
theorem

proj_apply_coe

L77 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.proj_apply_coe
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem proj_apply_coe (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    (proj A d p : MvPolynomial (Fin (n + 1)) A) = homogeneousComponent d p
theorem

proj_of_mem

L80 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.proj_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem proj_of_mem (d : ℕ) (p : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    proj A d (p : MvPolynomial (Fin (n + 1)) A) = p
theorem

homogeneousComponent_mul_add

L85 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.homogeneousComponent_mul_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem homogeneousComponent_mul_add {F : MvPolynomial (Fin (n + 1)) A} {m : ℕ} (hF :
  F.IsHomogeneous m)
    (a : MvPolynomial (Fin (n + 1)) A) (d : ℕ) :
    homogeneousComponent (m + d) (a * F) = homogeneousComponent d a * F
theorem

homogeneousComponent_mul_of_lt

L94 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.homogeneousComponent_mul_of_lt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem homogeneousComponent_mul_of_lt {F : MvPolynomial (Fin (n + 1)) A} {m : ℕ} (hF :
  F.IsHomogeneous m)
    (a : MvPolynomial (Fin (n + 1)) A) {e : ℕ} (he : e < m) :
    homogeneousComponent e (a * F) = 0
theorem

map_homogeneousComponent

L104 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.map_homogeneousComponent
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Pieces
variable {A : Type} [CommRing A]
Lean source · statement
theorem map_homogeneousComponent {B : Type} [CommRing B] (f : A →+* B) (d : ℕ)
    (p : MvPolynomial (Fin (n + 1)) A) :
    MvPolynomial.map f (homogeneousComponent d p) = homogeneousComponent d (MvPolynomial.map f p)
theorem

mem_span_iff

L119 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.mem_span_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
Lean source · statement
theorem mem_span_iff (u : MvPolynomial (Fin (n + 1)) A) :
    u ∈ Ideal.span (Set.range F) ↔ ∃ a : Fin g → MvPolynomial (Fin (n + 1)) A, ∑ i, a i * F i = u
theorem

sum_mul_mem

L123 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.sum_mul_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
Lean source · statement
theorem sum_mul_mem (a : Fin g → MvPolynomial (Fin (n + 1)) A) :
    ∑ i, a i * F i ∈ Ideal.span (Set.range F)
theorem

homogeneousComponent_sum_mul_add

L128 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.homogeneousComponent_sum_mul_add
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem homogeneousComponent_sum_mul_add (a : Fin g → MvPolynomial (Fin (n + 1)) A) (d : ℕ) :
    homogeneousComponent (m + d) (∑ i, a i * F i) = ∑ i, homogeneousComponent d (a i) * F i
theorem

homogeneousComponent_sum_mul_of_lt

L133 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.homogeneousComponent_sum_mul_of_lt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem homogeneousComponent_sum_mul_of_lt (a : Fin g → MvPolynomial (Fin (n + 1)) A) {e : ℕ} (he :
  e < m) :
    homogeneousComponent e (∑ i, a i * F i) = 0
theorem

isHomogeneous_sum_mul

L139 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.isHomogeneous_sum_mul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem isHomogeneous_sum_mul (a : Fin g → MvPolynomial (Fin (n + 1)) A) (d : ℕ)
    (ha : ∀ i, (a i).IsHomogeneous d) : (∑ i, a i * F i).IsHomogeneous (m + d)
theorem

exists_eq_sum_of_mem

L144 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.exists_eq_sum_of_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem exists_eq_sum_of_mem (u : MvPolynomial (Fin (n + 1)) A) (hu : u ∈ Ideal.span (Set.range F))
  (d : ℕ)
    (hud : u.IsHomogeneous (m + d)) :
    ∃ a : Fin g → MvPolynomial (Fin (n + 1)) A, (∀ i, (a i).IsHomogeneous d) ∧ ∑ i, a i * F i = u
theorem

eq_zero_of_mem_of_lt

L157 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.eq_zero_of_mem_of_lt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem eq_zero_of_mem_of_lt (u : MvPolynomial (Fin (n + 1)) A) (hu : u ∈ Ideal.span (Set.range F))
  {e : ℕ}
    (he : e < m) (hue : u.IsHomogeneous e) : u = 0
theorem

homogeneousComponent_mem_span

L166 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.homogeneousComponent_mem_span
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section SpanF
variable {A : Type} [CommRing A] {g m : ℕ}
  (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem homogeneousComponent_mem_span {u : MvPolynomial (Fin (n + 1)) A} (hu : u ∈ Ideal.span
  (Set.range F))
    (e : ℕ) : homogeneousComponent e u ∈ Ideal.span (Set.range F)
def

InM

L181 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM
Documentation

The condition that every polynomial coefficient lies in the maximal ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
def InM (p : MvPolynomial (Fin (n + 1)) A) : Prop
theorem

inM_iff_map_eq_zero

L183 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.inM_iff_map_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem inM_iff_map_eq_zero (p : MvPolynomial (Fin (n + 1)) A) :
    InM p ↔ MvPolynomial.map (IsLocalRing.residue A) p = 0
theorem

inM_iff_mem_smul_top

L188 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.inM_iff_mem_smul_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem inM_iff_mem_smul_top (p : MvPolynomial (Fin (n + 1)) A) :
    InM p ↔ p ∈ IsLocalRing.maximalIdeal A • (⊤ : Submodule A (MvPolynomial (Fin (n + 1)) A))
theorem

zero

L194 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.zero : InM (0 : MvPolynomial (Fin (n + 1)) A)
theorem

add

L196 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.add {p q : MvPolynomial (Fin (n + 1)) A} (hp : InM p) (hq : InM q) : InM (p + q)
theorem

sub

L200 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.sub
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.sub {p q : MvPolynomial (Fin (n + 1)) A} (hp : InM p) (hq : InM q) : InM (p - q)
theorem

mul_left

L204 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.mul_left
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.mul_left {p : MvPolynomial (Fin (n + 1)) A} (q : MvPolynomial (Fin (n + 1)) A) (hp :
  InM p) :
    InM (q * p)
theorem

smul

L210 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.smul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.smul {p : MvPolynomial (Fin (n + 1)) A} (a : A) (hp : InM p) : InM (a • p)
theorem

inM_smul_of_mem

L213 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.inM_smul_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem inM_smul_of_mem {a : A} (ha : a ∈ IsLocalRing.maximalIdeal A) (p : MvPolynomial (Fin (n +
  1)) A) :
    InM (a • p)
theorem

sum

L219 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.sum
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.sum {ι : Type} (s : Finset ι) {p : ι → MvPolynomial (Fin (n + 1)) A} (hp : ∀ i ∈ s, InM
  (p i)) :
    InM (∑ i ∈ s, p i)
theorem

homogeneousComponent

L225 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.InM.homogeneousComponent
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem InM.homogeneousComponent {p : MvPolynomial (Fin (n + 1)) A} (hp : InM p) (d : ℕ) :
    InM (homogeneousComponent d p)
theorem

inM_of_mem_smul

L232 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.inM_of_mem_smul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem inM_of_mem_smul (N : Submodule A (MvPolynomial (Fin (n + 1)) A)) {p : MvPolynomial (Fin (n
  + 1)) A}
    (hp : p ∈ IsLocalRing.maximalIdeal A • N) : InM p
theorem

mem_smul_top_of_inM

L237 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.mem_smul_top_of_inM
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem mem_smul_top_of_inM {e : ℕ} (p : ↥(homogeneousSubmodule (Fin (n + 1)) A e))
    (hp : InM (p : MvPolynomial (Fin (n + 1)) A)) :
    p ∈ IsLocalRing.maximalIdeal A • (⊤ : Submodule A ↥(homogeneousSubmodule (Fin (n + 1)) A e))
theorem

inM_of_mem_smul_top

L249 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.inM_of_mem_smul_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem inM_of_mem_smul_top {e : ℕ} (p : ↥(homogeneousSubmodule (Fin (n + 1)) A e))
    (hp : p ∈ IsLocalRing.maximalIdeal A • (⊤ : Submodule A ↥(homogeneousSubmodule (Fin (n + 1)) A
      e))) :
    InM (p : MvPolynomial (Fin (n + 1)) A)
theorem

one_tmul_eq_zero_iff

L257 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.one_tmul_eq_zero_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem one_tmul_eq_zero_iff {V : Type} [AddCommGroup V] [Module A V] (v : V) :
    (1 : IsLocalRing.ResidueField A) ⊗ₜ[A] v = 0 ↔ v ∈ IsLocalRing.maximalIdeal A • (⊤ : Submodule
      A V)
def

Lifts

L268 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.Lifts
Documentation

Lifting of homogeneous relations to coefficients lying in the maximal ideal.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
Lean source · statement
def Lifts (d : ℕ) : Prop
theorem

exists_eq_sum_of_mem_smul

L272 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.exists_eq_sum_of_mem_smul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
Lean source · statement
theorem exists_eq_sum_of_mem_smul {y : MvPolynomial (Fin (n + 1)) A}
    (hy : y ∈ IsLocalRing.maximalIdeal A • (Ideal.span (Set.range F)).restrictScalars A) :
    ∃ μ : Fin g → MvPolynomial (Fin (n + 1)) A, (∀ i, InM (μ i)) ∧ y = ∑ i, μ i * F i
theorem

lifts_of_projective

L289 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.lifts_of_projective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem lifts_of_projective (d : ℕ) (hproj : Module.Projective A (piece (Ideal.span (Set.range F))
  (m + d))) :
    Lifts F d
theorem

lifts_of_forall_relation

L340 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.lifts_of_forall_relation
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
omit hF in
Lean source · statement
theorem lifts_of_forall_relation (h0 : Lifts F 0) (h1 : Lifts F 1)
    (hrel : ∀ (d : ℕ) (c : Fin g → MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A)),
      (∀ i, (c i).IsHomogeneous d) →
      ∑ i, c i * MvPolynomial.map (IsLocalRing.residue A) (F i) = 0 →
      c ∈ Submodule.span (MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A))
        {l : Fin g → MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A) |
          (∃ d' ≤ 1, ∀ i, (l i).IsHomogeneous d') ∧
          ∑ i, l i * MvPolynomial.map (IsLocalRing.residue A) (F i) = 0})
    (d : ℕ) : Lifts F d
def

presMap

L414 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.presMap
Documentation

The homogeneous presentation map that multiplies coefficient polynomials by the selected generators.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
def presMap (d : ℕ) :
    (Fin g → ↥(homogeneousSubmodule (Fin (n + 1)) A d)) →ₗ[A] ↥(homogeneousSubmodule (Fin (n + 1))
      A (m + d))
theorem

presMap_apply_coe

L429 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.presMap_apply_coe
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
omit [IsLocalRing A] in
Lean source · statement
theorem presMap_apply_coe (d : ℕ) (a : Fin g → ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    (presMap F hF d a : MvPolynomial (Fin (n + 1)) A) = ∑ i, (a i : MvPolynomial (Fin (n + 1)) A) *
      F i
theorem

range_presMap

L434 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.range_presMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
omit [IsLocalRing A] in
Lean source · statement
theorem range_presMap (d : ℕ) :
    LinearMap.range (presMap F hF d) =
      Submodule.comap (homogeneousSubmodule (Fin (n + 1)) A (m + d)).subtype
        ((Ideal.span (Set.range F)).restrictScalars A)
theorem

free_piece_add

L451 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.free_piece_add
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
Lean source · statement
theorem free_piece_add (d : ℕ) (hL : Lifts F d) : Module.Free A (piece (Ideal.span (Set.range F))
  (m + d))
theorem

free_piece_of_lt

L504 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertLocalRelations.GotzLocalLift.free_piece_of_lt
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace GotzLocalLift
variable {n : ℕ}
section Local
variable {A : Type} [CommRing A] [IsLocalRing A]
variable {g m : ℕ} (F : Fin g → MvPolynomial (Fin (n + 1)) A)
variable (hF : ∀ i, (F i).IsHomogeneous m)
include hF
omit [IsLocalRing A] hF in
Lean source · statement
theorem free_piece_of_lt (hF : ∀ i, (F i).IsHomogeneous m) {e : ℕ} (he : e < m) :
    Module.Free A (piece (Ideal.span (Set.range F)) e)
theorem

free_piece_of_isLocalRing_of_forall_relation_mem_span

L528 ↗
AlgebraicGeometry.HilbertFunctor.free_piece_of_isLocalRing_of_forall_relation_mem_span
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace HilbertLocalRelations
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local simp] GotzLocalLift.proj_apply_coe
open _root_.AlgebraicCurves.Hilbert.Proofs in
open HilbertLocalRelations.GotzLocalLift in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.HilbertFunctor.free_piece_of_isLocalRing_of_forall_relation_mem_span
    (n m g : ℕ) (A : Type) [CommRing A] [IsLocalRing A]
    (F : Fin g → MvPolynomial (Fin (n + 1)) A) (hF : ∀ i, (F i).IsHomogeneous m)
    (h₀ : Module.Projective A (piece (Ideal.span (Set.range F)) m))
    (h₁ : Module.Projective A (piece (Ideal.span (Set.range F)) (m + 1)))
    (hrel : ∀ (d : ℕ) (c : Fin g → MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A)),
      (∀ i, (c i).IsHomogeneous d) →
      ∑ i, c i * MvPolynomial.map (IsLocalRing.residue A) (F i) = 0 →
      c ∈ Submodule.span (MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A))
        {l : Fin g → MvPolynomial (Fin (n + 1)) (IsLocalRing.ResidueField A) |
          (∃ d' ≤ 1, ∀ i, (l i).IsHomogeneous d') ∧
          ∑ i, l i * MvPolynomial.map (IsLocalRing.residue A) (F i) = 0}) :
    ∀ e, Module.Free A (piece (Ideal.span (Set.range F)) e)

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