NYLL
Module

ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
19 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists linear Equiv base Change cochain twist of is Pullback

Imports16
Imported by6

Declarations

theorem

preimage_pullbackChart

L61 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.preimage_pullbackChart
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem preimage_pullbackChart (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (j : Fin (n + 1)) :
    e ⁻¹ᵁ ProjSpace.pullbackChart ι j = ProjSpace.pullbackChart ι' j
theorem

preimage_inter

L66 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.preimage_inter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem preimage_inter (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) {i : ℕ} (s :
  (ProjSpace.stdCoverPullback ι).Idx i) :
    e ⁻¹ᵁ (ProjSpace.stdCoverPullback ι).inter s = (ProjSpace.stdCoverPullback ι').inter s
theorem

inter_le_pullbackChart

L79 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.inter_le_pullbackChart
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem inter_le_pullbackChart {W : Scheme.{u}} {R : Type u} [CommRing R]
    (φ : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) [IsAffineHom φ]
    {i : ℕ} (s : (ProjSpace.stdCoverPullback φ).Idx i) (t : Fin (i + 1)) :
    (ProjSpace.stdCoverPullback φ).inter s ≤ ProjSpace.pullbackChart φ ((s.1 t).down)
theorem

isAffineOpen_inter

L87 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.isAffineOpen_inter
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem isAffineOpen_inter {W : Scheme.{u}} {R : Type u} [CommRing R]
    (φ : W ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) [IsAffineHom φ]
    {i : ℕ} (s : (ProjSpace.stdCoverPullback φ).Idx i) :
    IsAffineOpen ((ProjSpace.stdCoverPullback φ).inter s)
theorem

X_eq_mvMapGraded_mul_one

L126 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.X_eq_mvMapGraded_mul_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem X_eq_mvMapGraded_mul_one (i : Fin (n + 1)) :
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) B) = (ProjSpace.mvMapGraded A B n)
      (MvPolynomial.X i) * 1
theorem

one_mem_zero

L131 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.one_mem_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem one_mem_zero : (1 : MvPolynomial (Fin (n + 1)) B) ∈ (MvPolynomial.homogeneousSubmodule (Fin
  (n + 1)) B) 0
def

toB

L136 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.toB
Documentation

The coordinate localization map induced by the coefficient base change.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
def toB (i : Fin (n + 1)) : Away 𝒜A (MvPolynomial.X i) →+* Away 𝒜B (MvPolynomial.X i)
theorem

toB_ratio

L141 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.toB_ratio
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem toB_ratio (i j : Fin (n + 1)) : toB (A := A) B i (ProjSpace.ratio A n i j) =
  ProjSpace.ratio B n i j
theorem

restrictFun_app_pullAway

