Module

ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup

60 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists linear Equiv H0 HSucc coker twist of ker eq sup

Imports31

Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.DirectSum.Decomposition
Mathlib.Algebra.GradedMonoid
Mathlib.Algebra.Module.Submodule.Equiv
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Fintype.Lattice
Mathlib.GroupTheory.MonoidLocalization.Basic
Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Mathlib.LinearAlgebra.Pi
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.RingTheory.GradedAlgebra.Basic
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.Tactic.Ring
Nyll.SchemeTheory.ProjectiveSpace.Basic
Nyll.SchemeTheory.ProjectiveSpace.Cover
Nyll.AlgebraicCurves.Geometry.Projective.ProjTwistDatum
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafHom
Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafConstructions

Imported by2

def

kerEquiv

L73 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.kerEquiv

Documentation

The induced equivalence of kernels from a commuting square with a bijective source map and injective target map.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
section Generic
variable {R : Type*} [CommRing R]
  {M0 M1 M2 N0 N1 N2 : Type*} [AddCommGroup M0] [Module R M0] [AddCommGroup M1] [Module R M1]
  [AddCommGroup M2] [Module R M2] [AddCommGroup N0] [Module R N0] [AddCommGroup N1] [Module R N1]
  [AddCommGroup N2] [Module R N2]

Lean source · statement

def kerEquiv (a : M0 →ₗ[R] M1) (b : N0 →ₗ[R] N1) (Φ0 : M0 →ₗ[R] N0) (Φ1 : M1 →ₗ[R] N1)
    (hcomm : Φ1 ∘ₗ a = b ∘ₗ Φ0) (h0 : Function.Bijective Φ0) (h1 : Function.Injective Φ1) :
    LinearMap.ker a ≃ₗ[R] LinearMap.ker b

theorem

kerEquiv_apply_val

L96 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.kerEquiv_apply_val

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
section Generic
variable {R : Type*} [CommRing R]
  {M0 M1 M2 N0 N1 N2 : Type*} [AddCommGroup M0] [Module R M0] [AddCommGroup M1] [Module R M1]
  [AddCommGroup M2] [Module R M2] [AddCommGroup N0] [Module R N0] [AddCommGroup N1] [Module R N1]
  [AddCommGroup N2] [Module R N2]

Lean source · statement

theorem kerEquiv_apply_val (a : M0 →ₗ[R] M1) (b : N0 →ₗ[R] N1) (Φ0 : M0 →ₗ[R] N0) (Φ1 : M1 →ₗ[R] N1)
    (hcomm : Φ1 ∘ₗ a = b ∘ₗ Φ0) (h0 : Function.Bijective Φ0) (h1 : Function.Injective Φ1)
    (x : LinearMap.ker a) : (kerEquiv a b Φ0 Φ1 hcomm h0 h1 x).1 = Φ0 x.1

abbrev

HQ

L104 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.HQ

Documentation

The quotient of the second differential kernel by the first differential image inside that kernel.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
section Generic
variable {R : Type*} [CommRing R]
  {M0 M1 M2 N0 N1 N2 : Type*} [AddCommGroup M0] [Module R M0] [AddCommGroup M1] [Module R M1]
  [AddCommGroup M2] [Module R M2] [AddCommGroup N0] [Module R N0] [AddCommGroup N1] [Module R N1]
  [AddCommGroup N2] [Module R N2]

Lean source · statement

abbrev HQ (a0 : M0 →ₗ[R] M1) (a1 : M1 →ₗ[R] M2) : Type _

def

HQEquiv

L111 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.HQEquiv

Documentation

The induced equivalence on cohomology from a commuting triple of maps with the stated surjectivity, bijectivity and injectivity properties.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
section Generic
variable {R : Type*} [CommRing R]
  {M0 M1 M2 N0 N1 N2 : Type*} [AddCommGroup M0] [Module R M0] [AddCommGroup M1] [Module R M1]
  [AddCommGroup M2] [Module R M2] [AddCommGroup N0] [Module R N0] [AddCommGroup N1] [Module R N1]
  [AddCommGroup N2] [Module R N2]

Lean source · statement

def HQEquiv (a0 : M0 →ₗ[R] M1) (a1 : M1 →ₗ[R] M2) (b0 : N0 →ₗ[R] N1) (b1 : N1 →ₗ[R]
  N2)
    (Φ0 : M0 →ₗ[R] N0) (Φ1 : M1 →ₗ[R] N1) (Φ2 : M2 →ₗ[R] N2)
    (hc0 : Φ1 ∘ₗ a0 = b0 ∘ₗ Φ0) (hc1 : Φ2 ∘ₗ a1 = b1 ∘ₗ Φ1)
    (h0 : Function.Surjective Φ0) (h1 : Function.Bijective Φ1) (h2 : Function.Injective Φ2) :
    HQ a0 a1 ≃ₗ[R] HQ b0 b1

theorem

HQEquiv_mk

