Module

Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion

98 declarations indexed from sourceView source ↗

Module documentation

Gluing compatible module morphisms from an open cover and their restriction equations.

Imports2

Imported by2

theorem

op_hom_eq

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.op_hom_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem op_hom_eq {U V : Y.Opens} (i j : op U ⟶ op V) : i = j

theorem

map_endo

L54 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.map_endo

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem map_endo (M : Y.Modules) {U : Y.Opens} (i : op U ⟶ op U) (x : Γ(M, U)) :
    M.presheaf.map i x = x

theorem

map_map

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.map_map

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem map_map (M : Y.Modules) {U V W : Y.Opens} (i : op U ⟶ op V) (j : op V ⟶ op W) (x : Γ(M,
    U)) :
    M.presheaf.map j (M.presheaf.map i x) = M.presheaf.map (i ≫ j) x

theorem

map_irrel

L63 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.map_irrel

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem map_irrel (M : Y.Modules) {U V : Y.Opens} (i j : op U ⟶ op V) (x : Γ(M, U)) :
    M.presheaf.map i x = M.presheaf.map j x

theorem

ring_map_endo

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.ring_map_endo

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem ring_map_endo {U : Y.Opens} (i : op U ⟶ op U) (x : Y.presheaf.obj (op U)) :
    Y.presheaf.map i x = x

theorem

ring_map_map

L70 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.ring_map_map

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem ring_map_map {U V W : Y.Opens} (i : op U ⟶ op V) (j : op V ⟶ op W) (x : Y.presheaf.obj
    (op U)) :
    Y.presheaf.map j (Y.presheaf.map i x) = Y.presheaf.map (i ≫ j) x

theorem

map_comp_eq

L75 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.map_comp_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem map_comp_eq (M : Y.Modules) {U V W : Y.Opens} (i : op U ⟶ op V) (j : op V ⟶ op W) (k :
    op U ⟶ op W) :
    M.presheaf.map i ≫ M.presheaf.map j = M.presheaf.map k

theorem

app_naturality

L80 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.app_naturality

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem app_naturality {M N : Y.Modules} (φ : M ⟶ N) {U V : Y.Opens} (i : op U ⟶ op V) (x : Γ(M,
    U)) :
    φ.app V (M.presheaf.map i x) = N.presheaf.map i (φ.app U x)

theorem

bijective_app_of_iso

L85 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_app_of_iso

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem bijective_app_of_iso {M N : Y.Modules} (e : M ≅ N) (U : Y.Opens) :
    Function.Bijective (e.hom.app U)

theorem

bijective_app_comp

L92 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_app_comp

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem bijective_app_comp {M N K : Y.Modules} (φ : M ⟶ N) (ψ : N ⟶ K) (U : Y.Opens)
    (hφ : Function.Bijective (φ.app U)) (hψ : Function.Bijective (ψ.app U)) :
    Function.Bijective ((φ ≫ ψ).app U)

theorem

bijective_map_of_eq

L97 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_map_of_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem bijective_map_of_eq (M : Y.Modules) {U V : Y.Opens} (h : U = V) (i : op U ⟶ op V) :
    Function.Bijective (M.presheaf.map i)

theorem

pushforward_map_apply

L103 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.pushforward_map_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem pushforward_map_apply {Z : Scheme.{u}} (f : Y ⟶ Z) (M : Y.Modules) {U V : Z.Opens} (i :
    op U ⟶ op V)
    (x : Γ((pushforward f).obj M, U)) :
    ((pushforward f).obj M).presheaf.map i x = M.presheaf.map ((Opens.map f.base).map i.unop).op
      x

theorem

hu_app

L121 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.hu_app

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)
include hu in

Lean source · statement

theorem hu_app (U : X.Opens) (s : Γ(M, U)) : a.app U (u₀.app U s) = b.app U (u₁.app U s)

def

liftFun

L127 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftFun

Documentation

Lift compatible sections through the given fibre product projections.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

def liftFun (U : X.Opens) (s : Γ(M, U)) : Γ(G, U)

theorem

π₀_liftFun

L130 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π₀_liftFun

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem π₀_liftFun (U : X.Opens) (s : Γ(M, U)) : π₀.app U (liftFun a b π₀ π₁ hlift u₀ u₁ hu U s)
    = u₀.app U s

theorem

π₁_liftFun

L134 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π₁_liftFun

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem π₁_liftFun (U : X.Opens) (s : Γ(M, U)) : π₁.app U (liftFun a b π₀ π₁ hlift u₀ u₁ hu U s)
    = u₁.app U s

