Module

Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top

5 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules is Iso of is Frame On of i Sup eq top

Imports1

Nyll.SchemeTheory.Modules.TensorSections

Imported by12

theorem

map_map

L33 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top.N2P4.map_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace N2P4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {P Q : X.Modules}

Lean source · statement

theorem map_map (M : X.Modules) {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (y : Γ(M,
  V₁)) :
    M.presheaf.map (homOfLE h₃₂).op (M.presheaf.map (homOfLE h₂₁).op y) =
      M.presheaf.map (homOfLE (h₃₂.trans h₂₁)).op y

theorem

app_map

L40 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top.N2P4.app_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace N2P4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {P Q : X.Modules}

Lean source · statement

theorem app_map (μ : P ⟶ Q) {V W : X.Opens} (h : W ≤ V) (x : Γ(P, V)) :
    μ.app W (P.presheaf.map (homOfLE h).op x) = Q.presheaf.map (homOfLE h).op (μ.app V x)

theorem

app_injective_of_le

L45 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top.N2P4.app_injective_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace N2P4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {P Q : X.Modules}

Lean source · statement

theorem app_injective_of_le (μ : P ⟶ Q) {V : X.Opens} (p : Γ(P, V)) (q : Γ(Q, V))
    (hp : IsFrameOn p V) (hq : IsFrameOn q V) (hμ : μ.app V p = q) {W : X.Opens} (hW : W ≤ V) :
    Function.Injective (μ.app W)

theorem

isIso_of_frames

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top.N2P4.isIso_of_frames

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
universe u v
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace N2P4
open AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {P Q : X.Modules}

Lean source · statement

theorem isIso_of_frames (μ : P ⟶ Q) {ι : Type v} (𝒱 : ι → X.Opens) (hcov : ⨆ i, 𝒱 i = ⊤)
    (p : ∀ i, Γ(P, 𝒱 i)) (q : ∀ i, Γ(Q, 𝒱 i))
    (hp : ∀ i, IsFrameOn (p i) (𝒱 i)) (hq : ∀ i, IsFrameOn (q i) (𝒱 i))
    (hμ : ∀ i, μ.app (𝒱 i) (p i) = q i) : IsIso μ

theorem

isIso_of_isFrameOn_of_iSup_eq_top

L110 ↗

AlgebraicGeometry.Scheme.Modules.isIso_of_isFrameOn_of_iSup_eq_top

Source context 5 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_of_isFrameOn_of_iSup_eq_top {X : Scheme.{u}}
  {P Q : X.Modules} (μ : P ⟶ Q) {ι : Type v} (𝒱 : ι → X.Opens) (hcov : ⨆ i, 𝒱 i = ⊤)
    (p : ∀ i, Γ(P, 𝒱 i)) (q : ∀ i, Γ(Q, 𝒱 i))
    (hp : ∀ i, Scheme.Modules.IsFrameOn (p i) (𝒱 i)) (hq : ∀ i, Scheme.Modules.IsFrameOn (q i) (𝒱
      i))
    (hμ : ∀ i, μ.app (𝒱 i) (p i) = q i) : IsIso μ

Module documentation

Scheme Modules is Iso of is Frame On of i Sup eq top

Declarations

map_map

app_map

app_injective_of_le

isIso_of_frames

isIso_of_isFrameOn_of_iSup_eq_top