NYLL
Module

Scheme_Modules_exists_glueOfCocycle_twist_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_glueOfCocycle_twist_iso
5 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists glue Of Cocycle twist iso

Imports7
Imported by2

Declarations

theorem

map_smul'

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso.AlgebraicGeometry.Scheme.Modules.GlueT2.map_smul'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
  SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
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 GlueT2
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} (hBA : B ≤ A) (r : Γ(X, A)) (m : Γ(M, A)) :
    M.presheaf.map (homOfLE hBA).op (r • m) = X.presheaf.map (homOfLE hBA).op r • M.presheaf.map
      (homOfLE hBA).op m
theorem

map_refl

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso.AlgebraicGeometry.Scheme.Modules.GlueT2.map_refl
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
  SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
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 GlueT2
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_refl {A : X.Opens} (m : Γ(M, A)) : M.presheaf.map (homOfLE (le_refl A)).op m = m
theorem

isFrameOn_unit_smul

L90 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso.AlgebraicGeometry.Scheme.Modules.GlueT2.isFrameOn_unit_smul
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
  SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
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 GlueT2
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 isFrameOn_unit_smul {A : X.Opens} {s : Γ(M, A)} (hs : IsFrameOn s A) (g : Γ(X, A)) (hg :
  IsUnit g) :
    IsFrameOn (g • s) A
lemma

iso_hom_inv_app_apply

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso.AlgebraicGeometry.Scheme.Modules.GlueT2.iso_hom_inv_app_apply
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
  SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
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 GlueT2
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
lemma iso_hom_inv_app_apply {N N' : X.Modules} (e : N ≅ N') (A : X.Opens) (x : Γ(N, A)) :
    e.inv.app A (e.hom.app A x) = x
theorem

exists_glueOfCocycle_twist_iso

L113 ↗
AlgebraicGeometry.Scheme.Modules.exists_glueOfCocycle_twist_iso
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_glueOfCocycle_twist_iso
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp] PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply
  SheafOfModules.unit_ihomSectionsEquivFamily AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
open _root_.CategoryTheory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
universe u
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules
  AlgebraicGeometry.Scheme.Modules.GlueT2 AlgebraicGeometry.Scheme.Modules.GlueOfCocycle in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_glueOfCocycle_twist_iso
    {X : Scheme.{u}} {ι : Type u} {U : ι → X.Opens} (hU : ⨆ i, U i = ⊤) (c :
      Scheme.Modules.UnitCocycle U)
    (h : ∀ i, Γ(X, U i)ˣ) :
    ∃ φ : Scheme.Modules.glueOfCocycle (c.twist h) ≅ Scheme.Modules.glueOfCocycle c,
      ∀ i, φ.hom.app (U i) (Scheme.Modules.glueFrame (c.twist h) i) =
        (↑(h i)⁻¹ : Γ(X, U i)) • Scheme.Modules.glueFrame c i

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