theorem

liftFun_eq_of

L138 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftFun_eq_of

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)
include hinj in

Lean source · statement

theorem liftFun_eq_of (U : X.Opens) (s : Γ(M, U)) (t : Γ(G, U)) (h₀ : π₀.app U t = u₀.app U s)
    (h₁ : π₁.app U t = u₁.app U s) : liftFun a b π₀ π₁ hlift u₀ u₁ hu U s = t

theorem

liftFun_add

L145 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftFun_add

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)
include hinj in

Lean source · statement

theorem liftFun_add (U : X.Opens) (s t : Γ(M, U)) :
    liftFun a b π₀ π₁ hlift u₀ u₁ hu U (s + t) =
      liftFun a b π₀ π₁ hlift u₀ u₁ hu U s + liftFun a b π₀ π₁ hlift u₀ u₁ hu U t

theorem

liftFun_smul

L152 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftFun_smul

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)
include hinj in

Lean source · statement

theorem liftFun_smul (U : X.Opens) (r : X.presheaf.obj (op U)) (s : Γ(M, U)) :
    liftFun a b π₀ π₁ hlift u₀ u₁ hu U (r • s) = r • liftFun a b π₀ π₁ hlift u₀ u₁ hu U s

theorem

liftFun_map

L158 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftFun_map

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)
include hinj in

Lean source · statement

theorem liftFun_map {U V : X.Opens} (i : op U ⟶ op V) (s : Γ(M, U)) :
    liftFun a b π₀ π₁ hlift u₀ u₁ hu V (M.presheaf.map i s) =
      G.presheaf.map i (liftFun a b π₀ π₁ hlift u₀ u₁ hu U s)

def

liftPresheafHom

L166 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.liftPresheafHom

Documentation

The presheaf morphism obtained by lifting compatible sections.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · full declaration

def liftPresheafHom : M.presheaf ⟶ G.presheaf where
  app U := AddCommGrpCat.ofHom
    { toFun := fun s => liftFun a b π₀ π₁ hlift u₀ u₁ hu U.unop s
      map_zero' := by
        have h := liftFun_add a b π₀ π₁ hinj hlift u₀ u₁ hu U.unop 0 0
        rw [add_zero] at h
        exact left_eq_add.mp h
      map_add' := fun s t => liftFun_add a b π₀ π₁ hinj hlift u₀ u₁ hu U.unop s t }
  naturality U V i := by
    ext s
    exact liftFun_map a b π₀ π₁ hinj hlift u₀ u₁ hu i s

def

lift

L179 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift

Documentation

The module morphism obtained by lifting compatible local morphisms.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

def lift : M ⟶ G

theorem

lift_app

L183 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift_app

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem lift_app (U : X.Opens) (s : Γ(M, U)) :
    (lift a b π₀ π₁ hinj hlift u₀ u₁ hu).app U s = liftFun a b π₀ π₁ hlift u₀ u₁ hu U s

theorem

lift_π₀

L186 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift_π₀

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem lift_π₀ : lift a b π₀ π₁ hinj hlift u₀ u₁ hu ≫ π₀ = u₀

theorem

lift_π₁

L190 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift_π₁

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem lift_π₁ : lift a b π₀ π₁ hinj hlift u₀ u₁ hu ≫ π₁ = u₁

theorem

lift_app_π₀

L194 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift_app_π₀

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem lift_app_π₀ (U : X.Opens) (s : Γ(M, U)) :
    π₀.app U ((lift a b π₀ π₁ hinj hlift u₀ u₁ hu).app U s) = u₀.app U s

theorem

lift_app_π₁

L198 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.lift_app_π₁

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Lift
variable {X : Scheme.{u}} {N₀ N₁ N₀₁ G M : X.Modules} (a : N₀ ⟶ N₀₁) (b : N₁ ⟶ N₀₁)
  (π₀ : G ⟶ N₀) (π₁ : G ⟶ N₁)
  (hinj : ∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s))
  (hlift : ∀ (U : X.Opens) (s₀ : Γ(N₀, U)) (s₁ : Γ(N₁, U)), a.app U s₀ = b.app U s₁ →
    ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁)
  (u₀ : M ⟶ N₀) (u₁ : M ⟶ N₁) (hu : u₀ ≫ a = u₁ ≫ b)

Lean source · statement