L154 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.HQEquiv_mk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
section Generic
variable {R : Type*} [CommRing R]
  {M0 M1 M2 N0 N1 N2 : Type*} [AddCommGroup M0] [Module R M0] [AddCommGroup M1] [Module R M1]
  [AddCommGroup M2] [Module R M2] [AddCommGroup N0] [Module R N0] [AddCommGroup N1] [Module R N1]
  [AddCommGroup N2] [Module R N2]

Lean source · full declaration

theorem HQEquiv_mk (a0 : M0 →ₗ[R] M1) (a1 : M1 →ₗ[R] M2) (b0 : N0 →ₗ[R] N1) (b1 : N1 →ₗ[R] N2)
    (Φ0 : M0 →ₗ[R] N0) (Φ1 : M1 →ₗ[R] N1) (Φ2 : M2 →ₗ[R] N2)
    (hc0 : Φ1 ∘ₗ a0 = b0 ∘ₗ Φ0) (hc1 : Φ2 ∘ₗ a1 = b1 ∘ₗ Φ1)
    (h0 : Function.Surjective Φ0) (h1 : Function.Bijective Φ1) (h2 : Function.Injective Φ2)
    (x : LinearMap.ker a1) :
    HQEquiv a0 a1 b0 b1 Φ0 Φ1 Φ2 hc0 hc1 h0 h1 h2 (Submodule.Quotient.mk x)
      = Submodule.Quotient.mk ⟨Φ1 x.1, by
          rw [LinearMap.mem_ker, ← LinearMap.comp_apply, ← hc1, LinearMap.comp_apply,
            LinearMap.mem_ker.mp x.2,
            map_zero]⟩ := rfl

theorem

res_irrel

L180 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.res_irrel

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Transport
variable {R : Type*} [CommRing R] {V : Scheme} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · statement

theorem res_irrel {U₁ U₂ U₃ : V.Opens} (h₁ : U₁ ≤ U₂) (h₂ : U₂ ≤ U₃) (h₃ : U₁ ≤ U₃) (x : F.obj U₃) :
    F.res h₁ (F.res h₂ x) = F.res h₃ x

theorem

res_eq_bijective

L184 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.res_eq_bijective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Transport
variable {R : Type*} [CommRing R] {V : Scheme} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)

Lean source · statement

theorem res_eq_bijective {U₁ U₂ : V.Opens} (h : U₁ = U₂) : Function.Bijective (F.res h.le)

theorem

preimage_iInf_fin

L191 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.preimage_iInf_fin

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf

Lean source · statement

theorem preimage_iInf_fin {X Y : Scheme} (f : X ⟶ Y) {m : ℕ} (U : Fin (m + 1) → Y.Opens) :
    f ⁻¹ᵁ (⨅ i, U i) = ⨅ i, f ⁻¹ᵁ U i

theorem

restrictFun_bijective_of_le_le

L213 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.restrictFun_bijective_of_le_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Res
variable {X Y : Scheme.{u}}

Lean source · statement

