NYLL
Module

Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.lean

Nyll.AlgebraicCurves.Geometry.Projective.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
102 declarations indexed from sourceView source ↗

Module documentation

Gluing an invertible scheme module from compatible projective chart modules and identifying its sections.

Imports13
Imported by4

Declarations

theorem

op_hom_eq

L67 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.op_hom_eq
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
Lean source · statement
theorem op_hom_eq {U V : Y.Opens} (i j : op U ⟶ op V) : i = j
theorem

map_endo

L70 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.map_endo
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L74 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.map_map
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L79 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.map_irrel
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L82 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ring_map_endo
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L86 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ring_map_map
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

app_naturality

L91 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.app_naturality
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L96 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_app_of_iso
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

L103 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_app_comp
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
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

isLocallyFreeOfRank_of_iso

L108 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.isLocallyFreeOfRank_of_iso
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
section Generic
variable {Y : Scheme.{u}}
omit U0 U1 in
Lean source · statement
theorem isLocallyFreeOfRank_of_iso {n : ℕ} {M N : Y.Modules} (e : M ≅ N)
    (h : Scheme.Modules.IsLocallyFreeOfRank n M) : Scheme.Modules.IsLocallyFreeOfRank n N
abbrev

ρ0

L116 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ρ0
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ρ0 :
    X.presheaf.obj (op U0) ⟶ X.presheaf.obj (op (U0 ⊓ U1))
abbrev

ρ1

L121 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ρ1
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ρ1 :
    X.presheaf.obj (op U1) ⟶ X.presheaf.obj (op (U0 ⊓ U1))
abbrev

g0

L127 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g0
Documentation

The affine-spectrum morphism from the intersection ring to the first chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev g0 : Spec (X.presheaf.obj (op (U0 ⊓ U1))) ⟶ Spec (X.presheaf.obj (op U0))
abbrev

g1

L131 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g1
Documentation

The affine-spectrum morphism from the intersection ring to the second chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev g1 : Spec (X.presheaf.obj (op (U0 ⊓ U1))) ⟶ Spec (X.presheaf.obj (op U1))
theorem

g0_f0

L136 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g0_f0
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
Lean source · statement
theorem g0_f0 : g0 U0 U1 ≫ hU0.fromSpec = hU01.fromSpec
theorem

g1_f1

L138 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g1_f1
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
Lean source · statement
theorem g1_f1 : g1 U0 U1 ≫ hU1.fromSpec = hU01.fromSpec
theorem

g1_f1_eq_g0_f0

L141 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g1_f1_eq_g0_f0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU01 in
Lean source · statement
theorem g1_f1_eq_g0_f0 : g1 U0 U1 ≫ hU1.fromSpec = g0 U0 U1 ≫ hU0.fromSpec
theorem

isOpenImmersion_g0

L144 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.isOpenImmersion_g0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU0 hU01 in
Lean source · statement
theorem isOpenImmersion_g0 : IsOpenImmersion (g0 U0 U1)
theorem

isOpenImmersion_g1

L148 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.isOpenImmersion_g1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU1 hU01 in
Lean source · statement
theorem isOpenImmersion_g1 : IsOpenImmersion (g1 U0 U1)
theorem

preimage_le_opensRange_of_comp

L152 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.preimage_le_opensRange_of_comp
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
omit U0 U1 in
Lean source · statement
theorem preimage_le_opensRange_of_comp {Y Z : Scheme.{u}} (g : Z ⟶ Y) (f : Y ⟶ X)
    [IsOpenImmersion f]
    [IsOpenImmersion g] (h : Z ⟶ X) [IsOpenImmersion h] (hgf : g ≫ f = h) {W : X.Opens}
    (hW : W ≤ h.opensRange) :
    f ⁻¹ᵁ W ≤ g.opensRange
theorem

preimage_f1_le_opensRange_g1

L163 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.preimage_f1_le_opensRange_g1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU01 in
Lean source · statement
theorem preimage_f1_le_opensRange_g1 [IsOpenImmersion (g1 U0 U1)] {W : X.Opens} (hW : W ≤ U0) :
    hU1.fromSpec ⁻¹ᵁ W ≤ (g1 U0 U1).opensRange
theorem

preimage_f0_le_opensRange_g0

L175 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.preimage_f0_le_opensRange_g0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU01 in
Lean source · statement
theorem preimage_f0_le_opensRange_g0 [IsOpenImmersion (g0 U0 U1)] {W : X.Opens} (hW : W ≤ U1) :
    hU0.fromSpec ⁻¹ᵁ W ≤ (g0 U0 U1).opensRange
abbrev

M0

L190 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.M0
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.M0 : (Spec
    (X.presheaf.obj (op U0))).Modules
abbrev

M1

L194 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.M1
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.M1 : (Spec
    (X.presheaf.obj (op U1))).Modules
abbrev

Q0

L199 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.Q0
Documentation

The first chart module extended to the intersection section ring.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev Q0 : ModuleCat (X.presheaf.obj (op (U0 ⊓ U1)))
abbrev

Q1

L202 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.Q1
Documentation

The second chart module extended to the intersection section ring.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev Q1 : ModuleCat (X.presheaf.obj (op (U0 ⊓ U1)))
abbrev

T0

L208 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.T0
Documentation