theorem lift_app_π₁ (U : X.Opens) (s : Γ(M, U)) :
    π₁.app U ((lift a b π₀ π₁ hinj hlift u₀ u₁ hu).app U s) = u₁.app U s

theorem

comp_app_apply

L208 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.comp_app_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]

Lean source · statement

theorem comp_app_apply {M N K : X.Modules} (φ : M ⟶ N) (ψ : N ⟶ K) (U : X.Opens) (x : Γ(M, U)) :
    (φ ≫ ψ).app U x = ψ.app U (φ.app U x)

def

resHom

L212 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.resHom

Documentation

Restrict sections between pushforwards whose image opens are ordered.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]

Lean source · statement

def resHom (hle : ∀ W : X.Opens, q ''ᵁ (q ⁻¹ᵁ W) ≤ p ''ᵁ (p ⁻¹ᵁ W)) (N : X.Modules) :
    (pushforward p).obj (N.restrict p) ⟶ (pushforward q).obj (N.restrict q)

theorem

resHom_apply

L238 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.resHom_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]

Lean source · statement

theorem resHom_apply (hle : ∀ W : X.Opens, q ''ᵁ (q ⁻¹ᵁ W) ≤ p ''ᵁ (p ⁻¹ᵁ W)) (N : X.Modules) (W
    : X.Opens)
    (s : Γ((pushforward p).obj (N.restrict p), W)) :
    (resHom p q hle N).app W s = N.presheaf.map (homOfLE (hle W)).op s

theorem

bijective_resHom_app

L243 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_resHom_app

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]

Lean source · statement

theorem bijective_resHom_app (hle : ∀ W : X.Opens, q ''ᵁ (q ⁻¹ᵁ W) ≤ p ''ᵁ (p ⁻¹ᵁ W)) (N :
    X.Modules)
    {W : X.Opens} (h : q ''ᵁ (q ⁻¹ᵁ W) = p ''ᵁ (p ⁻¹ᵁ W)) :
    Function.Bijective ((resHom p q hle N).app W)

theorem

unit_apply

L249 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.unit_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion q] in

Lean source · statement

theorem unit_apply (N : X.Modules) (W : X.Opens) (s : Γ(N, W)) :
    ((restrictAdjunction p).unit.app N).app W s = N.presheaf.map (homOfLE (p.image_preimage_le
      W)).op s

theorem

bijective_unit_app

L253 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_unit_app

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion q] in

Lean source · statement

theorem bijective_unit_app (N : X.Modules) {W : X.Opens} (hW : W ≤ p.opensRange) :
    Function.Bijective (((restrictAdjunction p).unit.app N).app W)

theorem

pushforward_app_apply

L261 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.pushforward_app_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · statement

theorem pushforward_app_apply {M N : A.Modules} (φ : M ⟶ N) (W : X.Opens) (x : Γ((pushforward
    p).obj M, W)) :
    ((pushforward p).map φ).app W x = φ.app (p ⁻¹ᵁ W) x

theorem

restrict_map_apply

L265 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrict_map_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion q] in

Lean source · statement

theorem restrict_map_apply (M : X.Modules) {U V : A.Opens} (i : op U ⟶ op V) (x : Γ(M.restrict
    p, U)) :
    (M.restrict p).presheaf.map i x = M.presheaf.map (p.opensFunctor.map i.unop).op x

theorem

image_comp_eq

L269 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.image_comp_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · statement

theorem image_comp_eq {C : Scheme.{u}} (g : C ⟶ A) (f : A ⟶ X) [IsOpenImmersion g]
    [IsOpenImmersion f]
    (U : C.Opens) : (g ≫ f) ''ᵁ U = f ''ᵁ (g ''ᵁ U)

theorem

image_eq_of_eq

L278 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.image_eq_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · statement

theorem image_eq_of_eq {p' q' : A ⟶ X} [IsOpenImmersion p'] [IsOpenImmersion q'] (h : p' = q')
    (V : A.Opens) :
    p' ''ᵁ V = q' ''ᵁ V

theorem

opensRange_eq_of_eq

L282 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.opensRange_eq_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · statement

theorem opensRange_eq_of_eq {p' q' : A ⟶ X} [IsOpenImmersion p'] [IsOpenImmersion q'] (h : p' =
    q') :
    p'.opensRange = q'.opensRange

theorem

preimage_eq_of_eq

L286 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.preimage_eq_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · statement

theorem preimage_eq_of_eq {p' q' : A ⟶ X} (h : p' = q') (W : X.Opens) : p' ⁻¹ᵁ W = q' ⁻¹ᵁ W

theorem

restrictComp_hom_apply

L289 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrictComp_hom_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion q] in