theorem restrictFun_bijective_of_le_le {W W' : X.Opens} (h : W ≤ W') (h' : W' ≤ W) :
    Function.Bijective (restrictFun h : Γ(X, W') → Γ(X, W))

theorem

restrictFun_injective_of_le_le

L219 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.restrictFun_injective_of_le_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Res
variable {X Y : Scheme.{u}}

Lean source · statement

theorem restrictFun_injective_of_le_le {W W' : X.Opens} (h : W ≤ W') (h' : W' ≤ W) {x y : Γ(X, W')}
    (e : restrictFun h x = restrictFun h y) : x = y

theorem

app_restrictFun

L223 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.app_restrictFun

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Res
variable {X Y : Scheme.{u}}

Lean source · statement

theorem app_restrictFun (f : X ⟶ Y) {W W' : Y.Opens} (h : W ≤ W') (x : Γ(Y, W')) :
    (f.app W).hom (restrictFun h x) = restrictFun (f.preimage_mono h) ((f.app W').hom x)

theorem

X_pow_mem

L239 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.X_pow_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem X_pow_mem (i : Fin (n + 1)) (e : ℕ) : (X i : S) ^ e ∈ 𝒜 e

def

frac

L244 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frac

Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

def frac (i : Fin (n + 1)) (e : ℕ) (G : 𝒜 e) : Away 𝒜 (X i : S)

theorem

frac_mul

L248 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frac_mul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem frac_mul (i : Fin (n + 1)) (a b : ℕ) (G : 𝒜 a) (H : 𝒜 b) :
    frac n k i (a + b) ⟨(G : S) * (H : S), SetLike.GradedMul.mul_mem G.2 H.2⟩ = frac n k i a G *
      frac n k i b H

theorem

frac_eq_zero

L257 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frac_eq_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem frac_eq_zero (i : Fin (n + 1)) (e : ℕ) (G : 𝒜 e) (hG : (G : S) = 0) : frac n k i e G = 0

theorem

frac_congr

L263 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frac_congr

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem frac_congr (i : Fin (n + 1)) {e : ℕ} {G H : 𝒜 e} (h : (G : S) = H) : frac n k i e G = frac
  n k i e H

theorem

frac_mem_span

L267 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frac_mem_span

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Principal
variable (n : ℕ) (k : Type u) [CommRing k]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem frac_mem_span (ℓ : S) (hℓ : ℓ.IsHomogeneous 1) (i : Fin (n + 1)) (d : ℕ) (G : S) (hG :
  G.IsHomogeneous d)
    (hGI : G ∈ Ideal.span {ℓ}) :
    Proj.awayToSection 𝒜 (X i) (frac n k i d ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr
      hG⟩) ∈
      Ideal.span {Proj.awayToSection 𝒜 (X i) (frac n k i 1 ⟨ℓ,
        (MvPolynomial.mem_homogeneousSubmodule 1 ℓ).mpr hℓ⟩)}

theorem

pullbackChart_comp

L308 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.pullbackChart_comp

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem pullbackChart_comp (i : Fin (n + 1)) : pullbackChart (j ≫ ιk) i = j ⁻¹ᵁ pullbackChart ιk i

theorem

frameUnit_comp

L311 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.frameUnit_comp

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k

Lean source · statement

theorem frameUnit_comp (i l : Fin (n + 1)) :
    frameUnit (j ≫ ιk) i l = (j.app (pullbackChart ιk i)).hom (frameUnit ιk i l)

def

resJVal

L317 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJVal

Documentation

The componentwise pullback of a twisted section along j.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

def resJVal (U : Zk.Opens) (g : twistObj (ιk ≫ ProjSpace.π k n) ιk m U) :
    ∀ i : Fin (n + 1), Γ(Z', (j ⁻¹ᵁ U) ⊓ pullbackChart (j ≫ ιk) i)

theorem

resJVal_compat

L321 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJVal_compat

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem resJVal_compat (U : Zk.Opens) (g : twistObj (ιk ≫ ProjSpace.π k n) ιk m U) :
    TwistCompat (j ≫ ιk) m (j ⁻¹ᵁ U) (resJVal ιk j m U g)

theorem

app_algebraMap

L328 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.app_algebraMap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem app_algebraMap (U : Zk.Opens) (r : k) :
    (j.app U).hom ((Scheme.TwoAffineOpenCover.algebraOfHom (ιk ≫ ProjSpace.π k n) U).algebraMap r) =
      (Scheme.TwoAffineOpenCover.algebraOfHom ((j ≫ ιk) ≫ ProjSpace.π k n) (j ⁻¹ᵁ U)).algebraMap r

def

resJ

L341 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ

Documentation

The linear pullback map on twisted sections along j.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · full declaration

def resJ (U : Zk.Opens) :
    (twist (ιk ≫ ProjSpace.π k n) ιk m).obj U →ₗ[k] (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk)
      m).obj (j ⁻¹ᵁ U) where
  toFun g := ⟨resJVal ιk j m U g, resJVal_compat ιk j m U g⟩
  map_add' g g' := twistObj.ext (funext fun i => by
    change (j.app _).hom (g.val i + g'.val i) = resJVal ιk j m U g i + resJVal ιk j m U g' i
    rw [map_add]; rfl)
  map_smul' r g := twistObj.ext (funext fun i => by
    change (j.app _).hom (restrictFun _ ((Scheme.TwoAffineOpenCover.algebraOfHom (ιk ≫ ProjSpace.π
      k n) U).algebraMap r) * g.val i)
      = restrictFun _ ((Scheme.TwoAffineOpenCover.algebraOfHom ((j ≫ ιk) ≫ ProjSpace.π k n) (j ⁻¹ᵁ
        U)).algebraMap r) *
          resJVal ιk j m U g i
    rw [map_mul, app_restrictFun, app_algebraMap]
    rfl)

theorem

resJ_val

L357 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_val

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem resJ_val (U : Zk.Opens) (g : (twist (ιk ≫ ProjSpace.π k n) ιk m).obj U) (i : Fin (n + 1)) :
    (resJ ιk j m U g).val i = (j.app (U ⊓ pullbackChart ιk i)).hom (g.val i)

theorem

resJ_res

L360 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_res

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem resJ_res {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk m).obj U') :
    resJ ιk j m U ((twist (ιk ≫ ProjSpace.π k n) ιk m).res h g) =
      (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) m).res (j.preimage_mono h) (resJ ιk j m U' g)

theorem

resJ_smul

L371 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_smul

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem resJ_smul (U : Zk.Opens) (a : Γ(Zk, U)) (g : (twist (ιk ≫ ProjSpace.π k n) ιk m).obj U) :
    resJ ιk j m U (a • g) = (j.app U).hom a • resJ ιk j m U g

theorem

spread_compat

L377 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.spread_compat

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · full declaration

theorem spread_compat (i₀ : Fin (n + 1)) (W : Zk.Opens) (y : Γ(Zk, W)) :
    TwistCompat ιk m W (fun i =>
      restrictFun (inf_le_right : W ⊓ pullbackChart ιk i ≤ pullbackChart ιk i) (frameUnit ιk i i₀)
        ^ m *
        restrictFun (inf_le_left : W ⊓ pullbackChart ιk i ≤ W) y) := by
  intro i l
  simp only [map_mul, map_pow, restrictFun_restrictFun]
  have hO : (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk l ≤ pullbackOverlap ιk i l := by
    rw [pullbackOverlap_eq_inf]; exact le_inf (inf_le_left.trans inf_le_right) inf_le_right
  have hc := congrArg (restrictFun hO) (frameUnit_cocycle ιk i l i₀)
  rw [map_mul, restrictFun_restrictFun, restrictFun_restrictFun, restrictFun_restrictFun] at hc
  have e1 : restrictFun ((inf_le_left : (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk l ≤ _).trans
    inf_le_right)
      (frameUnit ιk i i₀) = restrictFun (hO.trans (pullbackOverlap_le_left ιk i l)) (frameUnit ιk i
        i₀) := rfl
  have e2 : restrictFun ((inf_le_left : (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk l ≤ _).trans
    inf_le_left) y =
      restrictFun ((le_inf (le_trans inf_le_left inf_le_left) inf_le_right :
        (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk l ≤ W ⊓ pullbackChart ιk l).trans inf_le_left)
          y := rfl
  have e3 : restrictFun (hO.trans (pullbackOverlap_le_left ιk i l)) (frameUnit ιk i l) =
      restrictFun (le_trans inf_le_left inf_le_right : (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk
        l ≤ pullbackChart ιk i)
        (frameUnit ιk i l) := rfl
  have e4 : restrictFun (hO.trans (pullbackOverlap_le_right ιk i l)) (frameUnit ιk l i₀) =
      restrictFun ((le_inf (le_trans inf_le_left inf_le_left) inf_le_right :
        (W ⊓ pullbackChart ιk i) ⊓ pullbackChart ιk l ≤ W ⊓ pullbackChart ιk l).trans inf_le_right)
          (frameUnit ιk l i₀) := rfl
  rw [e1, ← hc, e2, e3, e4, mul_pow]
  ring

def

spread

L409 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.spread

Documentation

The compatible twisted section obtained by spreading a section from the chosen chart.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

def spread (i₀ : Fin (n + 1)) (W : Zk.Opens) (y : Γ(Zk, W)) :
    twistObj (ιk ≫ ProjSpace.π k n) ιk m W

theorem

spread_val

L413 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.spread_val

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem spread_val (i₀ : Fin (n + 1)) (W : Zk.Opens) (y : Γ(Zk, W)) (i : Fin (n + 1)) :
    (spread ιk m i₀ W y).val i =
      restrictFun (inf_le_right : W ⊓ pullbackChart ιk i ≤ pullbackChart ιk i) (frameUnit ιk i i₀)
        ^ m *
        restrictFun (inf_le_left : W ⊓ pullbackChart ιk i ≤ W) y

theorem

eq_spread

L419 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.eq_spread

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)

Lean source · statement

theorem eq_spread (i₀ : Fin (n + 1)) (W : Zk.Opens) (hW : W ≤ pullbackChart ιk i₀)
    (g : twistObj (ιk ≫ ProjSpace.π k n) ιk m W) :
    g = spread ιk m i₀ W (restrictFun (le_inf le_rfl hW : W ≤ W ⊓ pullbackChart ιk i₀) (g.val i₀))

theorem

twist_zero_val

L452 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.twist_zero_val

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)

Lean source · statement

theorem twist_zero_val {X : Scheme.{u}} (π : X ⟶ Spec (.of k)) (φ : X ⟶ Proj 𝒜) (m : ℕ) (U :
  X.Opens) (i : Fin (n + 1)) :
    (0 : (twist π φ m).obj U).val i = 0

def

tℓ

L459 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.tℓ

Documentation

The local section represented by the homogeneous linear form divided by the chosen coordinate.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)

Lean source · statement

def tℓ (i : Fin (n + 1)) : Γ(Zk, pullbackChart ιk i)

theorem

ideal_𝓘ℓ_eq

L470 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.ideal_𝓘ℓ_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
omit hker in

Lean source · statement

theorem ideal_𝓘ℓ_eq (i₀ : Fin (n + 1)) (V : (Proj 𝒜).affineOpens)
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) :
    𝓘ℓ.ideal V = Ideal.span {(restrictFun hV
      (Proj.awayToSection 𝒜 (X i₀) (frac n k i₀ 1 ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1
        ℓ).mpr hℓ⟩)))}

theorem

ker_app_eq_span

L490 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.ker_app_eq_span

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
include hker in

Lean source · statement

theorem ker_app_eq_span (i₀ : Fin (n + 1)) (V : (Proj 𝒜).affineOpens)
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) :
    RingHom.ker (j.app (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens))).hom =
      Ideal.span {(restrictFun
        (ιk.preimage_mono hV : ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens) ≤ pullbackChart ιk i₀)
        (tℓ ιk ℓ hℓ i₀))}

theorem

app_tℓ_eq_zero

L533 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.app_tℓ_eq_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
include hker in

Lean source · statement

theorem app_tℓ_eq_zero (i₀ : Fin (n + 1)) (V : (Proj 𝒜).affineOpens)
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) :
    (j.app (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens))).hom
      (restrictFun (ιk.preimage_mono hV : ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens) ≤ pullbackChart ιk i₀) (tℓ ιk
        ℓ hℓ i₀)) = 0

theorem

resJ_surjective

L545 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_surjective

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
omit hℓ h𝓘ℓ hker in

Lean source · statement

theorem resJ_surjective (i₀ : Fin (n + 1)) (V : (Proj 𝒜).affineOpens)
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) :
    Function.Surjective (resJ ιk j m (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens)))

