NYLL
Module

ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
22 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists is Homogeneous forall x Mul pow apply eq of is Closed Immersion

Imports6
Imported by2

Declarations

def

frac

L47 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frac
Documentation

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

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Frac
variable {k : Type u} [CommRing k] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def frac (d : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) (i :
  Fin (n + 1)) : Away 𝒜 (X i)
theorem

val_frac

L56 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.val_frac
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Frac
variable {k : Type u} [CommRing k] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem val_frac (d : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) (i : Fin (n +
  1)) :
    (frac d p i).val = Localization.mk p.1 (⟨MvPolynomial.X i ^ d, ⟨d, rfl⟩⟩ : Submonoid.powers
      (MvPolynomial.X i))
theorem

frac_add

L61 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frac_add
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Frac
variable {k : Type u} [CommRing k] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem frac_add (d : ℕ) (p q : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) (i : Fin (n
  + 1)) :
    frac d (p + q) i = frac d p i + frac d q i
theorem

frac_smul

L68 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frac_smul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Frac
variable {k : Type u} [CommRing k] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem frac_smul (d : ℕ) (c : k) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) (i :
  Fin (n + 1)) :
    frac d (c • p) i = algebraMap k (Away 𝒜 (X i)) c * frac d p i
theorem

awayMap_frac_eq

L77 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.awayMap_frac_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Frac
variable {k : Type u} [CommRing k] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem awayMap_frac_eq (d : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d)) (i j :
  Fin (n + 1)) :
    awayMap 𝒜 (ProjSpace.X_mem_one k n j) rfl (frac d p i)
      = awayMap 𝒜 (ProjSpace.X_mem_one k n j) rfl (ProjSpace.ratio k n i j) ^ d
          * awayMap 𝒜 (ProjSpace.X_mem_one k n i)
              (mul_comm (X i) (X j) : (X i * X j : MvPolynomial (Fin (n + 1)) k) = X j * X i) (frac
                d p j)
def

pullAway

L104 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway
Documentation

The section on a pulled-back projective chart induced by a homogeneous localization element.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def pullAway (i : Fin (n + 1)) (a : Away 𝒜 (X i)) : Γ(Z, ProjSpace.pullbackChart φ i)
theorem

pullAway_eq

L108 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem pullAway_eq (i : Fin (n + 1)) (a : Away 𝒜 (X i)) :
    pullAway φ i a = (φ.app (Proj.basicOpen 𝒜 (X i))) (Proj.awayToSection 𝒜 (X i) a)
theorem

pullAway_add

L111 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway_add
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem pullAway_add (i : Fin (n + 1)) (a b : Away 𝒜 (X i)) :
    pullAway φ i (a + b) = pullAway φ i a + pullAway φ i b
theorem

pullAway_mul

L115 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway_mul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem pullAway_mul (i : Fin (n + 1)) (a b : Away 𝒜 (X i)) :
    pullAway φ i (a * b) = pullAway φ i a * pullAway φ i b
theorem

pullAway_zero

L119 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem pullAway_zero (i : Fin (n + 1)) : pullAway φ i 0 = 0
theorem

restrictFun_pullAway_left

L122 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.restrictFun_pullAway_left
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem restrictFun_pullAway_left (i j : Fin (n + 1)) (a : Away 𝒜 (X i)) :
    ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_left φ i j) (pullAway φ i a)
      = (φ.app (Proj.basicOpen 𝒜 (X i * X j))).hom
          ((Proj.awayToSection 𝒜 (X i * X j)).hom (awayMap 𝒜 (ProjSpace.X_mem_one k n j) rfl a))
theorem

restrictFun_pullAway_right

L139 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.restrictFun_pullAway_right
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem restrictFun_pullAway_right (i j : Fin (n + 1)) (a : Away 𝒜 (X j)) :
    ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_right φ i j) (pullAway φ j a)
      = (φ.app (Proj.basicOpen 𝒜 (X i * X j))).hom
          ((Proj.awayToSection 𝒜 (X i * X j)).hom (awayMap 𝒜 (ProjSpace.X_mem_one k n i)
            (mul_comm (X i) (X j) : (X i * X j : MvPolynomial (Fin (n + 1)) k) = X j * X i) a))
theorem

restrictFun_pullAway_frac

L157 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.restrictFun_pullAway_frac
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Comp
variable {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
  (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem restrictFun_pullAway_frac (d : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
  d)) (i j : Fin (n + 1)) :
    ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_left φ i j) (pullAway φ i (frac d p i))
      = ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_left φ i j) (ProjSpace.frameUnit φ i j)
        ^ d
          * ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_right φ i j) (pullAway φ j (frac d
            p j))
theorem

frameUnit_eq_pullAway

L181 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frameUnit_eq_pullAway
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem frameUnit_eq_pullAway (i j : Fin (n + 1)) :
    ProjSpace.frameUnit ι i j = pullAway ι i (ProjSpace.ratio A n i j)
theorem

xMul_pow_apply

L184 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.xMul_pow_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem xMul_pow_apply (j : Fin (n + 1)) (k : ℕ) (f : ProjSpace.twistFam (ι ≫ ProjSpace.π A n) ι)
  (d : ℤ) (i : Fin (n + 1)) :
    (((ProjSpace.twistGradedModule ι (ι ≫ ProjSpace.π A n)).xMul j ^ k) f) d i =
      ProjSpace.restrictFun (inf_le_right : (⊤ : Z.Opens) ⊓ ProjSpace.pullbackChart ι i ≤
        ProjSpace.pullbackChart ι i)
        (ProjSpace.frameUnit ι i j) ^ k * f (d - k) i
theorem

exists_eq_pullAway_mk

