NYLL
Module

Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
17 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Frame On nonempty iso tensor Unit of map eq mul

Imports11
Imported by4

Declarations

abbrev

res

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.res
Documentation

Restriction of module sections along an inclusion of opens.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
abbrev res (M : X.Modules) {V W : X.Opens} (h : W ≤ V) : Γ(M, V) → Γ(M, W)
abbrev

rO

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.rO
Documentation

Restriction of structure sheaf sections along an inclusion of opens.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
abbrev rO {V W : X.Opens} (h : W ≤ V) : Γ(X, V) → Γ(X, W)
theorem

res_res

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.res_res
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem res_res (M : X.Modules) {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (y : Γ(M, V₁))
  :
    res M h₃₂ (res M h₂₁ y) = res M (h₃₂.trans h₂₁) y
theorem

rO_rO

L62 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.rO_rO
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem rO_rO {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (g : Γ(X, V₁)) :
    rO h₃₂ (rO h₂₁ g) = rO (h₃₂.trans h₂₁) g
theorem

res_smul

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.res_smul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem res_smul (M : X.Modules) {V W : X.Opens} (h : W ≤ V) (g : Γ(X, V)) (y : Γ(M, V)) :
    res M h (g • y) = rO h g • res M h y
theorem

map_le_refl

L70 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.map_le_refl
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem map_le_refl (M : X.Modules) {V : X.Opens} (y : Γ(M, V)) :
    M.presheaf.map (homOfLE (le_refl V)).op y = y
theorem

res_irrel

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.res_irrel
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem res_irrel (M : X.Modules) {V W : X.Opens} (h h' : W ≤ V) (y : Γ(M, V)) : res M h y = res M
  h' y
theorem

isFrameOn_of_res

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.isFrameOn_of_res
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem isFrameOn_of_res {M : X.Modules} {T U : X.Opens} (hUT : U ≤ T) {s : Γ(M, T)}
    (h : IsFrameOn (res M hUT s) U) : IsFrameOn s U
theorem

isFrameOn_unit_smul

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.isFrameOn_unit_smul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem isFrameOn_unit_smul {M : X.Modules} {V : X.Opens} {s : Γ(M, V)} (hs : IsFrameOn s V)
    (g : Γ(X, V)) (hg : IsUnit g) : IsFrameOn (g • s) V
theorem

nonempty_iso_unit_of_isFrameOn_top

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.nonempty_iso_unit_of_isFrameOn_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem nonempty_iso_unit_of_isFrameOn_top {N : X.Modules} (s : Γ(N, ⊤)) (hs : IsFrameOn s ⊤) :
    Nonempty (N ≅ 𝟙_ X.Modules)
def

U2

L121 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.U2
Documentation

The two member open family consisting of U and V, indexed by Bool.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
def U2 (U V : X.Opens) : Bool → X.Opens
theorem

iSup_U2

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.iSup_U2
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem iSup_U2 (U V : X.Opens) : iSup (U2 U V) = U ⊔ V
theorem

res_tensorSections_eq_mul_smul

L128 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.res_tensorSections_eq_mul_smul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem res_tensorSections_eq_mul_smul {L L' : X.Modules} {U V : X.Opens}
    (sU : Γ(L, U)) (sV : Γ(L, V)) (sU' : Γ(L', U)) (sV' : Γ(L', V)) (t t' : Γ(X, U ⊓ V))
    (ht : res L inf_le_left sU = t • res L inf_le_right sV)
    (ht' : res L' inf_le_left sU' = t' • res L' inf_le_right sV') :
    res (L ⊗ L') (inf_le_left : U ⊓ V ≤ U) (tensorSections sU sU') =
      (t * t') • res (L ⊗ L') (inf_le_right : U ⊓ V ≤ V) (tensorSections sV sV')
theorem

exists_units_of_nonempty_iso_unit

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.exists_units_of_nonempty_iso_unit
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem exists_units_of_nonempty_iso_unit {L : X.Modules} {U V : X.Opens}
    {sU : Γ(L, U)} {sV : Γ(L, V)} (hsU : IsFrameOn sU U) (hsV : IsFrameOn sV V) (t : Γ(X, U ⊓ V))
    (ht : res L inf_le_left sU = t • res L inf_le_right sV) (e : L ≅ 𝟙_ X.Modules) :
    ∃ (a : Γ(X, U)) (b : Γ(X, V)), IsUnit a ∧ IsUnit b ∧
      rO (inf_le_left : U ⊓ V ≤ U) a = t * rO (inf_le_right : U ⊓ V ≤ V) b
theorem

nonempty_iso_unit_of_units

L168 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.nonempty_iso_unit_of_units
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem nonempty_iso_unit_of_units {L : X.Modules} {U V : X.Opens} (hUV : U ⊔ V = ⊤)
    {sU : Γ(L, U)} {sV : Γ(L, V)} (hsU : IsFrameOn sU U) (hsV : IsFrameOn sV V) (t : Γ(X, U ⊓ V))
    (ht : res L inf_le_left sU = t • res L inf_le_right sV)
    (a : Γ(X, U)) (b : Γ(X, V)) (ha : IsUnit a) (hb : IsUnit b)
    (hab : rO (inf_le_left : U ⊓ V ≤ U) a = t * rO (inf_le_right : U ⊓ V ≤ V) b) :
    Nonempty (L ≅ 𝟙_ X.Modules)
theorem

nonempty_iso_of_same_transition

L226 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul.TwoChartCocycle.nonempty_iso_of_same_transition
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace TwoChartCocycle
variable {X : Scheme.{u}}
Lean source · statement
theorem nonempty_iso_of_same_transition {L L' : X.Modules} {U V : X.Opens} (hUV : U ⊔ V = ⊤)
    {sU : Γ(L, U)} {sV : Γ(L, V)} (hsU : IsFrameOn sU U) (hsV : IsFrameOn sV V)
    {sU' : Γ(L', U)} {sV' : Γ(L', V)} (hsU' : IsFrameOn sU' U) (hsV' : IsFrameOn sV' V)
    (t : Γ(X, U ⊓ V))
    (ht : res L inf_le_left sU = t • res L inf_le_right sV)
    (ht' : res L' inf_le_left sU' = t • res L' inf_le_right sV') :
    Nonempty (L ≅ L')
theorem

nonempty_iso_tensorUnit_of_map_eq_mul

L300 ↗
AlgebraicGeometry.Scheme.Modules.IsFrameOn.nonempty_iso_tensorUnit_of_map_eq_mul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsFrameOn_nonempty_iso_tensorUnit_of_map_eq_mul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.nonempty_iso_tensorUnit_of_map_eq_mul
    {X : Scheme.{u}} {L : X.Modules} {U V : X.Opens} (hUV : U ⊔ V = ⊤)
    {sU : Γ(L, U)} {sV : Γ(L, V)} (hsU : Scheme.Modules.IsFrameOn sU U) (hsV :
      Scheme.Modules.IsFrameOn sV V)
    (t : Γ(X, U ⊓ V))
    (ht : L.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op sU =
      t • L.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op sV)
    (a : Γ(X, U)) (b : Γ(X, V)) (ha : IsUnit a) (hb : IsUnit b)
    (hab : X.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op a =
      t * X.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op b) :
    Nonempty (L ≅ 𝟙_ X.Modules)

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