NYLL
Module

ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
24 declarations indexed from sourceView source ↗

Module documentation

Proj Space locally Of Finite Presentation comp of fg of ideal basic Open eq span

Imports15
Imported by1

Declarations

def

toAway

L56 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.toAway
Documentation

The algebra homomorphism sending affine coordinate variables to projective coordinate ratios on chart i.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def toAway : MvPolynomial {k : Fin (n + 1) // k ≠ i} A →ₐ[A]
    HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)
def

bvec

L64 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.bvec
Documentation

The projective coordinate vector with value one at the chosen chart coordinate and an affine variable elsewhere.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def bvec : Fin (n + 1) → MvPolynomial {k : Fin (n + 1) // k ≠ i} A
theorem

bvec_self

L67 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.bvec_self
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem bvec_self : bvec A n i i = 1
theorem

toAway_bvec

L69 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.toAway_bvec
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem toAway_bvec (k : Fin (n + 1)) : toAway A n i (bvec A n i k) = ProjSpace.ratio A n i k
theorem

range_toAway

L75 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.range_toAway
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem range_toAway : Function.Surjective (toAway A n i)
theorem

exists_algEquiv_away

L81 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.exists_algEquiv_away
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem exists_algEquiv_away :
    Nonempty (MvPolynomial {k : Fin (n + 1) // k ≠ i} A ≃ₐ[A]
      HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i))
instance

finitePresentation_away

L97 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.finitePresentation_away
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
instance finitePresentation_away :
    Algebra.FinitePresentation A (HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i))
theorem

finitePresentation_algebraMap_away

L102 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.finitePresentation_algebraMap_away
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartFP
variable (A : Type) [CommRing A] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem finitePresentation_algebraMap_away :
    (algebraMap A (HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i))).FinitePresentation
def

xpow

L115 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.xpow
Documentation

The power of a homogeneous coordinate, bundled in the homogeneous component of its degree.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def xpow (i : Fin (n + 1)) (d : ℕ) : ↥(homogeneousSubmodule (Fin (n + 1)) A d)
def

frac

L121 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.frac
Documentation

The homogeneous fraction with the given numerator and a matching power of the chosen coordinate.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def frac (i : Fin (n + 1)) (d : ℕ) (F : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)
theorem

frac_zero

L129 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.frac_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem frac_zero (i : Fin (n + 1)) (d : ℕ) : frac (A := A) i d 0 = 0
theorem

frac_add