The quasicoherent module on the intersection spectrum associated with the first extended chart module.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev T0 : (Spec (X.presheaf.obj (op (U0 ⊓ U1)))).Modules
abbrev

N0

L211 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.N0
Documentation

The first affine chart module pushed forward to the whole scheme.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev N0 : X.Modules
abbrev

N1

L214 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.N1
Documentation

The second affine chart module pushed forward to the whole scheme.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev N1 : X.Modules
abbrev

N01

L217 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.N01
Documentation

The intersection module pushed forward to the whole scheme through the first chart.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev N01 : X.Modules
abbrev

β0

L220 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.β0
Documentation

The canonical pullback isomorphism from the first chart module to its intersection module.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
abbrev β0 : (Scheme.Modules.pullback (g0 U0 U1)).obj (M0 U0 P0) ≅ T0 U0 U1 P0
def

a0

L226 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.a0
Documentation

The adjunction-unit morphism from the first chart module to its pushed-forward intersection module.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
def a0 : M0 U0 P0 ⟶ (pushforward (g0 U0 U1)).obj (T0 U0 U1 P0)
def

a

L231 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.a
Documentation

The first restriction morphism between modules pushed forward to the whole scheme.

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
def a : N0 U0 hU0 P0 ⟶ N01 U0 U1 hU0 P0
theorem

a_app

L234 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.a_app
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
theorem a_app (W : X.Opens) :
    (a U0 U1 hU0 P0).app W =
      ((pullbackPushforwardAdjunction (g0 U0 U1)).unit.app (M0 U0 P0)).app (hU0.fromSpec ⁻¹ᵁ W) ≫
        (β0 U0 U1 P0).hom.app ((g0 U0 U1) ⁻¹ᵁ (hU0.fromSpec ⁻¹ᵁ W))
theorem

a_app_apply

L241 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.a_app_apply
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
Lean source · statement
theorem a_app_apply (W : X.Opens) (s : Γ(N0 U0 hU0 P0, W)) :
    (a U0 U1 hU0 P0).app W s =
      ((β0 U0 U1 P0).hom.app ((g0 U0 U1) ⁻¹ᵁ (hU0.fromSpec ⁻¹ᵁ W)))
        ((((pullbackPushforwardAdjunction (g0 U0 U1)).unit.app (M0 U0 P0)).app (hU0.fromSpec ⁻¹ᵁ W))
          s)
def

σinv

L259 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.σinv
Documentation

The inverse overlap equivalence, bundled as a morphism of modules over the intersection ring.

Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def σinv : Q1 U0 U1 P1 ⟶ Q0 U0 U1 P0
theorem

σinv_apply

L266 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.σinv_apply
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem σinv_apply (x : Q1 U0 U1 P1) :
    letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
    σinv U0 U1 P0 P1 σ x = σ.symm x := rfl
theorem

bijective_σinv

L270 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_σinv
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_σinv : Function.Bijective (σinv U0 U1 P0 P1 σ)
instance

(anonymous instance)

L274 ↗
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
instance : IsIso (σinv U0 U1 P0 P1 σ)
def

β1

L280 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.β1
Documentation

The second chart pullback morphism to the first intersection module, using the overlap equivalence.

Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def β1 : (Scheme.Modules.pullback (g1 U0 U1)).obj (M1 U1 P1) ⟶ T0 U0 U1 P0
instance

(anonymous instance)

L284 ↗
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
instance : IsIso (β1 U0 U1 P0 P1 σ)
def

b0

L293 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.b0
Documentation

The adjunction-unit morphism from the second chart module to the common intersection module.

Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def b0 : M1 U1 P1 ⟶ (pushforward (g1 U0 U1)).obj (T0 U0 U1 P0)
def

b

L298 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.b
Documentation

The second restriction morphism to the common pushed-forward intersection module.

Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def b : N1 U1 hU1 P1 ⟶ N01 U0 U1 hU0 P0
theorem

b_app

L303 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.b_app
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem b_app (W : X.Opens) :
    (b U0 U1 hU0 hU1 hU01 P0 P1 σ).app W =
      ((pullbackPushforwardAdjunction (g1 U0 U1)).unit.app (M1 U1 P1)).app (hU1.fromSpec ⁻¹ᵁ W) ≫
        (β1 U0 U1 P0 P1 σ).app ((g1 U0 U1) ⁻¹ᵁ (hU1.fromSpec ⁻¹ᵁ W)) ≫
        (T0 U0 U1 P0).presheaf.map (eqToHom (congrArg (fun f => f ⁻¹ᵁ W)
          (g1_f1_eq_g0_f0 U0 U1 hU0 hU1 hU01).symm)).op := by
  simp only [b, b0, Scheme.Modules.Hom.comp_app, pushforward_map_app, pushforwardCongr_hom_app_app]
  rfl
theorem

b_app_apply