L150 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.restrictFun_app_pullAway
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem restrictFun_app_pullAway (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (i : Fin (n + 1))
    (a : Away 𝒜A (MvPolynomial.X i)) {W' : Z'.Opens}
    (h₁ : W' ≤ e ⁻¹ᵁ ProjSpace.pullbackChart ι i) (h₂ : W' ≤ ProjSpace.pullbackChart ι' i) :
    ProjSpace.restrictFun h₁ ((e.app (ProjSpace.pullbackChart ι i)).hom
        ((ι.app (Proj.basicOpen 𝒜A (MvPolynomial.X i))).hom ((Proj.awayToSection 𝒜A (MvPolynomial.X
          i)).hom a)))
      = ProjSpace.restrictFun h₂ ((ι'.app (Proj.basicOpen 𝒜B (MvPolynomial.X i))).hom
          ((Proj.awayToSection 𝒜B (MvPolynomial.X i)).hom (toB (A := A) B i a)))
theorem

restrictFun_app_frameUnit

L213 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.restrictFun_app_frameUnit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
omit [IsAffineHom ι] [IsAffineHom ι'] in
Lean source · statement
theorem restrictFun_app_frameUnit (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (i j : Fin (n + 1))
  {W' : Z'.Opens}
    (h₁ : W' ≤ e ⁻¹ᵁ ProjSpace.pullbackChart ι i) (h₂ : W' ≤ ProjSpace.pullbackChart ι' i) :
    ProjSpace.restrictFun h₁ ((e.app (ProjSpace.pullbackChart ι i)).hom (ProjSpace.frameUnit ι i j))
      = ProjSpace.restrictFun h₂ (ProjSpace.frameUnit ι' i j)
theorem

restrictFun_app_eq

L221 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.restrictFun_app_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem restrictFun_app_eq {U V : Z.Opens} (hVU : V ≤ U) {W' : Z'.Opens} (h₁ : W' ≤ e ⁻¹ᵁ V) (h₂ :
  W' ≤ e ⁻¹ᵁ U)
    (x : Γ(Z, U)) :
    ProjSpace.restrictFun h₁ ((e.app V).hom (ProjSpace.restrictFun hVU x)) = ProjSpace.restrictFun
      h₂ ((e.app U).hom x)
theorem

appLE_top_top

L233 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.appLE_top_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem appLE_top_top {X Y : Scheme.{u}} (g : X ⟶ Y) (h : (⊤ : X.Opens) ≤ g ⁻¹ᵁ ⊤) : g.appLE ⊤ ⊤ h
  = g.appTop
theorem

appLE_hom_apply

L240 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.appLE_hom_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
section Setup
variable {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
  (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
  (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
  (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
  (e : Z' ⟶ Z)
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
Lean source · statement
theorem appLE_hom_apply {X Y : Scheme.{u}} (g : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (h : V ≤ g ⁻¹ᵁ
  U) (x : Γ(Y, U)) :
    (g.appLE U V h).hom x = ProjSpace.restrictFun h ((g.app U).hom x)
def

valAddHom

L247 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.valAddHom
Documentation

Evaluation of all chart components of a twist section as an additive map.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
Lean source · statement
def valAddHom {R : Type u} [CommRing R] {n : ℕ} {X : Scheme.{u}} (π : X ⟶ Spec (.of
  R))
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) (m : ℕ) (U : X.Opens) :
    ProjSpace.twistObj π φ m U →+ (∀ j : Fin (n + 1), Γ(X, U ⊓ ProjSpace.pullbackChart φ j))
theorem

val_sum

L255 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.val_sum
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
Lean source · statement
theorem val_sum {R : Type u} [CommRing R] {n : ℕ} {X : Scheme.{u}} (π : X ⟶ Spec (.of R))
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) (m : ℕ) (U : X.Opens)
    {κ : Type*} (t : Finset κ) (f : κ → ProjSpace.twistObj π φ m U) :
    (∑ x ∈ t, f x).val = ∑ x ∈ t, (f x).val
theorem

val_zsmul

L261 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.val_zsmul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
Lean source · statement
theorem val_zsmul {R : Type u} [CommRing R] {n : ℕ} {X : Scheme.{u}} (π : X ⟶ Spec (.of R))
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) (m : ℕ) (U : X.Opens)
    (z : ℤ) (g : ProjSpace.twistObj π φ m U) : (z • g).val = z • g.val
theorem

val_sum'

L266 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.val_sum'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
Lean source · statement
theorem val_sum' {R : Type u} [CommRing R] {n : ℕ} {X : Scheme.{u}} (π : X ⟶ Spec (.of R))
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) [IsAffineHom φ] (m : ℕ) (U :
      X.Opens)
    {κ : Type*} (t : Finset κ) (f : κ → (ProjSpace.twist π φ m).obj U) :
    ((∑ x ∈ t, f x : (ProjSpace.twist π φ m).obj U) : ProjSpace.twistObj π φ m U).val
      = ∑ x ∈ t, (f x : ProjSpace.twistObj π φ m U).val
theorem

val_zsmul'

L274 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3.val_zsmul'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HomogeneousLocalization
namespace P2mWs6C3
Lean source · statement
theorem val_zsmul' {R : Type u} [CommRing R] {n : ℕ} {X : Scheme.{u}} (π : X ⟶ Spec (.of R))
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)) [IsAffineHom φ] (m : ℕ) (U :
      X.Opens)
    (z : ℤ) (g : (ProjSpace.twist π φ m).obj U) :
    ((z • g : (ProjSpace.twist π φ m).obj U) : ProjSpace.twistObj π φ m U).val = z • (g :
      ProjSpace.twistObj π φ m U).val
theorem

exists_linearEquiv_baseChange_cochain_twist_of_isPullback

L297 ↗
AlgebraicGeometry.ProjSpace.exists_linearEquiv_baseChange_cochain_twist_of_isPullback
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.ProjSpace
open CategoryTheory CategoryTheory.Limits MvPolynomial TensorProduct
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
open AlgebraicCurves.Cohomology.Sheaves.Proofs in
open ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback.P2mWs6C3 in
Lean source · statement
theorem exists_linearEquiv_baseChange_cochain_twist_of_isPullback
    {A : Type u} [CommRing A] {n : ℕ} {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) [IsAffineHom ι]
    (B : Type u) [CommRing B] [Algebra A B] {Z' : Scheme.{u}}
    (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) [IsAffineHom ι']
    (e : Z' ⟶ Z)
    (hpb : IsPullback e (ι' ≫ ProjSpace.π B n) (ι ≫ ProjSpace.π A n) (Spec.map (CommRingCat.ofHom
      (algebraMap A B))))
    (hcomp : e ≫ ι = ι' ≫ ProjSpace.map A B n) (d : ℕ) :
    ∃ ε : ∀ i : ℕ,
        B ⊗[A] (ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).cochain (ProjSpace.stdCoverPullback ι) i
          ≃ₗ[B]
          (ProjSpace.twist (ι' ≫ ProjSpace.π B n) ι' d).cochain (ProjSpace.stdCoverPullback ι') i,
      (∀ i : ℕ,
        (ε (i + 1)).toLinearMap ∘ₗ ((ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).d
          (ProjSpace.stdCoverPullback ι) i).baseChange B =
          (ProjSpace.twist (ι' ≫ ProjSpace.π B n) ι' d).d (ProjSpace.stdCoverPullback ι') i ∘ₗ (ε
            i).toLinearMap) ∧
      (∀ (i : ℕ) (c : (ProjSpace.twist (ι ≫ ProjSpace.π A n) ι d).cochain
        (ProjSpace.stdCoverPullback ι) i)
        (s : (ProjSpace.stdCoverPullback ι).Idx i) (j : Fin (n + 1))
        (h : (ProjSpace.stdCoverPullback ι').inter s ⊓ ProjSpace.pullbackChart ι' j ≤
          e ⁻¹ᵁ ((ProjSpace.stdCoverPullback ι).inter s ⊓ ProjSpace.pullbackChart ι j)),
        (ε i ((1 : B) ⊗ₜ[A] c) s).val j =
          ProjSpace.restrictFun h ((e.app ((ProjSpace.stdCoverPullback ι).inter s ⊓
            ProjSpace.pullbackChart ι j)) ((c s).val j)))

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