NYLL
Module

Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
16 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On exists is Frame On dual

Imports5
Imported by3

Declarations

lemma

presheaf_map_map

L40 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.presheaf_map_map
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
Lean source · statement
lemma presheaf_map_map (M : X.Modules) {A B C : X.Opens} (f : B ⟶ A) (g : C ⟶ B) (k : C ⟶ A) (x :
  Γ(M, A)) :
    M.presheaf.map g.op (M.presheaf.map f.op x) = M.presheaf.map k.op x
lemma

bij

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.bij
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
include hp in
Lean source · full declaration
lemma bij {W : X.Opens} (hW : W ≤ V) : Function.Bijective fun g : Γ(X, W) => g • P.presheaf.map
  (homOfLE ((hW : _ ≤ V).trans hVU)).op p :=
  hp (hW.trans hVU) hW
def

coef

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef
Documentation

The coefficient of a local section in the specified 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_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
def coef {W : X.Opens} (hW : W ≤ V) (m : Γ(P, W)) : Γ(X, W)
lemma

coef_smul_pr

L57 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef_smul_pr
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coef_smul_pr {W : X.Opens} (hW : W ≤ V) (m : Γ(P, W)) : coef hp hVU hW m • P.presheaf.map
  (homOfLE ((hW : _ ≤ V).trans hVU)).op p = m
lemma

coef_eq_of_smul_eq

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef_eq_of_smul_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coef_eq_of_smul_eq {W : X.Opens} (hW : W ≤ V) {m : Γ(P, W)} {g : Γ(X, W)} (h : g •
  P.presheaf.map (homOfLE ((hW : _ ≤ V).trans hVU)).op p = m) :
    coef hp hVU hW m = g
lemma

coef_pr

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef_pr
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coef_pr {W : X.Opens} (hW : W ≤ V) : coef hp hVU hW (P.presheaf.map (homOfLE ((hW : _ ≤
  V).trans hVU)).op p) = 1
lemma

coef_add

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef_add
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coef_add {W : X.Opens} (hW : W ≤ V) (m m' : Γ(P, W)) :
    coef hp hVU hW (m + m') = coef hp hVU hW m + coef hp hVU hW m'
lemma

coef_smul

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coef_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_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coef_smul {W : X.Opens} (hW : W ≤ V) (r : Γ(X, W)) (m : Γ(P, W)) :
    coef hp hVU hW (r • m) = r * coef hp hVU hW m
lemma

map_coef

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.map_coef
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma map_coef {W W' : X.Opens} (hW : W ≤ V) (i : W' ⟶ W) (m : Γ(P, W)) :
    X.presheaf.map i.op (coef hp hVU hW m) = coef hp hVU (i.le.trans hW) (P.presheaf.map i.op m)
def

coefLin

L90 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coefLin
Documentation

The linear coefficient map with values in sections of the unit sheaf.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · full declaration
def coefLin {W : X.Opens} (hW : W ≤ V) : Γ(P, W) →ₗ[Γ(X, W)] Γ(𝟙_ X.Modules, W) where
  toFun m := coef hp hVU hW m • Scheme.Modules.unitSection W
  map_add' m m' := by rw [coef_add, add_smul]
  map_smul' r m := by rw [coef_smul, mul_smul, RingHom.id_apply]
lemma

coefLin_apply

L95 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coefLin_apply
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coefLin_apply {W : X.Opens} (hW : W ≤ V) (m : Γ(P, W)) :
    coefLin hp hVU hW m = coef hp hVU hW m • Scheme.Modules.unitSection W
def

coefFamily

L99 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coefFamily
Documentation

The natural family of coefficient maps on subopens.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
def coefFamily :
    PresheafOfModules.InternalHom.naturalFamilies ((Scheme.Modules.toPMod X).obj P)
      ((Scheme.Modules.toPMod X).obj (𝟙_ X.Modules)) (op V)
lemma

coefFamily_app

L110 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.coefFamily_app
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma coefFamily_app {W : (X.Opens)ᵒᵖ} (f : op V ⟶ W) (m : Γ(P, W.unop)) :
    (coefFamily hp hVU).1 f m = coef hp hVU (f.unop.le : W.unop ≤ V) m •
      Scheme.Modules.unitSection W.unop
def

dualSection

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.dualSection
Documentation

The dual section corresponding to the natural family of coefficient maps.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
def dualSection : Γ(Scheme.Modules.dual P, V)
lemma

ihomEval_map_dualSection

L120 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual.DualFrameAux.ihomEval_map_dualSection
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
noncomputable section
namespace DualFrameAux
variable {X : Scheme.{u}}
variable {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)} (hp : Scheme.Modules.IsFrameOn p V) (hVU :
  V ≤ U)
Lean source · statement
lemma ihomEval_map_dualSection {W : X.Opens} (hW : W ≤ V) (m : Γ(P, W)) :
    Scheme.Modules.ihomEval P (𝟙_ X.Modules) W m
        ((Scheme.Modules.dual P).presheaf.map (homOfLE hW).op (dualSection hp hVU)) =
      coef hp hVU hW m • Scheme.Modules.unitSection W
theorem

exists_isFrameOn_dual

L135 ↗
AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isFrameOn_dual
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_exists_isFrameOn_dual
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open DualFrameAux in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isFrameOn_dual
    {X : Scheme.{u}} {P : X.Modules} {U V : X.Opens} {p : Γ(P, U)}
    (hp : Scheme.Modules.IsFrameOn p V) (hVU : V ≤ U) :
    ∃ q : Γ(Scheme.Modules.dual P, V), Scheme.Modules.IsFrameOn q V ∧
      Scheme.Modules.ihomEval P (𝟙_ X.Modules) V (P.presheaf.map (homOfLE hVU).op p) q =
        Scheme.Modules.unitSection V

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