NYLL
Module

ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
8 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists hom twist val eq mul and injective of cocycle

Imports14
Imported by2

Declarations

theorem

eq_zero_of_restrict_mul_eq_zero

L50 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.eq_zero_of_restrict_mul_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
Lean source · statement
theorem eq_zero_of_restrict_mul_eq_zero {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (t :
  Γ(X, U))
    (ht : ∀ y : Γ(X, U), t * y = 0 → y = 0) {V : X.Opens} (hV : V ≤ U) (g : Γ(X, V))
    (hg : (X.presheaf.map (homOfLE hV).op).hom t * g = 0) : g = 0
def

Cocycle

L80 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.Cocycle
Documentation

The compatibility condition for local sections whose transition factor is the eth power of the frame unit.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def Cocycle (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i)) : Prop
def

mulVal

L89 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.mulVal
Documentation

Componentwise multiplication of a twisted section by the given local sections.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
def mulVal (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i)) (d : ℕ) (U : Z.Opens) (g
  : twistObj π ι d U) : ∀ i : Fin (N + 1), Γ(Z, U ⊓ pullbackChart ι i)
theorem

mulVal_compat

L93 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.mulVal_compat
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem mulVal_compat (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i)) (htc : Cocycle ι e t)
    (d : ℕ) (U : Z.Opens) (g : twistObj π ι d U) :
    TwistCompat ι (d + e) U (mulVal π ι t d U g)
def

mulHom

L127 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.mulHom
Documentation

The morphism of twisted presheaves induced by local sections satisfying the transition cocycle condition.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · full declaration
def mulHom (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i)) (htc : Cocycle ι
  e t) (d : ℕ) :
    Hom (twist π ι d) (twist π ι (d + e)) where
  app U :=
    { toFun := fun g => ⟨mulVal π ι t d U g, mulVal_compat π ι e t htc d U g⟩
      map_add' := fun g g' => twistObj.ext (funext fun i => by
        change restrictFun _ (t i) * (g.val i + g'.val i) = restrictFun _ (t i) * g.val i +
          restrictFun _ (t i) * g'.val i
        rw [mul_add])
      map_smul' := fun r g => twistObj.ext (funext fun i => by
        let := Scheme.TwoAffineOpenCover.algebraOfHom π U
        change restrictFun (inf_le_right : U ⊓ pullbackChart ι i ≤ pullbackChart ι i) (t i)
            * (restrictFun (inf_le_left : U ⊓ pullbackChart ι i ≤ U) (algebraMap A (Γ(Z, U) : Type
              u) r) * g.val i)
          = restrictFun (inf_le_left : U ⊓ pullbackChart ι i ≤ U) (algebraMap A (Γ(Z, U) : Type u)
            r)
            * (restrictFun (inf_le_right : U ⊓ pullbackChart ι i ≤ pullbackChart ι i) (t i) * g.val
              i)
        ring) }
  app_smul U a g := twistObj.ext (funext fun i => by
    change restrictFun (inf_le_right : U ⊓ pullbackChart ι i ≤ pullbackChart ι i) (t i)
        * (restrictFun (inf_le_left : U ⊓ pullbackChart ι i ≤ U) a * g.val i)
      = restrictFun (inf_le_left : U ⊓ pullbackChart ι i ≤ U) a
        * (restrictFun (inf_le_right : U ⊓ pullbackChart ι i ≤ pullbackChart ι i) (t i) * g.val i)
    ring)
  naturality {U U'} h := LinearMap.ext fun g => twistObj.ext (funext fun i => by
    change restrictFun _ (t i) * ((twist π ι d).res h g).val i
      = ((twist π ι (d + e)).res h ⟨mulVal π ι t d U' g, mulVal_compat π ι e t htc d U' g⟩).val i
    rw [twist_res_val (π := π) (φ := ι) (m := d) h g i,
      twist_res_val (π := π) (φ := ι) (m := d + e) h
        ⟨mulVal π ι t d U' g, mulVal_compat π ι e t htc d U' g⟩ i]
    change restrictFun _ (t i) * restrictFun _ (g.val i) = restrictFun _ (restrictFun _ (t i) *
      g.val i)
    rw [map_mul, restrictFun_restrictFun])
theorem

mulHom_val

L162 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.mulHom_val
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem mulHom_val (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i)) (htc : Cocycle ι e t)
    (d : ℕ) (U : Z.Opens) (g : (twist π ι d).obj U) (i : Fin (N + 1)) :
    ((mulHom π ι e t htc d).app U g).val i
      = restrictFun (inf_le_right : U ⊓ pullbackChart ι i ≤ pullbackChart ι i) (t i) * g.val i
theorem

mulHom_injective

L168 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle.P2mTwistMulSol.mulHom_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
namespace P2mTwistMulSol
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.OModulePresheaf
section Mul
variable {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
  (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
Lean source · statement
theorem mulHom_injective [IsAffineHom ι] (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, pullbackChart ι i))
    (htc : Cocycle ι e t) (hnz : ∀ (i : Fin (N + 1)) (y : Γ(Z, pullbackChart ι i)), t i * y = 0 → y
      = 0)
    (d : ℕ) (U : Z.Opens) : Function.Injective ((mulHom π ι e t htc d).app U)
theorem

exists_hom_twist_val_eq_mul_and_injective_of_cocycle

L186 ↗
AlgebraicGeometry.ProjSpace.exists_hom_twist_val_eq_mul_and_injective_of_cocycle
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_hom_twist_val_eq_mul_and_injective_of_cocycle
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_hom_twist_val_eq_mul_and_injective_of_cocycle
    {A : Type u} [CommRing A] {N : ℕ} {Z : Scheme.{u}}
    (π : Z ⟶ Spec (.of A)) (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
      [IsAffineHom ι]
    (e : ℕ) (t : ∀ i : Fin (N + 1), Γ(Z, ProjSpace.pullbackChart ι i))
    (htc : ∀ i j : Fin (N + 1),
      ProjSpace.restrictFun (inf_le_left : ProjSpace.pullbackChart ι i ⊓ ProjSpace.pullbackChart ι
        j ≤ _) (t i)
        = ProjSpace.restrictFun (inf_le_left : ProjSpace.pullbackChart ι i ⊓
          ProjSpace.pullbackChart ι j ≤ _)
            (ProjSpace.frameUnit ι i j) ^ e
          * ProjSpace.restrictFun (inf_le_right : ProjSpace.pullbackChart ι i ⊓
            ProjSpace.pullbackChart ι j ≤ _) (t j))
    (hnz : ∀ (i : Fin (N + 1)) (y : Γ(Z, ProjSpace.pullbackChart ι i)), t i * y = 0 → y = 0) (d :
      ℕ) :
    ∃ μ : OModulePresheaf.Hom (ProjSpace.twist π ι d) (ProjSpace.twist π ι (d + e)),
      (∀ (U : Z.Opens) (g : (ProjSpace.twist π ι d).obj U) (i : Fin (N + 1)),
        (μ.app U g).val i
          = ProjSpace.restrictFun (inf_le_right : U ⊓ ProjSpace.pullbackChart ι i ≤ _) (t i) *
            g.val i) ∧
      (∀ U : Z.Opens, Function.Injective (μ.app U))

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