Module

Scheme_Modules_exists_isFrameOn_of_isUnit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isFrameOn_of_isUnit

37 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists is Frame On of is Unit

Imports6

Lean.Elab.Command
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Tactic.Ext
Mathlib.Tactic.Ring
Nyll.SchemeTheory.Modules.TensorSections

Imported by2

abbrev

rO

L38 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO

Documentation

The ring homomorphism restricting regular functions along an inclusion of opens.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

abbrev rO {A B : X.Opens} (h : B ≤ A) : Γ(X, A) →+* Γ(X, B)

theorem

rO_rO

L41 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO_rO

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem rO_rO {A B C : X.Opens} (hBA : B ≤ A) (hCB : C ≤ B) (g : Γ(X, A)) :
    rO hCB (rO hBA g) = rO (hCB.trans hBA) g

theorem

rO_irrel

L46 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO_irrel

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem rO_irrel {A B : X.Opens} (h h' : B ≤ A) (g : Γ(X, A)) : rO h g = rO h' g

theorem

rO_refl

L48 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO_refl

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem rO_refl {A : X.Opens} (g : Γ(X, A)) : rO (le_refl A) g = g

theorem

leTU

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.leTU

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)

Lean source · statement

theorem leTU : T ⊓ (U ⊓ V) ≤ T ⊓ U

theorem

leTV

L57 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.leTV

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)

Lean source · statement

theorem leTV : T ⊓ (U ⊓ V) ≤ T ⊓ V

theorem

leW

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.leW

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)

Lean source · statement

theorem leW : T ⊓ (U ⊓ V) ≤ U ⊓ V

def

pairs

L61 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.pairs

Documentation

Pairs of local sections satisfying the gluing relation determined by the overlap section t.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)

Lean source · full declaration

def pairs : AddSubgroup (Γ(X, T ⊓ U) × Γ(X, T ⊓ V)) where
  carrier := {p | rO (leTU U V T) p.1 = rO (leW U V T) t * rO (leTV U V T) p.2}
  zero_mem' := by simp
  add_mem' := by
    intro p q hp hq
    simp only [Set.mem_ofPred_eq, Prod.fst_add, Prod.snd_add, map_add] at hp hq ⊢
    rw [hp, hq, mul_add]
  neg_mem' := by
    intro p hp
    simp only [Set.mem_ofPred_eq, Prod.fst_neg, Prod.snd_neg, map_neg] at hp ⊢
    rw [hp, mul_neg]

theorem

mem_pairs

L75 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.mem_pairs

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)
variable {U V t T}

Lean source · statement

theorem mem_pairs {p : Γ(X, T ⊓ U) × Γ(X, T ⊓ V)} :
    p ∈ pairs U V t T ↔ rO (leTU U V T) p.1 = rO (leW U V T) t * rO (leTV U V T) p.2

instance

(anonymous instance)

L80 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)
variable {U V t T}
variable (U V t T)

Lean source · full declaration

instance : SMul Γ(X, T) (pairs U V t T) where
  smul g p := ⟨(rO inf_le_left g * p.1.1, rO inf_le_left g * p.1.2), by
    have hp := p.2
    rw [mem_pairs] at hp ⊢
    simp only [map_mul, rO_rO]
    rw [hp]
    have : rO ((leTU U V T).trans inf_le_left) g = rO ((leTV U V T).trans inf_le_left) g := rfl
    rw [this]; ring⟩

theorem

smul_val

L89 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.smul_val

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)
variable {U V t T}
variable (U V t T)

Lean source · statement

theorem smul_val (g : Γ(X, T)) (p : pairs U V t T) :
    (g • p).1 = (rO inf_le_left g * p.1.1, rO inf_le_left g * p.1.2)

instance

(anonymous instance)

L92 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Pairs
variable (T : X.Opens)
variable {U V t T}
variable (U V t T)

Lean source · full declaration