L205 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.exists_eq_pullAway_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
theorem exists_eq_pullAway_mk [IsClosedImmersion ι] (j : Fin (n + 1)) (z : Γ(Z,
  ProjSpace.pullbackChart ι j)) :
    ∃ (a : ℕ) (G : MvPolynomial (Fin (n + 1)) A) (hG : G ∈ 𝒜 a),
      z = pullAway ι j (Away.mk 𝒜 (ProjSpace.X_mem_one A n j) a G (by simpa using hG)) := by
  have hsurjι : Function.Surjective (ι.app (Proj.basicOpen 𝒜 (X j))) :=
    ι.app_surjective _ (Proj.isAffineOpen_basicOpen 𝒜 (X j) (ProjSpace.X_mem_one A n j) one_pos)
  have hsurjA : Function.Surjective (Proj.awayToSection 𝒜 (X j)).hom := by
    let e := Proj.basicOpenIsoAway 𝒜 (X j) (ProjSpace.X_mem_one A n j) one_pos
    intro s
    refine ⟨e.inv.hom s, ?_⟩
    change (e.inv ≫ e.hom).hom s = s
    rw [e.inv_hom_id]
    rfl
  obtain ⟨s, rfl⟩ := hsurjι z
  obtain ⟨q, rfl⟩ := hsurjA s
  obtain ⟨a, G, hG', rfl⟩ := HomogeneousLocalization.Away.mk_surjective 𝒜 (ProjSpace.X_mem_one A n
    j) q
  exact ⟨a, G, by simpa using hG', rfl⟩
theorem

basicOpen_frameUnit_le

L224 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.basicOpen_frameUnit_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem basicOpen_frameUnit_le (i j : Fin (n + 1)) :
    Z.basicOpen (ProjSpace.frameUnit ι i j) ≤ ProjSpace.pullbackChart ι j
theorem

exists_pow_mul_eq_zero

L265 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.exists_pow_mul_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem exists_pow_mul_eq_zero [IsClosedImmersion ι] (i j : Fin (n + 1)) (δ : Γ(Z,
  ProjSpace.pullbackChart ι i))
    (hδ : ProjSpace.restrictFun (ProjSpace.pullbackOverlap_le_left ι i j) δ = 0) :
    ∃ N : ℕ, ProjSpace.frameUnit ι i j ^ N * δ = 0
theorem

pullAway_pow

L284 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.pullAway_pow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem pullAway_pow (i : Fin (n + 1)) (a : Away 𝒜 (X i)) (N : ℕ) :
    pullAway ι i (a ^ N) = pullAway ι i a ^ N
theorem

frac_congr

L288 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frac_congr
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem frac_congr {d₁ d₂ : ℕ} (h : d₁ = d₂) (p : ↥(𝒜 d₁)) (i : Fin (n + 1)) :
    frac d₁ p i = frac d₂ ⟨p.1, h ▸ p.2⟩ i
theorem

frameUnit_pow_mul_pullAway_frac

L292 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion.SatUnitBody.frameUnit_pow_mul_pullAway_frac
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace SatUnitBody
section Main
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · full declaration
theorem frameUnit_pow_mul_pullAway_frac (i j : Fin (n + 1)) (N d : ℕ) (p : ↥(𝒜 d)) :
    ProjSpace.frameUnit ι i j ^ N * pullAway ι i (frac d p i) =
      pullAway ι i (frac (d + N) ⟨X j ^ N * p.1, by
        have h := SetLike.mul_mem_graded (SetLike.pow_mem_graded N (ProjSpace.X_mem_one A n j)) p.2
        rwa [smul_eq_mul, mul_one, Nat.add_comm N d] at h⟩ i) := by
  rw [frameUnit_eq_pullAway, ← pullAway_pow, ← pullAway_mul]
  congr 1
  apply HomogeneousLocalization.val_injective
  rw [val_mul, val_pow, ProjSpace.ratio, HomogeneousLocalization.Away.val_mk, val_frac, val_frac,
    Localization.mk_pow, Localization.mk_mul, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  refine ⟨1, ?_⟩
  simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow]
  ring
theorem

exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion

L324 ↗
AlgebraicGeometry.ProjSpace.exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
open _root_.MvPolynomial _root_.TensorProduct _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Projective.Proofs in
open ProjSpace_exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion in
open SatUnitBody in
Lean source · statement
theorem ProjSpace.exists_isHomogeneous_forall_xMul_pow_apply_eq_of_isClosedImmersion
    {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsClosedImmersion ι]
    (e : ℕ) (m : ProjSpace.twistFam (ι ≫ ProjSpace.π A n) ι)
    (hm : m ∈ (ProjSpace.twistGradedModule ι (ι ≫ ProjSpace.π A n)).grade (e : ℤ)) (j : Fin (n +
      1)) :
    ∃ (k : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous (e + k)),
      ∀ i : Fin (n + 1),
        (((ProjSpace.twistGradedModule ι (ι ≫ ProjSpace.π A n)).xMul j ^ k) m) ((e + k : ℕ) : ℤ) i =
          ProjSpace.restrictFun
            (inf_le_right : (⊤ : Z.Opens) ⊓ ProjSpace.pullbackChart ι i ≤ ProjSpace.pullbackChart ι
              i)
            ((ι.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)
              (MvPolynomial.X i)))
              (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)
                (MvPolynomial.X i)
                (HomogeneousLocalization.mk
                  { deg := e + k
                    num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule (e + k) F).mpr hF⟩
                    den := ⟨MvPolynomial.X i ^ (e + k), (MvPolynomial.mem_homogeneousSubmodule (e +
                      k) _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i (e + k))⟩
                    den_mem := ⟨e + k, rfl⟩ })))

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