Module

Scheme_Modules_IsFrameOn_of_iSup.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_of_iSup

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On of i Sup

Imports4

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Choose
Mathlib.Tactic.Conv
Nyll.SchemeTheory.Modules.TensorSections

Imported by6

theorem

map_map

L32 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_of_iSup.FrameL1Aux.map_map

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_of_iSup
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace FrameL1Aux
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem map_map {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

of_iSup

L41 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.of_iSup

Source context 5 commands