NYLL
Module

ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
16 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists linear Map homogeneous Submodule twist Obj top val eq

Imports3
Imported by9

Declarations

theorem

map_appTop_π_eq_awayToSection_algebraMap

L36 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.map_appTop_π_eq_awayToSection_algebraMap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
Lean source · statement
theorem map_appTop_π_eq_awayToSection_algebraMap (k : Type u) [CommRing k] (n : ℕ) (i : Fin (n +
  1)) (r : k) :
    (Proj (homogeneousSubmodule (Fin (n + 1)) k)).presheaf.map
        (homOfLE (le_top : Proj.basicOpen (homogeneousSubmodule (Fin (n + 1)) k) (X i) ≤ ⊤)).op
        ((ProjSpace.π k n).appTop ((Scheme.ΓSpecIso (.of k)).inv r))
      = Proj.awayToSection (homogeneousSubmodule (Fin (n + 1)) k) (X i)
          (algebraMap k (Away (homogeneousSubmodule (Fin (n + 1)) k) (X i)) r)
def

frac

L109 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L118 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L123 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L130 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L139 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L166 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L170 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L173 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L177 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L181 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L184 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L201 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

L219 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.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_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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

pullAway_algebraMap

L234 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq.P2mWs6E1Aux.pullAway_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6E1Aux
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_algebraMap (i : Fin (n + 1)) (c : k) {W : Z.Opens} (hW : W ≤
  ProjSpace.pullbackChart φ i) :
    ProjSpace.restrictFun hW (pullAway φ i (algebraMap k (Away 𝒜 (X i)) c))
      = (Scheme.TwoAffineOpenCover.algebraOfHom (φ ≫ ProjSpace.π k n) W).algebraMap c
theorem

exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq

L254 ↗
AlgebraicGeometry.ProjSpace.exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
open P2mWs6E1Aux in
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_linearMap_homogeneousSubmodule_twistObj_top_val_eq
    {k : Type u} [CommRing k] {n : ℕ} {Z : Scheme.{u}}
    (φ : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (d : ℕ) :
    ∃ θ : ↥(MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k d) →ₗ[k]
        ProjSpace.twistObj (φ ≫ ProjSpace.π k n) φ d ⊤,
      (∀ (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d) (i : Fin (n + 1)),
        (θ ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩).val i =
          ProjSpace.restrictFun (inf_le_right : ⊤ ⊓ ProjSpace.pullbackChart φ i ≤
            ProjSpace.pullbackChart φ i)
            ((φ.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
              (MvPolynomial.X i)))
              (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                (MvPolynomial.X i)
                (HomogeneousLocalization.mk
                  { deg := d
                    num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                    den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i d)⟩
                    den_mem := ⟨d, rfl⟩ })))) ∧
      (∀ (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d),
        θ ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩ = 0 ↔
          ∀ i : Fin (n + 1),
            (φ.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
              (MvPolynomial.X i)))
              (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                (MvPolynomial.X i)
                (HomogeneousLocalization.mk
                  { deg := d
                    num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                    den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i d)⟩
                    den_mem := ⟨d, rfl⟩ })) = 0)

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