theorem

resJ_eq_zero_iff

L581 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_eq_zero_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
include hker in

Lean source · statement

theorem resJ_eq_zero_iff
    (htc : ∀ i l : Fin (n + 1),
      restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i) (tℓ
        ιk ℓ hℓ i)
        = restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i)
          (frameUnit ιk i l) ^ 1
          * restrictFun (inf_le_right : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk
            l) (tℓ ιk ℓ hℓ l))
    (i₀ : Fin (n + 1)) (V : (Proj 𝒜).affineOpens) (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X
      i₀))
    (d : ℕ) (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens))) :
    resJ ιk j (d + 1) (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens)) g = 0 ↔
      ∃ h : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj (ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens)), ∀ i,
        g.val i = restrictFun (inf_le_right : ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens) ⊓ pullbackChart ιk i ≤
          pullbackChart ιk i)
          (tℓ ιk ℓ hℓ i) * h.val i

theorem

resJ_surjective'

L668 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_surjective'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
omit hℓ h𝓘ℓ hker in

Lean source · statement

theorem resJ_surjective' (W : Zk.Opens) (V : (Proj 𝒜).affineOpens) (i₀ : Fin (n + 1))
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) (hWV : W = ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens)) :
    Function.Surjective (resJ ιk j m W)