Lean source · full declaration

theorem restrictComp_hom_apply {C : Scheme.{u}} (g : C ⟶ A) [IsOpenImmersion g] (M : X.Modules)
    (V : C.Opens)
    (t : Γ(M.restrict (g ≫ p), V)) :
    (((restrictFunctorComp g p).hom.app M).app V t : Γ(M, p ''ᵁ (g ''ᵁ V))) =
      M.presheaf.map (eqToHom (image_comp_eq g p V).symm).op (show Γ(M, (g ≫ p) ''ᵁ V) from t)
        := rfl

theorem

restrictComp_inv_apply

L296 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrictComp_inv_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion q] in

Lean source · full declaration

theorem restrictComp_inv_apply {C : Scheme.{u}} (g : C ⟶ A) [IsOpenImmersion g] (M : X.Modules)
    (V : C.Opens)
    (t : Γ((M.restrict p).restrict g, V)) :
    (((restrictFunctorComp g p).inv.app M).app V t : Γ(M, (g ≫ p) ''ᵁ V)) =
      M.presheaf.map (eqToHom (image_comp_eq g p V)).op (show Γ(M, p ''ᵁ (g ''ᵁ V)) from t) := rfl

theorem

restrictCongr_hom_apply

L302 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrictCongr_hom_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · full declaration

