NYLL
Module

Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
8 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On exists Unique ihom Eval eq

Imports2
Imported by8

Declarations

theorem

map_map

L37 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.map_map
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem map_map (M : X.Modules) {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (y : Γ(M,
  V₁)) :
    M.presheaf.map (homOfLE h₃₂).op (M.presheaf.map (homOfLE h₂₁).op y) =
      M.presheaf.map (homOfLE (h₃₂.trans h₂₁)).op y
theorem

ihomSection_ext

L44 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.ihomSection_ext
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem ihomSection_ext (p : Γ(P, V)) (hp : IsFrameOn p V) {θ θ' : Γ((ihom P).obj Q, V)}
    (h : ihomEval P Q V p θ = ihomEval P Q V p θ') : θ = θ'
def

coeff

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.coeff
Documentation

Coordinates of a section relative to the restriction of the chosen frame.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
def coeff (p : Γ(P, V)) (hp : IsFrameOn p V) {W : X.Opens} (hW : W ≤ V) :
    Γ(P, W) ≃ₗ[Γ(X, W)] Γ(X, W)
theorem

coeff_smul

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.coeff_smul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem coeff_smul (p : Γ(P, V)) (hp : IsFrameOn p V) {W : X.Opens} (hW : W ≤ V) (g : Γ(X, W)) :
    coeff p hp hW (g • P.presheaf.map (homOfLE hW).op p) = g
theorem

smul_coeff

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.smul_coeff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem smul_coeff (p : Γ(P, V)) (hp : IsFrameOn p V) {W : X.Opens} (hW : W ≤ V) (x : Γ(P, W)) :
    coeff p hp hW x • P.presheaf.map (homOfLE hW).op p = x
theorem

exists_ihomSection

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.exists_ihomSection
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem exists_ihomSection (p : Γ(P, V)) (hp : IsFrameOn p V) (q : Γ(Q, V)) :
    ∃ θ : Γ((ihom P).obj Q, V), ihomEval P Q V p θ = q
theorem

exists_unique_ihomSection

L119 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq.N2P1.exists_unique_ihomSection
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace N2P1
variable {X : Scheme.{u}} {P Q : X.Modules} {V : X.Opens}
Lean source · statement
theorem exists_unique_ihomSection (p : Γ(P, V)) (hp : IsFrameOn p V) (q : Γ(Q, V)) :
    ∃! θ : Γ((ihom P).obj Q, V), ihomEval P Q V p θ = q
theorem

existsUnique_ihomEval_eq

L127 ↗
AlgebraicGeometry.Scheme.Modules.IsFrameOn.existsUnique_ihomEval_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_existsUnique_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.existsUnique_ihomEval_eq {X :
  Scheme.{u}} {P Q : X.Modules} {V : X.Opens} {p : Γ(P, V)}
    (hp : Scheme.Modules.IsFrameOn p V) (q : Γ(Q, V)) :
    ∃! θ : Γ((ihom P).obj Q, V), Scheme.Modules.ihomEval P Q V p θ = q

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