L312 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.b_app_apply
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem b_app_apply (W : X.Opens) (s : Γ(N1 U1 hU1 P1, W)) :
    (b U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s =
      (T0 U0 U1 P0).presheaf.map (eqToHom (congrArg (fun f => f ⁻¹ᵁ W)
          (g1_f1_eq_g0_f0 U0 U1 hU0 hU1 hU01).symm)).op
      (((β1 U0 U1 P0 P1 σ).app ((g1 U0 U1) ⁻¹ᵁ (hU1.fromSpec ⁻¹ᵁ W)))
        ((((pullbackPushforwardAdjunction (g1 U0 U1)).unit.app (M1 U1 P1)).app (hU1.fromSpec ⁻¹ᵁ W))
          s)) := by
  rw [b_app]
  rfl
theorem

bijective_a_app

L322 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_a_app
Source context 33 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
include hU01 in
Lean source · statement
theorem bijective_a_app {W : X.Opens} (hW : W ≤ U1) :
    Function.Bijective ((a U0 U1 hU0 P0).app W)
theorem

bijective_b_app

L333 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_b_app
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
section Sigma
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_b_app {W : X.Opens} (hW : W ≤ U0) :
    Function.Bijective ((b U0 U1 hU0 hU1 hU01 P0 P1 σ).app W)
theorem

glue_exists

L378 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.glue_exists
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem glue_exists : ∃ (L : X.Modules) (π₀ : L ⟶ N0 U0 hU0 P0) (π₁ : L ⟶ N1 U1 hU1 P1),
    π₀ ≫ a U0 U1 hU0 P0 = π₁ ≫ b U0 U1 hU0 hU1 hU01 P0 P1 σ ∧
      (∀ U : X.Opens, Function.Injective fun s : Γ(L, U) => (π₀.app U s, π₁.app U s)) ∧
      (∀ (U : X.Opens) (s₀ : Γ(N0 U0 hU0 P0, U)) (s₁ : Γ(N1 U1 hU1 P1, U)),
        (a U0 U1 hU0 P0).app U s₀ = (b U0 U1 hU0 hU1 hU01 P0 P1 σ).app U s₁ →
        ∃ s : Γ(L, U), π₀.app U s = s₀ ∧ π₁.app U s = s₁) :=
  Scheme.Modules.exists_fibreProduct_sections_bijective _ _
def

L

L387 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.L
Documentation

A scheme module chosen by the gluing existence theorem for the compatible chart modules.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def L : X.Modules
def

π0

L390 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π0
Documentation

The chosen projection from the glued module to the pushed-forward first chart module.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def π0 : L U0 U1 hU0 hU1 hU01 P0 P1 σ ⟶ N0 U0 hU0 P0
def

π1

L394 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π1
Documentation

The chosen projection from the glued module to the pushed-forward second chart module.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def π1 : L U0 U1 hU0 hU1 hU01 P0 P1 σ ⟶ N1 U1 hU1 P1
theorem

π_comm

L397 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π_comm
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem π_comm : π0 U0 U1 hU0 hU1 hU01 P0 P1 σ ≫ a U0 U1 hU0 P0 = π1 U0 U1 hU0 hU1 hU01 P0 P1 σ
    ≫ b U0 U1 hU0 hU1 hU01 P0 P1 σ
theorem

π_inj

L401 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π_inj
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem π_inj (W : X.Opens) : Function.Injective fun s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, W) =>
    ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s, (π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s) :=
  (glue_exists U0 U1 hU0 hU1 hU01 P0 P1 σ).choose_spec.choose_spec.choose_spec.2.1 W
theorem

π_lift

L405 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π_lift
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem π_lift (W : X.Opens) (s₀ : Γ(N0 U0 hU0 P0, W)) (s₁ : Γ(N1 U1 hU1 P1, W))
    (h : (a U0 U1 hU0 P0).app W s₀ = (b U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s₁) :
    ∃ s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, W), (π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s = s₀ ∧ (π1
      U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s = s₁
theorem

π_comm_app

L411 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.π_comm_app
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem π_comm_app (W : X.Opens) (s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, W)) :
    (a U0 U1 hU0 P0).app W ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s) = (b U0 U1 hU0 hU1 hU01 P0
      P1 σ).app W ((π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W s)
theorem

bijective_π0_app

L418 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_π0_app
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_π0_app {W : X.Opens} (hW : W ≤ U0) :
    Function.Bijective ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W)
theorem

bijective_π1_app