theorem restrictCongr_hom_apply {p' q' : A ⟶ X} [IsOpenImmersion p'] [IsOpenImmersion q'] (h :
    p' = q')
    (M : X.Modules) (V : A.Opens) (t : Γ(M.restrict p', V)) :
    (((restrictFunctorCongr h).hom.app M).app V t : Γ(M, q' ''ᵁ V)) =
      M.presheaf.map (eqToHom (image_eq_of_eq h V).symm).op (show Γ(M, p' ''ᵁ V) from t) := rfl

theorem

restrictCongr_inv_apply

L308 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrictCongr_inv_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] [IsOpenImmersion q] in

Lean source · full declaration

theorem restrictCongr_inv_apply {p' q' : A ⟶ X} [IsOpenImmersion p'] [IsOpenImmersion q'] (h :
    p' = q')
    (M : X.Modules) (V : A.Opens) (t : Γ(M.restrict q', V)) :
    (((restrictFunctorCongr h).inv.app M).app V t : Γ(M, p' ''ᵁ V)) =
      M.presheaf.map (eqToHom (image_eq_of_eq h V)).op (show Γ(M, q' ''ᵁ V) from t) := rfl

theorem

restrict_app_apply

L314 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrict_app_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section ResHom
variable {X A B : Scheme.{u}} (p : A ⟶ X) (q : B ⟶ X) [IsOpenImmersion p] [IsOpenImmersion q]
omit [IsOpenImmersion p] in

Lean source · statement

theorem restrict_app_apply {M N : X.Modules} (φ : M ⟶ N) (V : B.Opens) (x : Γ(M.restrict q, V)) :
    ((restrictFunctor q).map φ).app V x = φ.app (q ''ᵁ V) x

abbrev

N0

L327 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.N0

Documentation

Pushforward of the module restricted to the first open subscheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

abbrev N0 (N : X.Modules) : X.Modules

abbrev

N1

L329 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.N1

Documentation

Pushforward of the module restricted to the second open subscheme.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

abbrev N1 (N : X.Modules) : X.Modules

abbrev

N01

L331 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.N01

Documentation

Pushforward of the module restricted to the overlap.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

abbrev N01 (N : X.Modules) : X.Modules

theorem

le_a

L333 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.le_a

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

theorem le_a (W : X.Opens) : (g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) ≤ f₀ ''ᵁ (f₀ ⁻¹ᵁ W)

theorem

le_b

L339 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.le_b

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
include hg in

Lean source · statement

theorem le_b (W : X.Opens) : (g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) ≤ f₁ ''ᵁ (f₁ ⁻¹ᵁ W)

def

a

L347 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.a

Documentation

The restriction morphism from the first chart to the overlap.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

def a (N : X.Modules) : N0 f₀ N ⟶ N01 f₀ g₀ N

def

b

L350 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.b

Documentation

The restriction morphism from the second chart to the overlap.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

def b (N : X.Modules) : N1 f₁ N ⟶ N01 f₀ g₀ N

theorem

a_apply

L352 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.a_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

theorem a_apply (N : X.Modules) (W : X.Opens) (s : Γ(N0 f₀ N, W)) :
    (a f₀ g₀ N).app W s = N.presheaf.map (homOfLE (le_a f₀ g₀ W)).op s

theorem

b_apply

L354 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.b_apply

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)

Lean source · statement

theorem b_apply (N : X.Modules) (W : X.Opens) (s : Γ(N1 f₁ N, W)) :
    (b f₀ f₁ g₀ g₁ hg N).app W s =
      N.presheaf.map (homOfLE (le_b f₀ f₁ g₀ g₁ hg W)).op s

theorem

opensRange_g₀f₀

L361 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.opensRange_g₀f₀

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
include hg hov in

Lean source · statement

theorem opensRange_g₀f₀ : (g₀ ≫ f₀).opensRange = f₀.opensRange ⊓ f₁.opensRange

theorem

eq_a

L367 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.eq_a

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
include g₁ hg hov in

Lean source · statement

theorem eq_a {W : X.Opens} (hW : W ≤ f₁.opensRange) : (g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) = f₀ ''ᵁ
    (f₀ ⁻¹ᵁ W)

theorem

eq_b

L374 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.eq_b

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
include g₁ hg hov in

Lean source · statement

theorem eq_b {W : X.Opens} (hW : W ≤ f₀.opensRange) : (g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) = f₁ ''ᵁ
    (f₁ ⁻¹ᵁ W)

theorem

bijective_a_app

L380 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_a_app

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
include g₁ hg hov in

Lean source · statement

theorem bijective_a_app (N : X.Modules) {W : X.Opens} (hW : W ≤ f₁.opensRange) :
    Function.Bijective ((a f₀ g₀ N).app W)

theorem

bijective_b_app

L384 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_b_app

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
include hov in

Lean source · statement

theorem bijective_b_app (N : X.Modules) {W : X.Opens} (hW : W ≤ f₀.opensRange) :
    Function.Bijective ((b f₀ f₁ g₀ g₁ hg N).app W)

theorem

glue_exists

L390 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.glue_exists

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · full declaration

theorem glue_exists : ∃ (G : X.Modules) (π₀ : G ⟶ N0 f₀ N) (π₁ : G ⟶ N1 f₁ N),
    π₀ ≫ a f₀ g₀ N = π₁ ≫ b f₀ f₁ g₀ g₁ hg N ∧
      (∀ U : X.Opens, Function.Injective fun s : Γ(G, U) => (π₀.app U s, π₁.app U s)) ∧
      (∀ (U : X.Opens) (s₀ : Γ(N0 f₀ N, U)) (s₁ : Γ(N1 f₁ N, U)),
        (a f₀ g₀ N).app U s₀ = (b f₀ f₁ g₀ g₁ hg N).app U s₁ →
        ∃ s : Γ(G, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁) :=
  Scheme.Modules.exists_fibreProduct_sections_bijective _ _

def

G

L399 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.G

Documentation

The fibre product module used to glue the two restricted modules.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def G : X.Modules

def

π₀

L401 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π₀

Documentation

The first projection from the fibre product module.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def π₀ : G f₀ f₁ g₀ g₁ hg N ⟶ N0 f₀ N

def

π₁

L403 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π₁

Documentation

The second projection from the fibre product module.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def π₁ : G f₀ f₁ g₀ g₁ hg N ⟶ N1 f₁ N

theorem

π_comm

L405 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π_comm

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem π_comm : π₀ f₀ f₁ g₀ g₁ hg N ≫ a f₀ g₀ N = π₁ f₀ f₁ g₀ g₁ hg N ≫ b f₀ f₁ g₀ g₁ hg N

theorem

π_inj

L407 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π_inj

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · full declaration

theorem π_inj (U : X.Opens) : Function.Injective fun s : Γ(G f₀ f₁ g₀ g₁ hg N, U) =>
    ((π₀ f₀ f₁ g₀ g₁ hg N).app U s, (π₁ f₀ f₁ g₀ g₁ hg N).app U s) :=
  (glue_exists f₀ f₁ g₀ g₁ hg N).choose_spec.choose_spec.choose_spec.2.1 U

theorem

π_lift

L410 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π_lift

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem π_lift (U : X.Opens) (s₀ : Γ(N0 f₀ N, U)) (s₁ : Γ(N1 f₁ N, U))
    (h : (a f₀ g₀ N).app U s₀ = (b f₀ f₁ g₀ g₁ hg N).app U s₁) :
    ∃ s : Γ(G f₀ f₁ g₀ g₁ hg N, U), (π₀ f₀ f₁ g₀ g₁ hg N).app U s = s₀ ∧ (π₁ f₀ f₁ g₀ g₁ hg
      N).app U s = s₁

theorem

π_comm_app

L416 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.π_comm_app

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem π_comm_app (W : X.Opens) (s : Γ(G f₀ f₁ g₀ g₁ hg N, W)) :
    (a f₀ g₀ N).app W ((π₀ f₀ f₁ g₀ g₁ hg N).app W s) =
      (b f₀ f₁ g₀ g₁ hg N).app W ((π₁ f₀ f₁ g₀ g₁ hg N).app W s)

theorem

bijective_π₀_app

L423 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_π₀_app

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
include hov in

Lean source · statement

theorem bijective_π₀_app {W : X.Opens} (hW : W ≤ f₀.opensRange) :
    Function.Bijective ((π₀ f₀ f₁ g₀ g₁ hg N).app W)

theorem

bijective_π₁_app

L436 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_π₁_app

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
include hov in

Lean source · statement

theorem bijective_π₁_app {W : X.Opens} (hW : W ≤ f₁.opensRange) :
    Function.Bijective ((π₁ f₀ f₁ g₀ g₁ hg N).app W)

def

η₀

L450 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.η₀

Documentation

The unit of restriction and pushforward for the first chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def η₀ : N ⟶ N0 f₀ N

def

η₁

L453 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.η₁

Documentation

The unit of restriction and pushforward for the second chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def η₁ : N ⟶ N1 f₁ N

theorem

η₀_apply

L455 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.η₀_apply

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem η₀_apply (W : X.Opens) (s : Γ(N, W)) :
    (η₀ f₀ N).app W s = N.presheaf.map (homOfLE (f₀.image_preimage_le W)).op s

theorem

η₁_apply

L457 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.η₁_apply

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem η₁_apply (W : X.Opens) (s : Γ(N, W)) :
    (η₁ f₁ N).app W s = N.presheaf.map (homOfLE (f₁.image_preimage_le W)).op s

theorem

η_comm

L460 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.η_comm

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem η_comm : η₀ f₀ N ≫ a f₀ g₀ N = η₁ f₁ N ≫ b f₀ f₁ g₀ g₁ hg N

def

can

L466 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.can

Documentation

The canonical morphism to the fibre product of the two restrictions.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

def can : N ⟶ G f₀ f₁ g₀ g₁ hg N

theorem

can_π₀

L470 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.can_π₀

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem can_π₀ : can f₀ f₁ g₀ g₁ hg N ≫ π₀ f₀ f₁ g₀ g₁ hg N = η₀ f₀ N

theorem

can_π₁

L471 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.can_π₁

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem can_π₁ : can f₀ f₁ g₀ g₁ hg N ≫ π₁ f₀ f₁ g₀ g₁ hg N = η₁ f₁ N

theorem

bijective_of_comp

L473 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.bijective_of_comp

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)

Lean source · statement

theorem bijective_of_comp {A B C : X.Modules} (v : A ⟶ B) (p : B ⟶ C) (w : A ⟶ C) (h : v ≫ p =
    w) (W : X.Opens)
    (hp : Function.Bijective (p.app W)) (hw : Function.Bijective (w.app W)) : Function.Bijective
      (v.app W)

theorem

isIso_can

L485 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.isIso_can

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
include hov hcov in

Lean source · statement

theorem isIso_can : IsIso (can f₀ f₁ g₀ g₁ hg N)

def

u₀

L509 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₀

Documentation

Pushforward of the first local morphism composed with the restriction unit.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

def u₀ : M ⟶ N0 f₀ N

def

u₁

L511 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₁

Documentation

Pushforward of the second local morphism composed with the restriction unit.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

def u₁ : M ⟶ N1 f₁ N

theorem

u₀_apply

L513 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₀_apply

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem u₀_apply (W : X.Opens) (s : Γ(M, W)) :
    (u₀ f₀ N ψ₀).app W s = ψ₀.app (f₀ ⁻¹ᵁ W) (M.presheaf.map (homOfLE (f₀.image_preimage_le
      W)).op s)

theorem

u₁_apply

L516 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₁_apply

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem u₁_apply (W : X.Opens) (s : Γ(M, W)) :
    (u₁ f₁ N ψ₁).app W s = ψ₁.app (f₁ ⁻¹ᵁ W) (M.presheaf.map (homOfLE (f₁.image_preimage_le
      W)).op s)

theorem

g₀_image_le

L520 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.g₀_image_le

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)
omit [IsOpenImmersion f₀] in

Lean source · statement

theorem g₀_image_le (W : X.Opens) : g₀ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) ≤ f₀ ⁻¹ᵁ W

theorem

g₁_image_le

L525 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.g₁_image_le

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)
omit [IsOpenImmersion f₀] [IsOpenImmersion f₁] [IsOpenImmersion g₀] in
include hg in

Lean source · statement

theorem g₁_image_le (W : X.Opens) : g₁ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W) ≤ f₁ ⁻¹ᵁ W

theorem

u₀_a_apply

L530 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₀_a_apply

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem u₀_a_apply (W : X.Opens) (s : Γ(M, W))
    (k₁ : op W ⟶ op (f₀ ''ᵁ (g₀ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))))
    (k₂ : op (f₀ ''ᵁ (g₀ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))) ⟶ op ((g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))) :
    (u₀ f₀ N ψ₀ ≫ a f₀ g₀ N).app W s =
      N.presheaf.map k₂ (ψ₀.app (g₀ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W)) (M.presheaf.map k₁ s))

theorem

u₁_b_apply

L556 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u₁_b_apply

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem u₁_b_apply (W : X.Opens) (s : Γ(M, W))
    (k₁ : op W ⟶ op (f₁ ''ᵁ (g₁ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))))
    (k₂ : op (f₁ ''ᵁ (g₁ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))) ⟶ op ((g₀ ≫ f₀) ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W))) :
    (u₁ f₁ N ψ₁ ≫ b f₀ f₁ g₀ g₁ hg N).app W s =
      N.presheaf.map k₂ (ψ₁.app (g₁ ''ᵁ ((g₀ ≫ f₀) ⁻¹ᵁ W)) (M.presheaf.map k₁ s))

