NYLL
Module

Scheme_Modules_exists_iso_app_eq_of_isFrameOn_of_eq_smul.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_iso_app_eq_of_isFrameOn_of_eq_smul
9 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists iso app eq of is Frame On of eq smul

Imports7
Imported by4

Declarations

theorem

map_le_refl

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.map_le_refl
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem map_le_refl {M : X.Modules} {W : X.Opens} (t : Γ(M, W)) :
    M.presheaf.map (homOfLE (le_refl W)).op t = t
theorem

isUnit_of_isFrameOn_smul

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.isUnit_of_isFrameOn_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem isUnit_of_isFrameOn_smul {M : X.Modules} {W : X.Opens} {p : Γ(M, W)} {u : Γ(X, W)}
    (hp : IsFrameOn p W) (hp' : IsFrameOn (u • p) W) : IsUnit u
def

theta

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.theta
Documentation

The internal-Hom section taking the specified local frame to the given section.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
def theta {W : X.Opens} (p : Γ(P, W)) (hp : IsFrameOn p W) (q : Γ(Q, W)) :
    Γ((ihom P).obj Q, W)
theorem

ihomEval_theta

L73 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.ihomEval_theta
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem ihomEval_theta {W : X.Opens} (p : Γ(P, W)) (hp : IsFrameOn p W) (q : Γ(Q, W)) :
    ihomEval P Q W p (theta p hp q) = q
theorem

eq_theta

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.eq_theta
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem eq_theta {W : X.Opens} (p : Γ(P, W)) (hp : IsFrameOn p W) (q : Γ(Q, W))
    {θ : Γ((ihom P).obj Q, W)} (h : ihomEval P Q W p θ = q) : θ = theta p hp q
theorem

map_theta

L81 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.map_theta
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem map_theta {W W' : X.Opens} (h : W' ≤ W) (p : Γ(P, W)) (hp : IsFrameOn p W) (q : Γ(Q, W))
    (hp' : IsFrameOn (P.presheaf.map (homOfLE h).op p) W') :
    ((ihom P).obj Q).presheaf.map (homOfLE h).op (theta p hp q) =
      theta (P.presheaf.map (homOfLE h).op p) hp' (Q.presheaf.map (homOfLE h).op q)
theorem

theta_indep

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.theta_indep
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem theta_indep {W : X.Opens} (p : Γ(P, W)) (hp : IsFrameOn p W) (q : Γ(Q, W))
    (u : Γ(X, W)) (hp' : IsFrameOn (u • p) W) :
    theta (u • p) hp' (u • q) = theta p hp q
theorem

main

L97 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry.FrameTorsorGlue.main
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
namespace AlgebraicGeometry
namespace FrameTorsorGlue
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} {P Q : X.Modules}
Lean source · statement
theorem main (S : ∀ W : X.Opens, Set (Γ(P, W) × Γ(Q, W)))
    (hframe : ∀ (W : X.Opens) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W →
      IsFrameOn pq.1 W ∧ IsFrameOn pq.2 W)
    (hcov : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧ (S W).Nonempty)
    (hres : ∀ (W W' : X.Opens) (h : W' ≤ W) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W →
      (P.presheaf.map (homOfLE h).op pq.1, Q.presheaf.map (homOfLE h).op pq.2) ∈ S W')
    (hunit : ∀ (W : X.Opens) (pq pq' : Γ(P, W) × Γ(Q, W)), pq ∈ S W → pq' ∈ S W →
      ∃ u : Γ(X, W), pq'.1 = u • pq.1 ∧ pq'.2 = u • pq.2) :
    ∃ e : P ≅ Q, ∀ (W : X.Opens) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W → e.hom.app W pq.1 = pq.2
theorem

exists_iso_app_eq_of_isFrameOn_of_eq_smul

L172 ↗
AlgebraicGeometry.Scheme.Modules.exists_iso_app_eq_of_isFrameOn_of_eq_smul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.FrameIso.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_iso_app_eq_of_isFrameOn_of_eq_smul
    {X : Scheme.{u}} {P Q : X.Modules} (S : ∀ W : X.Opens, Set (Γ(P, W) × Γ(Q, W)))
    (hframe : ∀ (W : X.Opens) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W →
      Scheme.Modules.IsFrameOn pq.1 W ∧ Scheme.Modules.IsFrameOn pq.2 W)
    (hcov : ∀ x : X, ∃ W : X.Opens, x ∈ W ∧ (S W).Nonempty)
    (hres : ∀ (W W' : X.Opens) (h : W' ≤ W) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W →
      (P.presheaf.map (homOfLE h).op pq.1, Q.presheaf.map (homOfLE h).op pq.2) ∈ S W')
    (hunit : ∀ (W : X.Opens) (pq pq' : Γ(P, W) × Γ(Q, W)), pq ∈ S W → pq' ∈ S W →
      ∃ u : Γ(X, W), pq'.1 = u • pq.1 ∧ pq'.2 = u • pq.2) :
    ∃ e : P ≅ Q, ∀ (W : X.Opens) (pq : Γ(P, W) × Γ(Q, W)), pq ∈ S W → e.hom.app W pq.1 = pq.2

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