L431 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_π1_app
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_π1_app {W : X.Opens} (hW : W ≤ U1) :
    Function.Bijective ((π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app W)
theorem

nonempty_pullback_f0_iso

L444 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.nonempty_pullback_f0_iso
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem nonempty_pullback_f0_iso :
    Nonempty ((Scheme.Modules.pullback hU0.fromSpec).obj (L U0 U1 hU0 hU1 hU01 P0 P1 σ) ≅ M0 U0
      P0)
theorem

nonempty_pullback_f1_iso

L451 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.nonempty_pullback_f1_iso
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem nonempty_pullback_f1_iso :
    Nonempty ((Scheme.Modules.pullback hU1.fromSpec).obj (L U0 U1 hU0 hU1 hU01 P0 P1 σ) ≅ M1 U1
      P1)
theorem

isLocallyFreeOfRank_pullback_ι

L458 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.isLocallyFreeOfRank_pullback_ι
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
omit hU0 hU1 hU01 in
Lean source · statement
theorem isLocallyFreeOfRank_pullback_ι {U : X.Opens} (hU : IsAffineOpen U) (L : X.Modules) {n : ℕ}
    (h : Scheme.Modules.IsLocallyFreeOfRank n ((Scheme.Modules.pullback hU.fromSpec).obj L)) :
    Scheme.Modules.IsLocallyFreeOfRank n ((Scheme.Modules.pullback U.ι).obj L)
theorem

isInvertible_L

L477 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.isInvertible_L
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
variable (hsup : U0 ⊔ U1 = ⊤)
variable [Module.Finite (X.presheaf.obj (op U0)) P0] [Module.Projective (X.presheaf.obj (op U0)) P0]
variable [Module.Finite (X.presheaf.obj (op U1)) P1] [Module.Projective (X.presheaf.obj (op U1)) P1]
variable
  (hrk0 : ∀ (K : Type u) [Field K] [Algebra (X.presheaf.obj (op U0)) K],
    Module.finrank K (K ⊗[X.presheaf.obj (op U0)] P0) = 1)
  (hrk1 : ∀ (K : Type u) [Field K] [Algebra (X.presheaf.obj (op U1)) K],
    Module.finrank K (K ⊗[X.presheaf.obj (op U1)] P1) = 1)
include hsup hrk0 hrk1 in
Lean source · statement
theorem isInvertible_L : Scheme.Modules.IsInvertible (L U0 U1 hU0 hU1 hU01 P0 P1 σ)
theorem

Γsmul_def

L517 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.Γsmul_def
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · full declaration
theorem Γsmul_def (M : (Spec R).Modules) (r : R) (m : (moduleSpecΓFunctor (R := R)).obj M) :
    r • m = (((Spec R).presheaf.map (homOfLE (le_top : (⊤ : (Spec R).Opens) ≤ ⊤)).op)
      ((StructureSheaf.globalSectionsIso R).hom r)) • (show Γ(M, ⊤) from m) := rfl
theorem

ring_res_top_top

L521 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.ring_res_top_top
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
omit R in
Lean source · statement
theorem ring_res_top_top {Y : Scheme.{u}} (s : Y.presheaf.obj (op ⊤)) :
    (Y.presheaf.map (homOfLE (le_top : (⊤ : Y.Opens) ≤ ⊤)).op) s = s
theorem

Γsmul_def'

L525 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.Γsmul_def'
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · full declaration
theorem Γsmul_def' (M : (Spec R).Modules) (r : R) (m : (moduleSpecΓFunctor (R := R)).obj M) :
    r • m = ((Scheme.ΓSpecIso R).inv r) • (show Γ(M, ⊤) from m) := by
  rw [Γsmul_def]
  exact congrArg (fun a : Γ(Spec R, ⊤) => a • (show Γ(M, ⊤) from m))
    (ring_res_top_top (Y := Spec R) ((StructureSheaf.globalSectionsIso R).hom r))
theorem

map_toOpen

L531 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.map_toOpen
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · statement
theorem map_toOpen (M : ModuleCat.{u} R) {U V : (Spec R).Opens} (i : op U ⟶ op V) (m : M) :
    (tilde M).presheaf.map i (tilde.toOpen M U m : Γ(tilde M, U)) = tilde.toOpen M V m
theorem

tilde_map_app_toOpen

L535 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.tilde_map_app_toOpen
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · statement
theorem tilde_map_app_toOpen {M N : ModuleCat.{u} R} (f : M ⟶ N) (U : (Spec R).Opens) (m : M) :
    (tilde.map f).app U (tilde.toOpen M U m : Γ(tilde M, U)) = tilde.toOpen N U (f m)
theorem

toOpen_top_injective

L540 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.toOpen_top_injective
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · statement
theorem toOpen_top_injective (M : ModuleCat.{u} R) : Function.Injective (tilde.toOpen M ⊤)
theorem

toOpen_isoTop_inv

L543 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.toOpen_isoTop_inv
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SpecGeneric
variable {R : CommRingCat.{u}}
Lean source · statement
theorem toOpen_isoTop_inv (M : ModuleCat.{u} R) (y : (modulesSpecToSheaf.obj (tilde
    M)).presheaf.obj (op ⊤)) :
    tilde.toOpen M ⊤ ((tilde.isoTop M).inv y) = y
theorem

pushforward_map_apply

L555 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.pushforward_map_apply
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SchemeGeneric
variable {Y Z : Scheme.{u}}
Lean source · statement
theorem pushforward_map_apply (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

bijective_map_of_eq

L560 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_map_of_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SchemeGeneric
variable {Y Z : 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_smul_def

L566 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.pushforward_smul_def
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SchemeGeneric
variable {Y Z : Scheme.{u}}
Lean source · full declaration
theorem pushforward_smul_def (f : Y ⟶ Z) (M : Y.Modules) (U : Z.Opens) (r : Z.presheaf.obj (op U))
    (x : Γ((pushforward f).obj M, U)) :
    r • x = (f.app U r) • (show Γ(M, f ⁻¹ᵁ U) from x) := rfl
theorem

fromSpec_app_res_top

L570 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.fromSpec_app_res_top
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section SchemeGeneric
variable {Y Z : Scheme.{u}}
Lean source · statement
theorem fromSpec_app_res_top {U : Y.Opens} (hU : IsAffineOpen U) (h : (⊤ : (Spec (Y.presheaf.obj
    (op U))).Opens) ≤ hU.fromSpec ⁻¹ᵁ U)
    (b : Y.presheaf.obj (op U)) :
    ((Spec (Y.presheaf.obj (op U))).presheaf.map (homOfLE h).op) (hU.fromSpec.app U b)
      = (Scheme.ΓSpecIso (Y.presheaf.obj (op U))).inv b
theorem

top_le_f0

L592 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.top_le_f0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem top_le_f0 : (⊤ : (Spec (X.presheaf.obj (op U0))).Opens) ≤ hU0.fromSpec ⁻¹ᵁ U0
theorem

top_le_f1

L594 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.top_le_f1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem top_le_f1 : (⊤ : (Spec (X.presheaf.obj (op U1))).Opens) ≤ hU1.fromSpec ⁻¹ᵁ U1
abbrev

G0

L598 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.G0
Documentation

The global section module of the first chart module on its affine spectrum.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
abbrev G0 : ModuleCat (X.presheaf.obj (op U0))
abbrev

G1

L601 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.G1
Documentation

The global section module of the second chart module on its affine spectrum.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
abbrev G1 : ModuleCat (X.presheaf.obj (op U1))
def

κ0

L607 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.κ0
Documentation

The linear comparison from sections of the glued module on the first chart to affine-spectrum sections.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
def κ0 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0) →ₗ[X.presheaf.obj (op U0)] G0 U0 P0 where
  toFun s := ((M0 U0 P0).presheaf.map (homOfLE (top_le_f0 U0 hU0)).op
      ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U0 s : Γ(M0 U0 P0, hU0.fromSpec ⁻¹ᵁ U0)) : Γ(M0 U0
        P0, ⊤))
  map_add' s t := by rw [map_add]; exact map_add _ _ _
  map_smul' r s := by
    simp only [RingHom.id_apply]
    rw [Scheme.Modules.Hom.app_smul, pushforward_smul_def, Scheme.Modules.map_smul,
      fromSpec_app_res_top]
    exact (Γsmul_def' (M0 U0 P0) r _).symm
theorem

κ0_apply

L618 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.κ0_apply
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem κ0_apply (s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0)) : (κ0 U0 U1 hU0 hU1 hU01 P0 P1 σ s :
    Γ(M0 U0 P0, ⊤)) =
    (M0 U0 P0).presheaf.map (homOfLE (top_le_f0 U0 hU0)).op
      ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U0 s : Γ(M0 U0 P0, hU0.fromSpec ⁻¹ᵁ U0))
