Module

Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn

3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists unit Cocycle map eq smul of is Frame On

Imports4

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Choose
Nyll.SchemeTheory.Modules.TensorSections
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesGlueOfCocycle

Imported by2

theorem

map_smul'

L64 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn.AlgebraicGeometry.Scheme.Modules.RatioCocycle.map_smul'

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RatioCocycle
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem map_smul' {A B : X.Opens} (h : B ≤ A) (r : Γ(X, A)) (m : Γ(M, A)) :
    M.presheaf.map (homOfLE h).op (r • m) = X.presheaf.map (homOfLE h).op r • M.presheaf.map
      (homOfLE h).op m

theorem

map_map

L69 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn.AlgebraicGeometry.Scheme.Modules.RatioCocycle.map_map

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RatioCocycle
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules.GlueOfCocycle
variable {X : Scheme.{u}} {M : X.Modules}

Lean source · statement

theorem map_map {A B C : X.Opens} (hBA : B ≤ A) (hCB : C ≤ B) (m : Γ(M, A)) :
    M.presheaf.map (homOfLE hCB).op (M.presheaf.map (homOfLE hBA).op m) = M.presheaf.map (homOfLE
      (hCB.trans hBA)).op m

theorem

exists_unitCocycle_map_eq_smul_of_isFrameOn

L77 ↗

AlgebraicGeometry.Scheme.Modules.exists_unitCocycle_map_eq_smul_of_isFrameOn

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_unitCocycle_map_eq_smul_of_isFrameOn
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe u
open AlgebraicGeometry.Scheme.Modules.RatioCocycle AlgebraicGeometry.Scheme.Modules.GlueOfCocycle in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_unitCocycle_map_eq_smul_of_isFrameOn
    {X : Scheme.{u}} {ι : Type u} {U : ι → X.Opens}
    {M : X.Modules} (e : ∀ i, Γ(M, U i)) (he : ∀ i, Scheme.Modules.IsFrameOn (e i) (U i)) :
    ∃ c : Scheme.Modules.UnitCocycle U, ∀ i j,
      M.presheaf.map (homOfLE (inf_le_right : U i ⊓ U j ≤ U j)).op (e j) =
        c.u i j • M.presheaf.map (homOfLE (inf_le_left : U i ⊓ U j ≤ U i)).op (e i)

Module documentation

Scheme Modules exists unit Cocycle map eq smul of is Frame On

Declarations

map_smul'

map_map

exists_unitCocycle_map_eq_smul_of_isFrameOn