theorem

hψ_app

L583 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.hψ_app

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)
include hψ in

Lean source · statement

theorem hψ_app (V : Y₀₁.Opens) (t : Γ(M, (g₀ ≫ f₀) ''ᵁ V))
    (e₁ : op ((g₀ ≫ f₀) ''ᵁ V) ⟶ op (f₀ ''ᵁ (g₀ ''ᵁ V)))
    (e₂ : op (f₀ ''ᵁ (g₀ ''ᵁ V)) ⟶ op ((g₀ ≫ f₀) ''ᵁ V))
    (e₃ : op ((g₀ ≫ f₀) ''ᵁ V) ⟶ op (f₁ ''ᵁ (g₁ ''ᵁ V)))
    (e₄ : op (f₁ ''ᵁ (g₁ ''ᵁ V)) ⟶ op ((g₀ ≫ f₀) ''ᵁ V)) :
    N.presheaf.map e₂ (ψ₀.app (g₀ ''ᵁ V) (M.presheaf.map e₁ t)) =
      N.presheaf.map e₄ (ψ₁.app (g₁ ''ᵁ V) (M.presheaf.map e₃ t))

theorem

u_comm

L608 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.u_comm

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)
include hψ in

Lean source · statement

theorem u_comm : u₀ f₀ N ψ₀ ≫ a f₀ g₀ N = u₁ f₁ N ψ₁ ≫ b f₀ f₁ g₀ g₁ hg N