theorem

bijective_κ0

L623 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_κ0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_κ0 : Function.Bijective (κ0 U0 U1 hU0 hU1 hU01 P0 P1 σ)
def

e0

L630 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.e0
Documentation

The linear equivalence identifying first-chart sections of the glued module with the given chart module.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def e0 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0) ≃ₗ[X.presheaf.obj (op U0)] (ModuleCat.of
    (X.presheaf.obj (op U0)) P0)
theorem

toOpen_e0

L636 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.toOpen_e0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem toOpen_e0 (s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0)) :
    (tilde.toOpen (ModuleCat.of (X.presheaf.obj (op U0)) P0) ⊤ (e0 U0 U1 hU0 hU1 hU01 P0 P1 σ s)
      : Γ(M0 U0 P0, ⊤)) =
      (M0 U0 P0).presheaf.map (homOfLE (top_le_f0 U0 hU0)).op
        ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U0 s : Γ(M0 U0 P0, hU0.fromSpec ⁻¹ᵁ U0))
def

κ1

L649 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.κ1
Documentation

The linear comparison from sections of the glued module on the second chart to affine-spectrum sections.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
def κ1 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1) →ₗ[X.presheaf.obj (op U1)] G1 U1 P1 where
  toFun s := ((M1 U1 P1).presheaf.map (homOfLE (top_le_f1 U1 hU1)).op
      ((π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U1 s : Γ(M1 U1 P1, hU1.fromSpec ⁻¹ᵁ U1)) : Γ(M1 U1
        P1, ⊤))
  map_add' s t := by rw [map_add]; exact map_add _ _ _
  map_smul' r s := by
    simp only [RingHom.id_apply]
    rw [Scheme.Modules.Hom.app_smul, pushforward_smul_def, Scheme.Modules.map_smul,
      fromSpec_app_res_top]
    exact (Γsmul_def' (M1 U1 P1) r _).symm
theorem

bijective_κ1

L660 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_κ1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_κ1 : Function.Bijective (κ1 U0 U1 hU0 hU1 hU01 P0 P1 σ)
def

e1

L667 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.e1
Documentation

The linear equivalence identifying second-chart sections of the glued module with the given chart module.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def e1 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1) ≃ₗ[X.presheaf.obj (op U1)] (ModuleCat.of
    (X.presheaf.obj (op U1)) P1)
theorem

toOpen_e1

L673 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.toOpen_e1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem toOpen_e1 (s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1)) :
    (tilde.toOpen (ModuleCat.of (X.presheaf.obj (op U1)) P1) ⊤ (e1 U0 U1 hU0 hU1 hU01 P0 P1 σ s)
      : Γ(M1 U1 P1, ⊤)) =
      (M1 U1 P1).presheaf.map (homOfLE (top_le_f1 U1 hU1)).op
        ((π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U1 s : Γ(M1 U1 P1, hU1.fromSpec ⁻¹ᵁ U1))
theorem

preimage_g0f0_inf

L683 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.preimage_g0f0_inf
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
include hU01 in
Lean source · statement
theorem preimage_g0f0_inf : (g0 U0 U1 ≫ hU0.fromSpec) ⁻¹ᵁ (U0 ⊓ U1) = ⊤
theorem

top_le_g0f0

L686 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.top_le_g0f0
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
include hU01 in
Lean source · statement
theorem top_le_g0f0 : (⊤ : (Spec (X.presheaf.obj (op (U0 ⊓ U1)))).Opens) ≤ (g0 U0 U1 ≫
    hU0.fromSpec) ⁻¹ᵁ (U0 ⊓ U1)
abbrev

G01

L691 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.G01
Documentation

The global section module of the common intersection module on its affine spectrum.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
abbrev G01 : ModuleCat (X.presheaf.obj (op (U0 ⊓ U1)))
theorem

g0f0_app_res_top

L694 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.g0f0_app_res_top
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
include hU01 in
Lean source · statement
theorem g0f0_app_res_top (r : X.presheaf.obj (op (U0 ⊓ U1))) :
    ((Spec (X.presheaf.obj (op (U0 ⊓ U1)))).presheaf.map (homOfLE (top_le_g0f0 U0 U1 hU0 hU01)).op)
      ((g0 U0 U1 ≫ hU0.fromSpec).app (U0 ⊓ U1) r)
      = (Scheme.ΓSpecIso (X.presheaf.obj (op (U0 ⊓ U1)))).inv r
def

κ01

L708 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.κ01
Documentation

The linear comparison from intersection sections of the glued module to affine-spectrum sections.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
def κ01 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0 ⊓ U1) →ₗ[X.presheaf.obj (op (U0 ⊓ U1))] G01 U0 U1
    P0 where
  toFun s := ((T0 U0 U1 P0).presheaf.map (homOfLE (top_le_g0f0 U0 U1 hU0 hU01)).op
      ((a U0 U1 hU0 P0).app (U0 ⊓ U1) ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app (U0 ⊓ U1) s) :
        Γ(T0 U0 U1 P0, (g0 U0 U1 ≫ hU0.fromSpec) ⁻¹ᵁ (U0 ⊓ U1))) : Γ(T0 U0 U1 P0, ⊤))
  map_add' s t := by rw [map_add, map_add]; exact map_add _ _ _
  map_smul' r s := by
    simp only [RingHom.id_apply]
    rw [Scheme.Modules.Hom.app_smul, Scheme.Modules.Hom.app_smul, pushforward_smul_def,
      Scheme.Modules.map_smul, g0f0_app_res_top U0 U1 hU0 hU01]
    exact (Γsmul_def' (T0 U0 U1 P0) r _).symm
theorem

bijective_κ01

L720 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.bijective_κ01
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem bijective_κ01 : Function.Bijective (κ01 U0 U1 hU0 hU1 hU01 P0 P1 σ)
def

e01

L728 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.e01
Documentation

The linear equivalence identifying intersection sections of the glued module with the extended first chart module.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
def e01 : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] (Q0 U0 U1
    P0)