instance : Module Γ(X, T) (pairs U V t T) where
  one_smul p := by apply Subtype.ext; rw [smul_val]; simp
  mul_smul a b p := by apply Subtype.ext; simp only [smul_val, map_mul]; ext <;> simp [mul_assoc]
  smul_zero a := by apply Subtype.ext; rw [smul_val]; simp
  smul_add a p q := by
    apply Subtype.ext
    simp only [smul_val, AddSubgroup.coe_add, Prod.fst_add, Prod.snd_add, mul_add, Prod.mk_add_mk]
  add_smul a b p := by
    apply Subtype.ext
    simp only [smul_val, map_add, add_mul, AddSubgroup.coe_add, Prod.mk_add_mk]
  zero_smul p := by apply Subtype.ext; rw [smul_val]; simp

def

resPairs

L107 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.resPairs

Documentation

The restriction homomorphism on compatible pairs of local sections.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · full declaration

def resPairs {T T' : X.Opens} (h : T' ≤ T) : pairs U V t T →+ pairs U V t T' where
  toFun p := ⟨(rO (inf_le_inf_right U h) p.1.1, rO (inf_le_inf_right V h) p.1.2), by
    have hp := p.2
    rw [mem_pairs] at hp ⊢
    rw [rO_rO, rO_rO]
    have e1 : rO ((leTU U V T').trans (inf_le_inf_right U h)) p.1.1 =
        rO (inf_le_inf_right (U ⊓ V) h) (rO (leTU U V T) p.1.1) := by rw [rO_rO]
    have e2 : rO ((leTV U V T').trans (inf_le_inf_right V h)) p.1.2 =
        rO (inf_le_inf_right (U ⊓ V) h) (rO (leTV U V T) p.1.2) := by rw [rO_rO]
    rw [e1, e2, hp, map_mul, rO_rO]⟩
  map_zero' := by apply Subtype.ext; simp
  map_add' p q := by apply Subtype.ext; simp

theorem

resPairs_val

L120 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.resPairs_val

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem resPairs_val {T T' : X.Opens} (h : T' ≤ T) (p : pairs U V t T) :
    (resPairs U V t h p).1 = (rO (inf_le_inf_right U h) p.1.1, rO (inf_le_inf_right V h) p.1.2)

def

prePt

L125 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.prePt

Documentation

The presheaf of abelian groups formed by pairs satisfying the overlap gluing relation.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · full declaration

def prePt : (Opens X)ᵒᵖ ⥤ Ab where
  obj T := AddCommGrpCat.of (pairs U V t T.unop)
  map {T T'} f := AddCommGrpCat.ofHom (resPairs U V t f.unop.le)
  map_id T := by
    ext p
    · exact rO_refl _
    · exact rO_refl _
  map_comp {T₁ T₂ T₃} f g := by
    ext p
    · exact (rO_rO _ _ _).symm
    · exact (rO_rO _ _ _).symm

instance

instModulePrePt

L137 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.instModulePrePt

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

instance instModulePrePt (T : (Opens X)ᵒᵖ) :
    Module (X.ringCatSheaf.obj.obj T) ((prePt U V t).obj T)

theorem

prePt_map_smul

L141 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.prePt_map_smul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem prePt_map_smul ⦃T T' : (Opens X)ᵒᵖ⦄ (f : T ⟶ T') (r : X.ringCatSheaf.obj.obj T) (m : (prePt
  U V t).obj T) :
    (prePt U V t).map f (r • m) = X.ringCatSheaf.obj.map f r • (prePt U V t).map f m

def

P

L151 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.P

Documentation

The module presheaf formed by compatible pairs of local sections.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

def P : PresheafOfModules X.ringCatSheaf.obj

theorem

prePt_isSheaf

L154 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.prePt_isSheaf

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem prePt_isSheaf : TopCat.Presheaf.IsSheaf (prePt U V t)

def

L

L222 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.L

Documentation

The module sheaf obtained by gluing with the overlap section t.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

def L : X.Modules

theorem

sections_eq

L225 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sections_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem sections_eq (T : X.Opens) : (Γ(L U V t, T) : Type u) = pairs U V t T

theorem

rO_rO_self

L229 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO_rO_self

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem rO_rO_self {A B : X.Opens} (h : B ≤ A) (h' : A ≤ B) (g : Γ(X, B)) : rO h (rO h' g) = g

theorem

rO_bijective_of_le_le

L232 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.rO_bijective_of_le_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem rO_bijective_of_le_le {A B : X.Opens} (h : B ≤ A) (h' : A ≤ B) : Function.Bijective (rO h)

def

tinv

L238 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.tinv

Documentation

The inverse of the overlap section, using the specified proof that it is a unit.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

def tinv (ht : IsUnit t) : Γ(X, U ⊓ V)

theorem

tinv_mul

L240 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.tinv_mul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem tinv_mul (ht : IsUnit t) : tinv U V t ht * t = 1

theorem

mul_tinv

L241 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.mul_tinv

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem mul_tinv (ht : IsUnit t) : t * tinv U V t ht = 1

def

sU

L247 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sU

Documentation

The local frame on U represented by the pair consisting of one and the inverse transition section.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

def sU (ht : IsUnit t) : Γ(L U V t, U)

def

sV

L255 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sV

Documentation

The local frame on V represented by the transition section and one.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

def sV : Γ(L U V t, V)

theorem

sU_val

L261 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sU_val

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem sU_val (ht : IsUnit t) : (sU U V t ht).1 = (1, tinv U V t ht)

theorem

sV_val

L262 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sV_val

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem sV_val : (sV U V t).1 = (rO (le_of_eq (inf_comm V U) : V ⊓ U ≤ U ⊓ V) t, 1)

theorem

L_map

L264 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.L_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem L_map {T T' : X.Opens} (h : T' ≤ T) (p : Γ(L U V t, T)) :
    ((L U V t).presheaf.map (homOfLE h).op p : Γ(L U V t, T')) = resPairs U V t h p

theorem

L_smul

L267 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.L_smul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · full declaration

theorem L_smul {T : X.Opens} (g : Γ(X, T)) (p : Γ(L U V t, T)) :
    ((g • p : Γ(L U V t, T)) : pairs U V t T) = g • (show pairs U V t T from p) := rfl

theorem

sV_res_eq_smul_sU_res

L270 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.sV_res_eq_smul_sU_res

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem sV_res_eq_smul_sU_res (ht : IsUnit t) :
    ((L U V t).presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op (sV U V t) : Γ(L U V t, U ⊓ V))
      =
      t • (L U V t).presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op (sU U V t ht)

theorem

isFrameOn_sU

L285 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.isFrameOn_sU

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem isFrameOn_sU (ht : IsUnit t) : Scheme.Modules.IsFrameOn (sU U V t ht) U

theorem

isFrameOn_sV

L319 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.isFrameOn_sV

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))
section Frames

Lean source · statement

theorem isFrameOn_sV : Scheme.Modules.IsFrameOn (sV U V t) V

theorem

exists_isFrameOn'_of_isUnit

L351 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit.TwoChartGlue.exists_isFrameOn'_of_isUnit

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace TwoChartGlue
variable {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V))

Lean source · statement

theorem exists_isFrameOn'_of_isUnit (ht : IsUnit t) :
    ∃ (M : X.Modules) (a : Γ(M, U)) (b : Γ(M, V)), Scheme.Modules.IsFrameOn a U ∧
      Scheme.Modules.IsFrameOn b V ∧
      (M.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op b : Γ(M, U ⊓ V)) =
        t • M.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op a

theorem

exists_isFrameOn_of_isUnit

L379 ↗

AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_of_isUnit

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isFrameOn_of_isUnit
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_isFrameOn_of_isUnit
    {X : Scheme.{u}} (U V : X.Opens) (t : Γ(X, U ⊓ V)) (ht : IsUnit t) :
    ∃ (M : X.Modules) (a : Γ(M, U)) (b : Γ(M, V)),
      Scheme.Modules.IsFrameOn a U ∧ Scheme.Modules.IsFrameOn b V ∧
      M.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op b =
        t • M.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op a

Module documentation

Scheme Modules exists is Frame On of is Unit

Declarations