def

v

L623 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.v

Documentation

The morphism to the fibre product induced by the compatible local morphisms.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

def v : M ⟶ G f₀ f₁ g₀ g₁ hg N

theorem

v_π₀

L628 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.v_π₀

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem v_π₀ : v f₀ f₁ g₀ g₁ hg N ψ₀ ψ₁ hψ ≫ π₀ f₀ f₁ g₀ g₁ hg N = u₀ f₀ N ψ₀

theorem

v_π₁

L629 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.v_π₁

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem v_π₁ : v f₀ f₁ g₀ g₁ hg N ψ₀ ψ₁ hψ ≫ π₁ f₀ f₁ g₀ g₁ hg N = u₁ f₁ N ψ₁

def

φ

L632 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.φ

Documentation

The glued morphism obtained by inverting the canonical fibre product comparison.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

def φ : M ⟶ N

theorem

φ_can

L636 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.φ_can

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem φ_can : φ f₀ f₁ g₀ g₁ hg hov N hcov ψ₀ ψ₁ hψ ≫ can f₀ f₁ g₀ g₁ hg N = v f₀ f₁ g₀ g₁ hg N
    ψ₀ ψ₁ hψ

theorem

φ_η₀

L641 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.φ_η₀

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem φ_η₀ : φ f₀ f₁ g₀ g₁ hg hov N hcov ψ₀ ψ₁ hψ ≫ η₀ f₀ N = u₀ f₀ N ψ₀