theorem

toOpen_e01

L734 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.toOpen_e01
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem toOpen_e01 (s : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0 ⊓ U1)) :
    (tilde.toOpen (Q0 U0 U1 P0) ⊤ (e01 U0 U1 hU0 hU1 hU01 P0 P1 σ s) : Γ(T0 U0 U1 P0, ⊤)) =
      (T0 U0 U1 P0).presheaf.map (homOfLE (top_le_g0f0 U0 U1 hU0 hU01)).op
      ((a U0 U1 hU0 P0).app (U0 ⊓ U1) ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app (U0 ⊓ U1) s) :
        Γ(T0 U0 U1 P0, (g0 U0 U1 ≫ hU0.fromSpec) ⁻¹ᵁ (U0 ⊓ U1)))
theorem

pullbackSpecIso_hom_app_unit_toOpen

L769 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.pullbackSpecIso_hom_app_unit_toOpen
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
section KeyBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S) (M : ModuleCat.{u} R)
Lean source · statement
theorem pullbackSpecIso_hom_app_unit_toOpen (V : (Spec R).Opens) (m : M) :
    ((tilde.pullbackSpecIso φ M).hom.app ((Spec.map φ) ⁻¹ᵁ V))
      ((((pullbackPushforwardAdjunction (Spec.map φ)).unit.app (tilde M)).app V)
        (tilde.toOpen M V m : Γ(tilde M, V))) =
    (tilde.toOpen ((ModuleCat.extendScalars φ.hom).obj M) ((Spec.map φ) ⁻¹ᵁ V) ((1 : S) ⊗ₜ m) :
      Γ(tilde ((ModuleCat.extendScalars φ.hom).obj M), (Spec.map φ) ⁻¹ᵁ V))
theorem

res_π0_eq_toOpen

L799 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.res_π0_eq_toOpen
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem res_π0_eq_toOpen (m : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0)) {V : (Spec (X.presheaf.obj
    (op U0))).Opens}
    (i : op (hU0.fromSpec ⁻¹ᵁ U0) ⟶ op V) :
    (M0 U0 P0).presheaf.map i ((π0 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U0 m : Γ(M0 U0 P0,
      hU0.fromSpec ⁻¹ᵁ U0)) =
      tilde.toOpen (ModuleCat.of (X.presheaf.obj (op U0)) P0) V (e0 U0 U1 hU0 hU1 hU01 P0 P1 σ
        m)
theorem

res_π1_eq_toOpen

L817 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.res_π1_eq_toOpen
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem res_π1_eq_toOpen (m : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1)) {V : (Spec (X.presheaf.obj
    (op U1))).Opens}
    (i : op (hU1.fromSpec ⁻¹ᵁ U1) ⟶ op V) :
    (M1 U1 P1).presheaf.map i ((π1 U0 U1 hU0 hU1 hU01 P0 P1 σ).app U1 m : Γ(M1 U1 P1,
      hU1.fromSpec ⁻¹ᵁ U1)) =
      tilde.toOpen (ModuleCat.of (X.presheaf.obj (op U1)) P1) V (e1 U0 U1 hU0 hU1 hU01 P0 P1 σ
        m)