theorem

resJ_eq_zero_iff'

L674 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.resJ_eq_zero_iff'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section Main
variable {n : ℕ} {k : Type u} [CommRing k] {Zk Z' : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (j : Z' ⟶ Zk)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
variable (m : ℕ)
variable [IsClosedImmersion ιk] [IsClosedImmersion j]
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
  (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
  (h𝓘ℓ : ∀ i : Fin (n + 1),
      𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
        i),
        Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i)
          (ProjSpace.X_mem_one k n i) one_pos⟩ =
      Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
        G ∈ Ideal.span {ℓ} ∧
        s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ }) })
  (hker : (j ≫ ιk).ker = ιk.ker ⊔ 𝓘ℓ)
include h𝓘ℓ hker
include hker in

Lean source · statement

theorem resJ_eq_zero_iff'
    (htc : ∀ i l : Fin (n + 1),
      restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i) (tℓ
        ιk ℓ hℓ i)
        = restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i)
          (frameUnit ιk i l) ^ 1
          * restrictFun (inf_le_right : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk
            l) (tℓ ιk ℓ hℓ l))
    (W : Zk.Opens) (V : (Proj 𝒜).affineOpens) (i₀ : Fin (n + 1))
    (hV : (V : (Proj 𝒜).Opens) ≤ Proj.basicOpen 𝒜 (X i₀)) (hWV : W = ιk ⁻¹ᵁ (V : (Proj 𝒜).Opens))
    (d : ℕ) (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj W) :
    resJ ιk j (d + 1) W g = 0 ↔
      ∃ h : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj W, ∀ i,
        g.val i = restrictFun (inf_le_right : W ⊓ pullbackChart ιk i ≤ pullbackChart ιk i) (tℓ ιk ℓ
          hℓ i) * h.val i

theorem

restrictFun_app_awayToSection_left