theorem

φ_η₁

L644 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.φ_η₁

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem φ_η₁ : φ f₀ f₁ g₀ g₁ hg hov N hcov ψ₀ ψ₁ hψ ≫ η₁ f₁ N = u₁ f₁ N ψ₁

theorem

restrict_φ₀

L647 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrict_φ₀

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem restrict_φ₀ : (restrictFunctor f₀).map (φ f₀ f₁ g₀ g₁ hg hov N hcov ψ₀ ψ₁ hψ) = ψ₀

theorem

restrict_φ₁

L668 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion.AlgebraicGeometry.Scheme.Modules.GlueHom.restrict_φ₁

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace GlueHom
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme.Modules
section Glue
variable {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀]
    [IsOpenImmersion f₁]
  (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
  (hg : g₀ ≫ f₀ = g₁ ≫ f₁)
variable (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
variable (N : X.Modules)
variable (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
variable {M : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
  (hψ : (restrictFunctorComp g₀ f₀).hom.app M ≫ (restrictFunctor g₀).map ψ₀ ≫
    (restrictFunctorComp g₀ f₀).inv.app N =
    (restrictFunctorCongr hg).hom.app M ≫ (restrictFunctorComp g₁ f₁).hom.app M ≫
      (restrictFunctor g₁).map ψ₁ ≫
      (restrictFunctorComp g₁ f₁).inv.app N ≫ (restrictFunctorCongr hg).inv.app N)

Lean source · statement

theorem restrict_φ₁ : (restrictFunctor f₁).map (φ f₀ f₁ g₀ g₁ hg hov N hcov ψ₀ ψ₁ hψ) = ψ₁

theorem

exists_hom_restrict_eq_of_isOpenImmersion

L700 ↗

AlgebraicGeometry.Scheme.Modules.exists_hom_restrict_eq_of_isOpenImmersion

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_hom_restrict_eq_of_isOpenImmersion
universe u v
noncomputable section
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open AlgebraicGeometry.Scheme.Modules.GlueHom in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_hom_restrict_eq_of_isOpenImmersion
    {X Y₀ Y₁ Y₀₁ : Scheme.{u}} (f₀ : Y₀ ⟶ X) (f₁ : Y₁ ⟶ X) [IsOpenImmersion f₀] [IsOpenImmersion f₁]
    (g₀ : Y₀₁ ⟶ Y₀) (g₁ : Y₀₁ ⟶ Y₁) [IsOpenImmersion g₀] [IsOpenImmersion g₁]
    (hg : g₀ ≫ f₀ = g₁ ≫ f₁) (hcov : f₀.opensRange ⊔ f₁.opensRange = ⊤)
    (hov : f₀.opensRange ⊓ f₁.opensRange ≤ (g₀ ≫ f₀).opensRange)
    {M N : X.Modules} (ψ₀ : M.restrict f₀ ⟶ N.restrict f₀) (ψ₁ : M.restrict f₁ ⟶ N.restrict f₁)
    (hψ : (Scheme.Modules.restrictFunctorComp g₀ f₀).hom.app M ≫ (Scheme.Modules.restrictFunctor
      g₀).map ψ₀ ≫
            (Scheme.Modules.restrictFunctorComp g₀ f₀).inv.app N =
          (Scheme.Modules.restrictFunctorCongr hg).hom.app M ≫
            (Scheme.Modules.restrictFunctorComp g₁ f₁).hom.app M ≫
              (Scheme.Modules.restrictFunctor g₁).map ψ₁ ≫
            (Scheme.Modules.restrictFunctorComp g₁ f₁).inv.app N ≫
              (Scheme.Modules.restrictFunctorCongr hg).inv.app N) :
    ∃ φ : M ⟶ N, (Scheme.Modules.restrictFunctor f₀).map φ = ψ₀ ∧
      (Scheme.Modules.restrictFunctor f₁).map φ = ψ₁

Module documentation

Declarations