theorem

β1_app_unit_toOpen

L835 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.β1_app_unit_toOpen
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem β1_app_unit_toOpen (V : (Spec (X.presheaf.obj (op U1))).Opens) (p : P1) :
    ((β1 U0 U1 P0 P1 σ).app ((g1 U0 U1) ⁻¹ᵁ V))
      ((((pullbackPushforwardAdjunction (g1 U0 U1)).unit.app (M1 U1 P1)).app V)
        (tilde.toOpen (ModuleCat.of (X.presheaf.obj (op U1)) P1) V p : Γ(M1 U1 P1, V))) =
    (tilde.toOpen (Q0 U0 U1 P0) ((g1 U0 U1) ⁻¹ᵁ V)
      (σinv U0 U1 P0 P1 σ ((1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ p)) :
        Γ(T0 U0 U1 P0, (g1 U0 U1) ⁻¹ᵁ V))
theorem

sq0

L854 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.sq0
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem sq0 (m : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U0)) :
    e01 U0 U1 hU0 hU1 hU01 P0 P1 σ ((L U0 U1 hU0 hU1 hU01 P0 P1 σ).presheaf.map (homOfLE
      (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
      ((1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ[X.presheaf.obj (op U0)]
        (e0 U0 U1 hU0 hU1 hU01 P0 P1 σ m : ModuleCat.of (X.presheaf.obj (op U0)) P0) : Q0 U0 U1
          P0)
theorem

sq1

L877 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.sq1
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · statement
theorem sq1 (m : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1)) :
    e01 U0 U1 hU0 hU1 hU01 P0 P1 σ ((L U0 U1 hU0 hU1 hU01 P0 P1 σ).presheaf.map (homOfLE
      (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
      σinv U0 U1 P0 P1 σ ((1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ[X.presheaf.obj (op U1)]
        (e1 U0 U1 hU0 hU1 hU01 P0 P1 σ m : ModuleCat.of (X.presheaf.obj (op U1)) P1))
theorem

sq1'

L898 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.sq1'
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
Lean source · full declaration
theorem sq1' (m : Γ(L U0 U1 hU0 hU1 hU01 P0 P1 σ, U1)) :
    letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
    σ (e01 U0 U1 hU0 hU1 hU01 P0 P1 σ ((L U0 U1 hU0 hU1 hU01 P0 P1 σ).presheaf.map (homOfLE
      (inf_le_right : U0 ⊓ U1 ≤ U1)).op m)) =
      (1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ[X.presheaf.obj (op U1)]
        (e1 U0 U1 hU0 hU1 hU01 P0 P1 σ m : ModuleCat.of (X.presheaf.obj (op U1)) P1) := by
  rw [sq1]
  exact σ.apply_symm_apply _
theorem

exists_isInvertible_of_projective

L946 ↗
AlgebraicCurves.Geometry.Projective.Proofs.Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.exists_isInvertible_of_projective
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueInvertible
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible
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_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
variable (P0 : Type u) [AddCommGroup P0] [Module (X.presheaf.obj (op U0)) P0]
variable (P1 : Type u) [AddCommGroup P1] [Module (X.presheaf.obj (op U1)) P1]
variable (σ : letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
   ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
     ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U1)] P1))
variable (hsup : U0 ⊔ U1 = ⊤)
variable [Module.Finite (X.presheaf.obj (op U0)) P0] [Module.Projective (X.presheaf.obj (op U0)) P0]
variable [Module.Finite (X.presheaf.obj (op U1)) P1] [Module.Projective (X.presheaf.obj (op U1)) P1]
variable
  (hrk0 : ∀ (K : Type u) [Field K] [Algebra (X.presheaf.obj (op U0)) K],
    Module.finrank K (K ⊗[X.presheaf.obj (op U0)] P0) = 1)
  (hrk1 : ∀ (K : Type u) [Field K] [Algebra (X.presheaf.obj (op U1)) K],
    Module.finrank K (K ⊗[X.presheaf.obj (op U1)] P1) = 1)
include hU0 hU1 hU01 hsup hrk0 hrk1 in
Lean source · full declaration
theorem exists_isInvertible_of_projective :
    letI := (ρ0 U0 U1).hom.toAlgebra; letI := (ρ1 U0 U1).hom.toAlgebra
    ∃ (L : X.Modules), Scheme.Modules.IsInvertible L ∧
      ∃ (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] P0)
        (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] P1)
        (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))]
          ((X.presheaf.obj (op (U0 ⊓ U1))) ⊗[X.presheaf.obj (op U0)] P0)),
        (∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
          (1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ[X.presheaf.obj (op U0)] e0 m) ∧
        (∀ m, σ (e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m)) =
          (1 : X.presheaf.obj (op (U0 ⊓ U1))) ⊗ₜ[X.presheaf.obj (op U1)] e1 m) :=
  ⟨L U0 U1 hU0 hU1 hU01 P0 P1 σ, isInvertible_L U0 U1 hU0 hU1 hU01 P0 P1 σ hsup hrk0 hrk1, e0 U0
    U1 hU0 hU1 hU01 P0 P1 σ, e1 U0 U1 hU0 hU1 hU01 P0 P1 σ, e01 U0 U1 hU0 hU1 hU01 P0 P1 σ, sq0
      U0 U1 hU0 hU1 hU01 P0 P1 σ, sq1' U0 U1 hU0 hU1 hU01 P0 P1 σ⟩