L703 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.restrictFun_app_awayToSection_left

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section TlCocycle
variable {n : ℕ} {k : Type u} [CommRing k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem restrictFun_app_awayToSection_left (i l : Fin (n + 1)) (z : Away 𝒜 (X i : S)) :
    restrictFun (pullbackOverlap_le_left ιk i l)
        ((ιk.app (Proj.basicOpen 𝒜 (X i))).hom ((Proj.awayToSection 𝒜 (X i)).hom z))
      = (ιk.app (Proj.basicOpen 𝒜 (X i * X l))).hom
          ((Proj.awayToSection 𝒜 (X i * X l)).hom (awayMap 𝒜 (X_mem_one k n l) rfl z))

theorem

restrictFun_app_awayToSection_right

L719 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.restrictFun_app_awayToSection_right

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section TlCocycle
variable {n : ℕ} {k : Type u} [CommRing k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem restrictFun_app_awayToSection_right (i l : Fin (n + 1)) (z : Away 𝒜 (X l : S)) :
    restrictFun (pullbackOverlap_le_right ιk i l)
        ((ιk.app (Proj.basicOpen 𝒜 (X l))).hom ((Proj.awayToSection 𝒜 (X l)).hom z))
      = (ιk.app (Proj.basicOpen 𝒜 (X i * X l))).hom
          ((Proj.awayToSection 𝒜 (X i * X l)).hom
            (awayMap 𝒜 (X_mem_one k n i) (mul_comm (X i) (X l) : (X i * X l : S) = X l * X i) z))

theorem

awayMap_tfrac

L738 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.awayMap_tfrac

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section TlCocycle
variable {n : ℕ} {k : Type u} [CommRing k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem awayMap_tfrac (i l : Fin (n + 1)) :
    awayMap 𝒜 (X_mem_one k n l) rfl (frac n k i 1 ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1
      ℓ).mpr hℓ⟩)
      = awayMap 𝒜 (X_mem_one k n l) rfl (ratio k n i l)
        * awayMap 𝒜 (X_mem_one k n i) (mul_comm (X i) (X l) : (X i * X l : S) = X l * X i)
            (frac n k l 1 ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1 ℓ).mpr hℓ⟩)

theorem

tℓ_cocycle

L756 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.tℓ_cocycle

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.HomogeneousLocalization
section TlCocycle
variable {n : ℕ} {k : Type u} [CommRing k] {Zk : Scheme.{u}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
  (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
local notation "S" => MvPolynomial (Fin (n + 1)) k

Lean source · statement

theorem tℓ_cocycle (i l : Fin (n + 1)) :
    restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i) (tℓ ιk
      ℓ hℓ i)
      = restrictFun (inf_le_left : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk i)
        (frameUnit ιk i l) ^ 1
        * restrictFun (inf_le_right : pullbackChart ιk i ⊓ pullbackChart ιk l ≤ pullbackChart ιk l)
          (tℓ ιk ℓ hℓ l)

theorem

K'_inter

L830 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.K'_inter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

theorem K'_inter {i : ℕ} (s : (K).Idx i) : (K').inter s = j ⁻¹ᵁ ((K).inter s)

theorem

K_inter

L835 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.K_inter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

theorem K_inter {i : ℕ} (s : (K).Idx i) : (K).inter s = ιk ⁻¹ᵁ ((K₀).inter s)

def

σ

L841 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.σ

Documentation

The map on the quotient presheaf induced by restriction, which vanishes on the image of μ.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

def σ (W : Zk.Opens) : (Q).obj W →ₗ[k] (F').obj (j ⁻¹ᵁ W)

theorem

σ_mk

L846 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.σ_mk

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
omit [IsClosedImmersion ιk] [IsClosedImmersion j] in

Lean source · statement

theorem σ_mk (W : Zk.Opens) (g : (F).obj W) :
    σ ιk j d μ resJ resJ_μ W (Submodule.Quotient.mk g) = resJ W g

theorem

σ_res

L850 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.σ_res

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
include resJ_res in
omit [IsClosedImmersion ιk] [IsClosedImmersion j] in

Lean source · full declaration

theorem σ_res {W W' : Zk.Opens} (h : W ≤ W') (q : (Q).obj W') :
    σ ιk j d μ resJ resJ_μ W ((Q).res h q)
      = (F').res (show j ⁻¹ᵁ W ≤ j ⁻¹ᵁ W' from fun _ hx => h hx) (σ ιk j d μ resJ resJ_μ W' q) := by
  obtain ⟨g, rfl⟩ := Submodule.Quotient.mk_surjective _ q
  rw [coker_res_mk, σ_mk, σ_mk, resJ_res]

def

T

L860 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.T

Documentation

The quotient-section map on a cover intersection, followed by restriction to the corresponding pulled-back intersection.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

def T {i : ℕ} (s : (K).Idx i) : (Q).obj ((K).inter s) →ₗ[k] (F').obj ((K').inter s)

theorem

T_res

L863 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.T_res

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
include resJ_res in

Lean source · statement

theorem T_res {i i' : ℕ} (s : (K).Idx i) (s' : (K).Idx i') (h : (K).inter s ≤ (K).inter s')
    (h' : (K').inter s ≤ (K').inter s') (q : (Q).obj ((K).inter s')) :
    T ιk j d μ resJ resJ_μ s ((Q).res h q) = (F').res h' (T ιk j d μ resJ resJ_μ s' q)

theorem

T_bijective

L873 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.T_bijective

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
include hsurj hker in

Lean source · statement

theorem T_bijective {i : ℕ} (s : (K).Idx i) : Function.Bijective (T ιk j d μ resJ resJ_μ s)

def

Φ

L890 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.Φ

Documentation

The cochain map induced by the quotient-section maps on cover intersections.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · full declaration

def Φ (i : ℕ) : (Q).cochain (K) i →ₗ[k] (F').cochain (K') i where
  toFun c s := T ιk j d μ resJ resJ_μ s (c s)
  map_add' c c' := funext fun s => (T ιk j d μ resJ resJ_μ s).map_add (c s) (c' s)
  map_smul' r c := funext fun s => (T ιk j d μ resJ resJ_μ s).map_smul r (c s)

theorem

Φ_apply

L895 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.Φ_apply

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

theorem Φ_apply (i : ℕ) (c : (Q).cochain (K) i) (s : (K).Idx i) :
    Φ ιk j d μ resJ resJ_μ i c s = T ιk j d μ resJ resJ_μ s (c s)

theorem

Φ_bijective

L898 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.Φ_bijective

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
include hsurj hker in

Lean source · statement

theorem Φ_bijective (i : ℕ) : Function.Bijective (Φ ιk j d μ resJ resJ_μ i)

theorem

Φ_comm

L908 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.Φ_comm

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n
include resJ_res in

Lean source · statement

theorem Φ_comm (i : ℕ) :
    Φ ιk j d μ resJ resJ_μ (i + 1) ∘ₗ (Q).d (K) i = (F').d (K') i ∘ₗ Φ ιk j d μ resJ resJ_μ i

def

e₀

L936 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.e₀

Documentation

The induced linear equivalence on degree-zero cohomology.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

def e₀ : (Q).H0 (K) ≃ₗ[k] (F').H0 (K')

def

eS

L942 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.eS

Documentation

The induced linear equivalence on higher cohomology.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

def eS (i : ℕ) : (Q).HSucc (K) i ≃ₗ[k] (F').HSucc (K') i

theorem

e₀_val

L950 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.e₀_val

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

theorem e₀_val (c : (Q).H0 (K)) (s : (K').Idx 0) :
    (e₀ ιk j d μ resJ resJ_res resJ_μ hsurj hker c).1 s = T ιk j d μ resJ resJ_μ s (c.1 s)

theorem

e₀_proj_val

L953 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup.P2mQuotSec.e₀_proj_val

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mQuotSec
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Cech
variable {k : Type} [CommRing k] {n : ℕ} {Zk Z' : Scheme.{0}}
  (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsClosedImmersion ιk]
  (j : Z' ⟶ Zk) [IsClosedImmersion j] (d : ℕ)
  (μ : Hom (twist (ιk ≫ ProjSpace.π k n) ιk d) (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
  (resJ : ∀ U : Zk.Opens, (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj U →ₗ[k]
    (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).obj (j ⁻¹ᵁ U))
  (resJ_res : ∀ {U U' : Zk.Opens} (h : U ≤ U') (g : (twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).obj
    U'),
    resJ U ((twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).res h g)
      = (twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)).res (show j ⁻¹ᵁ U ≤ j ⁻¹ᵁ U' from fun
        _ hx => h hx)
          (resJ U' g))
  (resJ_μ : ∀ (U : Zk.Opens) (x : (twist (ιk ≫ ProjSpace.π k n) ιk d).obj U), resJ U (μ.app U x) =
    0)
  (hsurj : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → Function.Surjective (resJ W))
  (hker : ∀ (W : Zk.Opens) (V : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1))
    k)).affineOpens)
    (i₀ : Fin (n + 1)), V.1 ≤ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
      (MvPolynomial.X i₀) →
    W = ιk ⁻¹ᵁ V.1 → ∀ g, resJ W g = 0 → g ∈ LinearMap.range (μ.app W))
local notation "F" => twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)
local notation "F'" => twist ((j ≫ ιk) ≫ ProjSpace.π k n) (j ≫ ιk) (d + 1)
local notation "Q" => OModulePresheaf.coker μ
local notation "K" => ProjSpace.stdCoverPullback ιk
local notation "K'" => ProjSpace.stdCoverPullback (j ≫ ιk)
local notation "K₀" => ProjSpace.stdCover k n

Lean source · statement

theorem e₀_proj_val (c : (F).cochain (K) 0) (hc : c ∈ (F).H0 (K)) (s : (K').Idx 0) (i : Fin (n + 1))
    (h : (K').inter s ⊓ pullbackChart (j ≫ ιk) i ≤ j ⁻¹ᵁ ((K).inter s) ⊓ pullbackChart (j ≫ ιk) i) :
    ((e₀ ιk j d μ resJ resJ_res resJ_μ hsurj hker
        ((OModulePresheaf.imCokerSES μ).proj.toAffHom.H0Map (K) ⟨c, hc⟩)).1 s).val i
      = ProjSpace.restrictFun h ((resJ ((K).inter s) (c s)).val i)

theorem

exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup

L963 ↗

AlgebraicGeometry.ProjSpace.exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.exists_linearEquiv_H0_HSucc_coker_twist_of_ker_eq_sup
    (n : ℕ) (k : Type) [CommRing k]
    (Zk : Scheme.{0}) (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
      [IsClosedImmersion ιk]
    (ℓ : MvPolynomial (Fin (n + 1)) k) (hℓ : ℓ.IsHomogeneous 1)
    (𝓘ℓ : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)).IdealSheafData)
    (h𝓘ℓ : (∀ i : Fin (n + 1),
        𝓘ℓ.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
          (MvPolynomial.X i),
          Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
            (MvPolynomial.X i) (ProjSpace.X_mem_one k n i) one_pos⟩ =
        Ideal.span { s | ∃ (d : ℕ) (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous d),
          G ∈ Ideal.span {ℓ} ∧
          s = Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
            (MvPolynomial.X i)
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule d G).mpr hG⟩
                  den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) }))
    (Z' : Scheme.{0}) (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
      [IsClosedImmersion ι']
    (hker : ι'.ker = ιk.ker ⊔ 𝓘ℓ) (d : ℕ)
    (htc : ∀ i j : Fin (n + 1),
      ProjSpace.restrictFun (inf_le_left : ProjSpace.pullbackChart ιk i ⊓ ProjSpace.pullbackChart
        ιk j ≤ _)
          ((ιk.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 := 1
                  num := ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1 ℓ).mpr hℓ⟩
                  den := ⟨MvPolynomial.X i ^ 1, (MvPolynomial.mem_homogeneousSubmodule 1 _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i 1)⟩
                  den_mem := ⟨1, rfl⟩ })))
        = ProjSpace.restrictFun (inf_le_left : ProjSpace.pullbackChart ιk i ⊓
          ProjSpace.pullbackChart ιk j ≤ _)
            (ProjSpace.frameUnit ιk i j) ^ 1
          * ProjSpace.restrictFun (inf_le_right : ProjSpace.pullbackChart ιk i ⊓
            ProjSpace.pullbackChart ιk j ≤ _)
          ((ιk.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
            (MvPolynomial.X j)))
            (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
              j)
              (HomogeneousLocalization.mk
                { deg := 1
                  num := ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1 ℓ).mpr hℓ⟩
                  den := ⟨MvPolynomial.X j ^ 1, (MvPolynomial.mem_homogeneousSubmodule 1 _).mpr
                    (MvPolynomial.isHomogeneous_X_pow j 1)⟩
                  den_mem := ⟨1, rfl⟩ }))))
    (μ : OModulePresheaf.Hom (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk d)
      (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)))
    (hμ : ∀ (U : Zk.Opens) (g : (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk d).obj U) (i : Fin (n +
      1)),
      (μ.app U g).val i
        = ProjSpace.restrictFun (inf_le_right : U ⊓ ProjSpace.pullbackChart ιk i ≤ _)
          ((ιk.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 := 1
                  num := ⟨ℓ, (MvPolynomial.mem_homogeneousSubmodule 1 ℓ).mpr hℓ⟩
                  den := ⟨MvPolynomial.X i ^ 1, (MvPolynomial.mem_homogeneousSubmodule 1 _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i 1)⟩
                  den_mem := ⟨1, rfl⟩ }))) * g.val i) :
    ∃ (e₀ : (OModulePresheaf.coker μ).H0 (ProjSpace.stdCoverPullback ιk) ≃ₗ[k]
        (ProjSpace.twist (ι' ≫ ProjSpace.π k n) ι' (d + 1)).H0 (ProjSpace.stdCoverPullback ι'))
      (_e : ∀ i : ℕ, (OModulePresheaf.coker μ).HSucc (ProjSpace.stdCoverPullback ιk) i ≃ₗ[k]
        (ProjSpace.twist (ι' ≫ ProjSpace.π k n) ι' (d + 1)).HSucc (ProjSpace.stdCoverPullback ι')
          i),
      ∀ (c : (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).cochain
        (ProjSpace.stdCoverPullback ιk) 0)
        (hc : c ∈ (ProjSpace.twist (ιk ≫ ProjSpace.π k n) ιk (d + 1)).H0
          (ProjSpace.stdCoverPullback ιk))
        (G : MvPolynomial (Fin (n + 1)) k) (hG : G.IsHomogeneous (d + 1)),
          (∀ (s : (ProjSpace.stdCoverPullback ιk).Idx 0) (i : Fin (n + 1)),
            (c s).val i =
              ProjSpace.restrictFun
                (inf_le_right : (ProjSpace.stdCoverPullback ιk).inter s ⊓ ProjSpace.pullbackChart
                  ιk i ≤
                  ProjSpace.pullbackChart ιk i)
                (ιk.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 + 1
                    num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule (d + 1) G).mpr hG⟩
                    den := ⟨MvPolynomial.X i ^ (d + 1), (MvPolynomial.mem_homogeneousSubmodule (d +
                      1) _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i (d + 1))⟩
                    den_mem := ⟨d + 1, rfl⟩ })))) →
          ∀ (s : (ProjSpace.stdCoverPullback ι').Idx 0) (i : Fin (n + 1)),
            ((e₀ ((OModulePresheaf.imCokerSES μ).proj.toAffHom.H0Map (ProjSpace.stdCoverPullback
              ιk) ⟨c, hc⟩)).1 s).val i =
              ProjSpace.restrictFun
                (inf_le_right : (ProjSpace.stdCoverPullback ι').inter s ⊓ 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 + 1
                    num := ⟨G, (MvPolynomial.mem_homogeneousSubmodule (d + 1) G).mpr hG⟩
                    den := ⟨MvPolynomial.X i ^ (d + 1), (MvPolynomial.mem_homogeneousSubmodule (d +
                      1) _).mpr
                      (MvPolynomial.isHomogeneous_X_pow i (d + 1))⟩
                    den_mem := ⟨d + 1, rfl⟩ })))

Module documentation

Proj Space exists linear Equiv H0 HSucc coker twist of ker eq sup

Declarations