L135 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.frac_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem frac_add (i : Fin (n + 1)) (d : ℕ) (F G : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    frac i d (F + G) = frac i d F + frac i d G
theorem

frac_mul

L142 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.frac_mul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem frac_mul (i : Fin (n + 1)) (e d : ℕ) (G : ↥(homogeneousSubmodule (Fin (n + 1)) A e))
    (F : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    frac i (e + d) ⟨(G : MvPolynomial (Fin (n + 1)) A) * (F : MvPolynomial (Fin (n + 1)) A),
      SetLike.mul_mem_graded G.2 F.2⟩ = frac i e G * frac i d F
def

comp

L153 ↗
K1BSOL.comp
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def _root_.K1BSOL.comp (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) : ↥(homogeneousSubmodule
  (Fin (n + 1)) A d)
theorem

comp_zero

L158 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.comp_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem comp_zero (d : ℕ) : comp (A := A) (n := n) d 0 = 0
theorem

comp_add

L160 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.comp_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem comp_add (d : ℕ) (p q : MvPolynomial (Fin (n + 1)) A) : comp d (p + q) = comp d p + comp d
  q
theorem

coe_decompose

L164 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.coe_decompose
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem coe_decompose (φ : MvPolynomial (Fin (n + 1)) A) (i : ℕ) :
    ((DirectSum.decompose 𝒜 φ) i : MvPolynomial (Fin (n + 1)) A) = homogeneousComponent i φ
theorem

homogeneousComponent_mul_of_mem_right

L168 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.homogeneousComponent_mul_of_mem_right
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
theorem homogeneousComponent_mul_of_mem_right {e : ℕ} (a : MvPolynomial (Fin (n + 1)) A)
    {g : MvPolynomial (Fin (n + 1)) A} (hg : g ∈ homogeneousSubmodule (Fin (n + 1)) A e) (d : ℕ) :
    homogeneousComponent d (a * g) = if e ≤ d then homogeneousComponent (d - e) a * g else 0 := by
  have h := DirectSum.coe_decompose_mul_of_right_mem 𝒜 (a := a) d hg
  simpa only [coe_decompose] using h
theorem

comp_of_mem

L174 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.comp_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
theorem comp_of_mem {e : ℕ} {F : MvPolynomial (Fin (n + 1)) A}
    (hF : F ∈ homogeneousSubmodule (Fin (n + 1)) A e) (d : ℕ) :
    comp d F = if h : d = e then ⟨F, h ▸ hF⟩ else 0 := by
  apply Subtype.ext
  simp only [comp, homogeneousComponent_of_mem hF]
  split_ifs <;> rfl
def

fcHom

L185 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.fcHom
Documentation

The additive map sending a polynomial to the localized fraction of its chosen homogeneous component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
def fcHom (i : Fin (n + 1)) (d : ℕ) :
    MvPolynomial (Fin (n + 1)) A →+ HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i) where
  toFun p := frac i d (comp d p)
  map_zero' := by simp only [comp_zero, frac_zero]
  map_add' p q := by simp only [comp_add, frac_add]
theorem

fcHom_apply

L191 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.fcHom_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fcHom_apply (i : Fin (n + 1)) (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    fcHom (A := A) i d p = frac i d (comp d p)
theorem

fcHom_mul_of_mem

L194 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.fcHom_mul_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
theorem fcHom_mul_of_mem (i : Fin (n + 1)) (d e : ℕ) (a : MvPolynomial (Fin (n + 1)) A)
    {g : MvPolynomial (Fin (n + 1)) A} (hg : g ∈ homogeneousSubmodule (Fin (n + 1)) A e) :
    fcHom (A := A) i d (a * g) = if e ≤ d then fcHom (A := A) i (d - e) a * frac i e ⟨g, hg⟩ else 0
      := by
  rcases Nat.lt_or_ge d e with hde | hed
  · rw [ite_eq_right (not_le.mpr hde), fcHom_apply]
    have h0 : comp d (a * g) = 0 := Subtype.ext (by
      simp only [comp, homogeneousComponent_mul_of_mem_right a hg d, ite_eq_right (not_le.mpr hde),
        Submodule.coe_zero])
    rw [h0, frac_zero]
  · obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le' hed
    rw [ite_eq_left hed, fcHom_apply, fcHom_apply, Nat.add_sub_cancel]
    have h1 : comp (d' + e) (a * g) =
        ⟨(comp d' a : MvPolynomial (Fin (n + 1)) A) * ((⟨g, hg⟩ : ↥(𝒜 e)) : MvPolynomial (Fin (n +
          1)) A),
          SetLike.mul_mem_graded (comp d' a).2 hg⟩ := Subtype.ext (by
      simp only [comp, homogeneousComponent_mul_of_mem_right a hg (d' + e), ite_eq_left hed,
        Nat.add_sub_cancel])
    rw [h1, frac_mul]
theorem

fg_span_chart

L214 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span.K1BSOL.fg_span_chart
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K1BSOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fg_span_chart (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (hfg : I.FG) (i : Fin (n + 1)) :
    (Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d),
          F ∈ I ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                  den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) }).FG
theorem

locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span

L307 ↗
AlgebraicGeometry.ProjSpace.locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open MvPolynomial CategoryTheory CategoryTheory.Limits
attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] K1BSOL.finitePresentation_away
open _root_.AlgebraicCurves.Geometry.Projective.Proofs in
open ProjSpace_locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span in
open K1BSOL in
Lean source · statement
theorem ProjSpace.locallyOfFinitePresentation_comp_of_fg_of_ideal_basicOpen_eq_span
    (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (hfg : I.FG)
    (𝓘 : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).IdealSheafData)
    (h𝓘 : ∀ i : Fin (n + 1),
        𝓘.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i),
          Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i)
            (ProjSpace.X_mem_one A n i) one_pos⟩ =
        Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d),
          F ∈ I ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                  den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) }) :
    LocallyOfFinitePresentation (𝓘.subschemeι ≫ ProjSpace.π A n)

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