theorem

exists_isInvertible_sectionsOf_equiv_of_projective

L968 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.exists_isInvertible_sectionsOf_equiv_of_projective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits _root_.AlgebraicGeometry
    AlgebraicGeometry TensorProduct Opposite in
open _root_.AlgebraicCurves.Geometry.Projective.Proofs in
open Scheme_TwoAffineOpenCover_exists_isInvertible_sectionsOf_equiv_of_projective in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · full declaration
theorem exists_isInvertible_sectionsOf_equiv_of_projective
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (P0 : Type u) [AddCommGroup P0] [Module (𝒱.cover c).A0 P0]
    [Module.Projective (𝒱.cover c).A0 P0] [Module.Finite (𝒱.cover c).A0 P0]
    (P1 : Type u) [AddCommGroup P1] [Module (𝒱.cover c).A1 P1]
    [Module.Projective (𝒱.cover c).A1 P1] [Module.Finite (𝒱.cover c).A1 P1]
    (hrk0 : ∀ (K : Type u) [Field K] [Algebra (𝒱.cover c).A0 K],
      Module.finrank K (K ⊗[(𝒱.cover c).A0] P0) = 1)
    (hrk1 : ∀ (K : Type u) [Field K] [Algebra (𝒱.cover c).A1 K],
      Module.finrank K (K ⊗[(𝒱.cover c).A1] P1) = 1)
    (σ : letI : Algebra (𝒱.cover c).A0 (𝒱.cover c).A01 := (𝒱.cover c).ρ0.toRingHom.toAlgebra
         letI : Algebra (𝒱.cover c).A1 (𝒱.cover c).A01 := (𝒱.cover c).ρ1.toRingHom.toAlgebra
         ((𝒱.cover c).A01 ⊗[(𝒱.cover c).A0] P0) ≃ₗ[(𝒱.cover c).A01]
           ((𝒱.cover c).A01 ⊗[(𝒱.cover c).A1] P1)) :
    letI : Algebra (𝒱.cover c).A0 (𝒱.cover c).A01 := (𝒱.cover c).ρ0.toRingHom.toAlgebra
    letI : Algebra (𝒱.cover c).A1 (𝒱.cover c).A01 := (𝒱.cover c).ρ1.toRingHom.toAlgebra
    ∃ (L : X.Modules), Scheme.Modules.IsInvertible L ∧
      ∃ (e0 : (𝒱.sectionsOf c L).M0 ≃ₗ[(𝒱.cover c).A0] P0)
        (e1 : (𝒱.sectionsOf c L).M1 ≃ₗ[(𝒱.cover c).A1] P1)
        (e01 : (𝒱.sectionsOf c L).M01 ≃ₗ[(𝒱.cover c).A01]
          ((𝒱.cover c).A01 ⊗[(𝒱.cover c).A0] P0)),
        (∀ m, e01 ((𝒱.sectionsOf c L).r0 m) = (1 : (𝒱.cover c).A01) ⊗ₜ[(𝒱.cover c).A0] e0 m) ∧
        (∀ m, σ (e01 ((𝒱.sectionsOf c L).r1 m)) = (1 : (𝒱.cover c).A01) ⊗ₜ[(𝒱.cover c).A1] e1 m)
          := by
  let i0 : Module (X.presheaf.obj (op 𝒱.U0)) P0 := ‹Module (𝒱.cover c).A0 P0›
  let i1 : Module (X.presheaf.obj (op 𝒱.U1)) P1 := ‹Module (𝒱.cover c).A1 P1›
  have : Module.Finite (X.presheaf.obj (op 𝒱.U0)) P0 := ‹Module.Finite (𝒱.cover c).A0 P0›
  have : Module.Projective (X.presheaf.obj (op 𝒱.U0)) P0 := ‹Module.Projective (𝒱.cover c).A0 P0›
  have : Module.Finite (X.presheaf.obj (op 𝒱.U1)) P1 := ‹Module.Finite (𝒱.cover c).A1 P1›
  have : Module.Projective (X.presheaf.obj (op 𝒱.U1)) P1 := ‹Module.Projective (𝒱.cover c).A1 P1›
  obtain ⟨L, hL, e0, e1, e01, h0, h1⟩ :=
    AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueInvertible.exists_isInvertible_of_projective
      𝒱.U0 𝒱.U1 𝒱.isAffineOpen_U0 𝒱.isAffineOpen_U1 𝒱.isAffineOpen_inf P0 P1 σ 𝒱.sup_eq_top hrk0
        hrk1
  exact ⟨L, hL, e0, e1, e01, h0, h1⟩

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