Module

Scheme_Modules_IsFrameOn_dual_eq_of_ihomEval_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_dual_eq_of_ihomEval_eq

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On dual eq of ihom Eval eq

Imports6

Mathlib.AlgebraicGeometry.Modules.Sheaf
Nyll.SchemeTheory.Modules.Monoidal
Nyll.SchemeTheory.Modules.TensorSections
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesIhomSections
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesDet
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesNormModule

Imported by3

lemma

presheaf_map_map_aux

L37 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_dual_eq_of_ihomEval_eq.presheaf_map_map_aux

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_dual_eq_of_ihomEval_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite

Lean source · statement

lemma presheaf_map_map_aux {X : Scheme.{u}} (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

theorem

dual_eq_of_ihomEval_eq

L42 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.dual_eq_of_ihomEval_eq