Module

Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible

102 declarations indexed from sourceView source ↗

Module documentation

An isomorphism of invertible scheme modules obtained from compatible linear equivalences of chart sections.

Imports9

Imported by5

theorem

op_hom_eq

L60 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.op_hom_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

map_endo

L63 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.map_endo

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

map_map

L67 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.map_map

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

map_irrel

L72 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.map_irrel

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

ring_map_endo

L75 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ring_map_endo

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

ring_map_map

L79 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ring_map_map

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

ring_map_irrel

L84 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ring_map_irrel

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

app_naturality

L87 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.app_naturality

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

theorem

comp_app_apply

L92 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.comp_app_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

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

def

rsec

L96 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec

Documentation

A section of a restricted module, viewed over the image open in the original scheme.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

def rsec {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)
    (x : Γ(M.restrict p, V)) : Γ(M, p ''ᵁ V)

def

usec

L99 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.usec

Documentation

A section over the image open, viewed in the restricted module.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

def usec {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)
    (x : Γ(M, p ''ᵁ V)) : Γ(M.restrict p, V)

theorem

rsec_usec

L106 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec_usec

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem rsec_usec (x : Γ(M, p ''ᵁ V)) : rsec p M V (usec p M V x) = x

theorem

usec_rsec

L107 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.usec_rsec

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem usec_rsec (x : Γ(M.restrict p, V)) : usec p M V (rsec p M V x) = x

theorem

rsec_injective

L108 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec_injective

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem rsec_injective : Function.Injective (rsec p M V)

theorem

rsec_add

L109 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec_add

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem rsec_add (x y : Γ(M.restrict p, V)) : rsec p M V (x + y) = rsec p M V x + rsec p M V y

theorem

usec_add

L111 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.usec_add

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem usec_add (x y : Γ(M, p ''ᵁ V)) : usec p M V (x + y) = usec p M V x + usec p M V y

theorem

rsec_smul

L113 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec_smul

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem rsec_smul (ρ : A.presheaf.obj (op V)) (z : Γ(M.restrict p, V)) :
    rsec p M V (ρ • z) = ((p.appIso V).inv ρ) • rsec p M V z

theorem

usec_smul

L115 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.usec_smul

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem usec_smul (a : X.presheaf.obj (op (p ''ᵁ V))) (y : Γ(M, p ''ᵁ V)) :
    usec p M V (a • y) = ((p.appIso V).hom a) • usec p M V y

theorem

rsec_map

L120 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.rsec_map

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem rsec_map {V' : A.Opens} (i : op V ⟶ op V') (z : Γ(M.restrict p, V)) :
    rsec p M V' ((M.restrict p).presheaf.map i z) = M.presheaf.map (p.opensFunctor.map
      i.unop).op (rsec p M V z)

theorem

usec_map

L123 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.usec_map

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}
section RSec
variable {X A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] (M : X.Modules) (V : A.Opens)

Lean source · statement

theorem usec_map {V' : A.Opens} (i : op V ⟶ op V') (y : Γ(M, p ''ᵁ V)) :
    (M.restrict p).presheaf.map i (usec p M V y) = usec p M V' (M.presheaf.map
      (p.opensFunctor.map i.unop).op y)

theorem

locallyTrivial_of_iso

L129 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.locallyTrivial_of_iso

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Generic
variable {Y : Scheme.{u}}

Lean source · statement

theorem locallyTrivial_of_iso {M N : Y.Modules} (e : M ≅ N) (hM : Scheme.Modules.IsInvertible M) :
    ∀ y : Y, ∃ (V : Y.Opens), y ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj N ≅ SheafOfModules.unit
        V.toScheme.ringCatSheaf)

theorem

tilde_map_app_toOpen

L143 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.tilde_map_app_toOpen

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
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

fromTildeΓ_app_top_toOpen

L148 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.fromTildeΓ_app_top_toOpen

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section SpecGeneric
variable {R : CommRingCat.{u}}

Lean source · full declaration

theorem fromTildeΓ_app_top_toOpen (M : (Spec (.of R)).Modules)
    (m : (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) :
    (Scheme.Modules.fromTildeΓ M).app ⊤
      (show Γ(tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)), ⊤) from tilde.toOpen _ ⊤ m) =
      (show Γ(M, ⊤) from m) := by
  have h := Scheme.Modules.toOpen_fromTildeΓ_app M ⊤
  have h' := ConcreteCategory.congr_hom h m
  refine h'.trans ?_
  exact map_endo M _ _

theorem

image_top

L164 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.image_top

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

theorem image_top : hU.fromSpec ''ᵁ ⊤ = U

abbrev

ιd

L168 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ιd

Documentation

The opposite open map identifying the affine chart with its image from Spec.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

abbrev ιd : op U ⟶ op (hU.fromSpec ''ᵁ ⊤)

abbrev

ιu

L171 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ιu

Documentation

The inverse opposite open map for the affine chart identification.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

abbrev ιu : op (hU.fromSpec ''ᵁ ⊤) ⟶ op U

theorem

appIso_inv_ΓSpecIso_inv

L173 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.appIso_inv_ΓSpecIso_inv

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

theorem appIso_inv_ΓSpecIso_inv (r : X.presheaf.obj (op U)) :
    (hU.fromSpec.appIso ⊤).inv ((Scheme.ΓSpecIso (X.presheaf.obj (op U))).inv r) =
      X.presheaf.map (ιd U hU) r

abbrev

RL

L203 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.RL

Documentation

The module restricted to the affine Spec model of the chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

abbrev RL : (Spec (X.presheaf.obj (op U))).Modules

abbrev

ΓR

L206 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ΓR

Documentation

The global sections module of the restriction to the affine Spec chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

abbrev ΓR : ModuleCat (X.presheaf.obj (op U))

def

toΓ

L210 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ

Documentation

Global sections on the affine chart, viewed over its image open.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

def toΓ : ΓR U hU L → Γ(L, hU.fromSpec ''ᵁ ⊤)

def

ofΓ

L212 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ofΓ

Documentation

Sections over the image open, viewed as global sections of the affine chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

def ofΓ : Γ(L, hU.fromSpec ''ᵁ ⊤) → ΓR U hU L

theorem

toΓ_ofΓ

L214 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_ofΓ

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem toΓ_ofΓ (x : Γ(L, hU.fromSpec ''ᵁ ⊤)) : toΓ U hU L (ofΓ U hU L x) = x

theorem

ofΓ_toΓ

L215 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ofΓ_toΓ

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem ofΓ_toΓ (s : ΓR U hU L) : ofΓ U hU L (toΓ U hU L s) = s

theorem

toΓ_add

L216 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_add

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem toΓ_add (s t : ΓR U hU L) : toΓ U hU L (s + t) = toΓ U hU L s + toΓ U hU L t

theorem

ofΓ_add

L217 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ofΓ_add

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem ofΓ_add (s t : Γ(L, hU.fromSpec ''ᵁ ⊤)) : ofΓ U hU L (s + t) = ofΓ U hU L s + ofΓ U hU L
    t

theorem

toΓ_injective

L219 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_injective

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem toΓ_injective : Function.Injective (toΓ U hU L)

theorem

toΓ_eq

L221 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_eq

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · full declaration

theorem toΓ_eq (s : ΓR U hU L) : (show Γ(RL U hU L, ⊤) from s) = toΓ U hU L s := rfl

theorem

toΓ_smul

L223 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_smul

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem toΓ_smul (r : X.presheaf.obj (op U)) (s : ΓR U hU L) :
    toΓ U hU L (r • s) = (X.presheaf.map (ιd U hU) r) • toΓ U hU L s

def

τ

L237 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ

Documentation

The comparison from global sections on the Spec chart to sections on the original chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

def τ (s : ΓR U hU L) : Γ(L, U)

def

τ'

L240 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ'

Documentation

The inverse comparison from original chart sections to global sections on the Spec chart.

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

def τ' (m : Γ(L, U)) : ΓR U hU L

theorem

toΓ_τ'

L242 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.toΓ_τ'

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem toΓ_τ' (m : Γ(L, U)) : toΓ U hU L (τ' U hU L m) = L.presheaf.map (ιd U hU) m

theorem

τ_τ'

L244 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ_τ'

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ_τ' (m : Γ(L, U)) : τ U hU L (τ' U hU L m) = m

theorem

τ'_τ

L248 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ'_τ

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ'_τ (s : ΓR U hU L) : τ' U hU L (τ U hU L s) = s

theorem

τ_add

L252 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ_add

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ_add (s t : ΓR U hU L) : τ U hU L (s + t) = τ U hU L s + τ U hU L t

theorem

τ'_add

L256 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ'_add

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ'_add (m n : Γ(L, U)) : τ' U hU L (m + n) = τ' U hU L m + τ' U hU L n

theorem

τ_smul

L260 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ_smul

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ_smul (r : X.presheaf.obj (op U)) (s : ΓR U hU L) : τ U hU L (r • s) = r • τ U hU L s

theorem

τ'_smul

L264 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.τ'_smul

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Chart
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U)
variable (L : X.Modules)

Lean source · statement

theorem τ'_smul (r : X.presheaf.obj (op U)) (m : Γ(L, U)) : τ' U hU L (r • m) = r • τ' U hU L m

def

eL

L299 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.eL

Documentation

The section equivalence transported to the global sections modules on the affine chart.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · full declaration

def eL : ΓR U hU L ≃ₗ[X.presheaf.obj (op U)] ΓR U hU L' where
  toFun s := τ' U hU L' (e (τ U hU L s))
  invFun s' := τ' U hU L (e.symm (τ U hU L' s'))
  map_add' s t := by rw [τ_add, map_add, τ'_add]
  map_smul' r s := by rw [τ_smul, LinearEquiv.map_smul, τ'_smul]; rfl
  left_inv s := by simp only [τ_τ', LinearEquiv.symm_apply_apply, τ'_τ]
  right_inv s' := by simp only [τ_τ', LinearEquiv.apply_symm_apply, τ'_τ]

def

eR

L308 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.eR

Documentation

The corresponding isomorphism in the category of modules over the chart ring.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

def eR : ΓR U hU L ≅ ΓR U hU L'

theorem

eR_hom_apply

L310 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.eR_hom_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem eR_hom_apply (s : ΓR U hU L) : (eR U hU L L' e).hom s = τ' U hU L' (e (τ U hU L s))

theorem

isIso_fromTildeΓ

L312 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isIso_fromTildeΓ

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))
include hL in

Lean source · statement

theorem isIso_fromTildeΓ :
    IsIso (Scheme.Modules.fromTildeΓ (R := X.presheaf.obj (op U)) (RL U hU L))

def

ψiso

L320 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ψiso

Documentation

The chart module isomorphism induced by the given section equivalence.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

def ψiso : RL U hU L ≅ RL U hU L'

def

ψ

L330 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ψ

Documentation

The morphism underlying the induced chart module isomorphism.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

def ψ : RL U hU L ⟶ RL U hU L'

instance

isIso_ψ

L332 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isIso_ψ

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

instance isIso_ψ : IsIso (ψ U hU L L' hL hL' e)

theorem

ψ_eq

L334 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ψ_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · full declaration

theorem ψ_eq : ψ U hU L L' hL hL' e =
    (haveI := isIso_fromTildeΓ U hU L hL
     inv (Scheme.Modules.fromTildeΓ (R := X.presheaf.obj (op U)) (RL U hU L)) ≫
      (tilde.functor (X.presheaf.obj (op U))).map (eR U hU L L' e).hom ≫
      Scheme.Modules.fromTildeΓ (R := X.presheaf.obj (op U)) (RL U hU L')) := rfl

theorem

ψ_app_top_τ'

L340 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ψ_app_top_τ'

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section ChartHom
variable {X : Scheme.{u}} (U : X.Opens) (hU : IsAffineOpen U) (L L' : X.Modules)
  (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem ψ_app_top_τ' (m : Γ(L, U)) :
    (ψ U hU L L' hL hL' e).app ⊤ (usec hU.fromSpec L ⊤ (L.presheaf.map (ιd U hU) m)) =
      usec hU.fromSpec L' ⊤ (L'.presheaf.map (ιd U hU) (e m))

theorem

image_comp_eq

L399 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.image_comp_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

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

theorem

map_congr_hom

L408 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.map_congr_hom

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

theorem map_congr_hom {Y : Scheme.{u}} (M : Y.Modules) {U V : Y.Opens} (i j : op U ⟶ op V) (x y
    : Γ(M, U))
    (h : x = y) : M.presheaf.map i x = M.presheaf.map j y

theorem

image_eq_of_eq

L412 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.image_eq_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

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

theorem

opensRange_eq_of_eq

L416 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.opensRange_eq_of_eq

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

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

theorem

restrict_app_apply

L420 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.restrict_app_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

theorem restrict_app_apply {A : Scheme.{u}} (p : A ⟶ X) [IsOpenImmersion p] {M N : X.Modules} (φ
    : M ⟶ N)
    (V : A.Opens) (x : Γ(M.restrict p, V)) :
    ((Scheme.Modules.restrictFunctor p).map φ).app V x = φ.app (p ''ᵁ V) x

theorem

bijective_app_of_iso

L425 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.bijective_app_of_iso

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · statement

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

theorem

isIso_fromTildeΓ_restrict

L432 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isIso_fromTildeΓ_restrict

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section MoreGeneric
variable {X : Scheme.{u}}

Lean source · full declaration

theorem isIso_fromTildeΓ_restrict {A : CommRingCat.{u}} (f : Spec A ⟶ X) [IsOpenImmersion f] (L
    : X.Modules)
    (hL : Scheme.Modules.IsInvertible L) :
    IsIso (Scheme.Modules.fromTildeΓ (R := A) (show (Spec (.of A)).Modules from L.restrict f)) := by
  refine Scheme.Modules.isIso_fromTildeGamma_of_locallyTrivial _ ?_
  have h := locallyTrivial_of_iso ((Scheme.Modules.restrictFunctorIsoPullback f).app L).symm
    (hL.pullback f)
  exact h

abbrev

ρ0

L447 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ρ0

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)

Lean source · statement

abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ρ0 : X.presheaf.obj
    (op U0) ⟶ X.presheaf.obj (op (U0 ⊓ U1))

abbrev

ρ1

L450 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ρ1

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso

Lean source · statement

abbrev _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ρ1 : X.presheaf.obj
    (op U1) ⟶ X.presheaf.obj (op (U0 ⊓ U1))

abbrev

g0

L454 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.g0

Documentation

The Spec morphism from the chart intersection to the first chart.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso

Lean source · statement

abbrev g0 : Spec (X.presheaf.obj (op (U0 ⊓ U1))) ⟶ Spec (X.presheaf.obj (op U0))

abbrev

g1

L457 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.g1

Documentation

The Spec morphism from the chart intersection to the second chart.

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso

Lean source · statement

abbrev g1 : Spec (X.presheaf.obj (op (U0 ⊓ U1))) ⟶ Spec (X.presheaf.obj (op U1))

theorem

g0_f0

L462 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.g0_f0

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
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

L464 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.g1_f1

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
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

hg

L467 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.hg

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
variable (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
include hU01 in

Lean source · statement

theorem hg : g0 U0 U1 ≫ hU0.fromSpec = g1 U0 U1 ≫ hU1.fromSpec

theorem

isOpenImmersion_g0

L470 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isOpenImmersion_g0

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
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

L474 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isOpenImmersion_g1

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Charts
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso
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)

abbrev

cW

L489 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.cW

Documentation

The opposite open map identifying the given open with its Spec image.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

abbrev cW : op W ⟶ op (hU.fromSpec ''ᵁ (g ''ᵁ ⊤))

abbrev

cW'

L491 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.cW'

Documentation

The inverse opposite open map for the Spec image identification.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

abbrev cW' : op (hU.fromSpec ''ᵁ (g ''ᵁ ⊤)) ⟶ op W

def

Θ

L494 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ

Documentation

The chart comparison on sections transported to the specified smaller open.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

def Θ (x : Γ(L, W)) : Γ(L', W)

theorem

Θ_add

L499 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ_add

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem Θ_add (x y : Γ(L, W)) :
    Θ U W hU g hgW L L' hL hL' e (x + y) = Θ U W hU g hgW L L' hL hL' e x + Θ U W hU g hgW L L'
      hL hL' e y

theorem

Θ_smul

L504 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ_smul

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem Θ_smul (a : X.presheaf.obj (op W)) (x : Γ(L, W)) :
    Θ U W hU g hgW L L' hL hL' e (a • x) = a • Θ U W hU g hgW L L' hL hL' e x

def

Θₗ

L512 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θₗ

Documentation

The linear map on the smaller open induced by the chart comparison.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · full declaration

def Θₗ : Γ(L, W) →ₗ[X.presheaf.obj (op W)] Γ(L', W) where
  toFun := Θ U W hU g hgW L L' hL hL' e
  map_add' := Θ_add U W hU g hgW L L' hL hL' e
  map_smul' := Θ_smul U W hU g hgW L L' hL hL' e

theorem

Θₗ_apply

L517 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θₗ_apply

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem Θₗ_apply (x : Γ(L, W)) : Θₗ U W hU g hgW L L' hL hL' e x = Θ U W hU g hgW L L' hL hL' e
    x

theorem

Θ_res

L520 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ_res

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem Θ_res (m : Γ(L, U)) :
    Θ U W hU g hgW L L' hL hL' e (L.presheaf.map (homOfLE hWU).op m) = L'.presheaf.map (homOfLE
      hWU).op (e m)

theorem

ψ_app_normal

L532 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.ψ_app_normal

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section OneChart
variable {X : Scheme.{u}} (U W : X.Opens) (hU : IsAffineOpen U) (hWU : W ≤ U)
  {B : Scheme.{u}} (g : B ⟶ Spec (X.presheaf.obj (op U))) [IsOpenImmersion g]
  (hgW : hU.fromSpec ''ᵁ (g ''ᵁ ⊤) = W)
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e : Γ(L, U) ≃ₗ[X.presheaf.obj (op U)] Γ(L', U))

Lean source · statement

theorem ψ_app_normal (t : Γ(L, hU.fromSpec ''ᵁ (g ''ᵁ ⊤)))
    (k : op (hU.fromSpec ''ᵁ (g ''ᵁ ⊤)) ⟶ op W) (k' : op W ⟶ op (hU.fromSpec ''ᵁ (g ''ᵁ ⊤))) :
    rsec hU.fromSpec L' (g ''ᵁ ⊤) ((ψ U hU L L' hL hL' e).app (g ''ᵁ ⊤) (usec hU.fromSpec L (g
      ''ᵁ ⊤) t)) =
      L'.presheaf.map k' (Θ U W hU g hgW L L' hL hL' e (L.presheaf.map k t))

theorem

f0_g0_top

L562 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.f0_g0_top

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
omit [IsOpenImmersion (g1 U0 U1)] in
include hU01 in

Lean source · statement

theorem f0_g0_top : hU0.fromSpec ''ᵁ ((g0 U0 U1) ''ᵁ ⊤) = U0 ⊓ U1

theorem

f1_g1_top

L568 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.f1_g1_top

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
omit [IsOpenImmersion (g0 U0 U1)] in
include hU01 in

Lean source · statement

theorem f1_g1_top : hU1.fromSpec ''ᵁ ((g1 U0 U1) ''ᵁ ⊤) = U0 ⊓ U1

abbrev

Θ0

L574 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ0

Documentation

The comparison induced on the chart intersection from the first chart.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

abbrev Θ0

abbrev

Θ1

L576 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ1

Documentation

The comparison induced on the chart intersection from the second chart.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

abbrev Θ1

theorem

Θ0_eq

L579 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ0_eq

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
include he0 span0 in
omit [IsOpenImmersion (g1 U0 U1)] in

Lean source · statement

theorem Θ0_eq : Θ0 U0 U1 hU0 hU01 L L' hL hL' e0 = e01.toLinearMap

theorem

Θ1_eq

L585 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.Θ1_eq

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
include he1 span1 in
omit [IsOpenImmersion (g0 U0 U1)] in

Lean source · statement

theorem Θ1_eq : Θ1 U0 U1 hU1 hU01 L L' hL hL' e1 = e01.toLinearMap

def

T0

L591 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.T0

Documentation

The first chart comparison restricted to the common Spec model of the intersection.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

def T0 : L.restrict (g0 U0 U1 ≫ hU0.fromSpec) ⟶ L'.restrict (g0 U0 U1 ≫ hU0.fromSpec)

def

T1

L597 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.T1

Documentation

The second chart comparison transported to the same common Spec model of the intersection.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

def T1 : L.restrict (g0 U0 U1 ≫ hU0.fromSpec) ⟶ L'.restrict (g0 U0 U1 ≫ hU0.fromSpec)

theorem

P_top

L605 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.P_top

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
include hU01 in
omit [IsOpenImmersion (g1 U0 U1)] in

Lean source · statement

theorem P_top : (g0 U0 U1 ≫ hU0.fromSpec) ''ᵁ ⊤ = U0 ⊓ U1

abbrev

dd

L610 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.dd

Documentation

The opposite open map from the common Spec image to the chart intersection.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

abbrev dd : op ((g0 U0 U1 ≫ hU0.fromSpec) ''ᵁ ⊤) ⟶ op (U0 ⊓ U1)

abbrev

dd'

L613 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.dd'

Documentation

The inverse opposite open map for the common Spec image identification.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

abbrev dd' : op (U0 ⊓ U1) ⟶ op ((g0 U0 U1 ≫ hU0.fromSpec) ''ᵁ ⊤)

theorem

T0_app_top

L616 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.T0_app_top

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
omit [IsOpenImmersion (g1 U0 U1)] in

Lean source · statement

theorem T0_app_top (t : Γ(L.restrict (g0 U0 U1 ≫ hU0.fromSpec), ⊤)) :
    rsec (g0 U0 U1 ≫ hU0.fromSpec) L' ⊤ ((T0 U0 U1 hU0 L L' hL hL' e0).app ⊤ t) =
      L'.presheaf.map (dd' U0 U1 hU0 hU01)
        (Θ0 U0 U1 hU0 hU01 L L' hL hL' e0 (L.presheaf.map (dd U0 U1 hU0 hU01)
          (rsec (g0 U0 U1 ≫ hU0.fromSpec) L ⊤ t)))

theorem

T1_app_top

L636 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.T1_app_top

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)

Lean source · statement

theorem T1_app_top (t : Γ(L.restrict (g0 U0 U1 ≫ hU0.fromSpec), ⊤)) :
    rsec (g0 U0 U1 ≫ hU0.fromSpec) L' ⊤ ((T1 U0 U1 hU0 hU1 hU01 L L' hL hL' e1).app ⊤ t) =
      L'.presheaf.map (dd' U0 U1 hU0 hU01)
        (Θ1 U0 U1 hU1 hU01 L L' hL hL' e1 (L.presheaf.map (dd U0 U1 hU0 hU01)
          (rsec (g0 U0 U1 ≫ hU0.fromSpec) L ⊤ t)))

theorem

T0_eq_T1

L660 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.T0_eq_T1

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Agreement
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
include he0 he1 span0 span1 in

Lean source · statement

theorem T0_eq_T1 : T0 U0 U1 hU0 L L' hL hL' e0 = T1 U0 U1 hU0 hU1 hU01 L L' hL hL' e1

theorem

hcov

L722 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.hcov

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Main
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
  (hsup : U0 ⊔ U1 = ⊤)
omit [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)] in
include hsup in

Lean source · statement

theorem hcov : hU0.fromSpec.opensRange ⊔ hU1.fromSpec.opensRange = ⊤

theorem

hov

L726 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.hov

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Main
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
  (hsup : U0 ⊔ U1 = ⊤)
omit [IsOpenImmersion (g1 U0 U1)] in
include hU01 in

Lean source · statement

theorem hov : hU0.fromSpec.opensRange ⊓ hU1.fromSpec.opensRange ≤ (g0 U0 U1 ≫
    hU0.fromSpec).opensRange

theorem

exists_φ

L731 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.exists_φ

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Main
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
  (hsup : U0 ⊔ U1 = ⊤)
include hU01 he0 he1 span0 span1 hsup in

Lean source · statement

theorem exists_φ : ∃ φ : L ⟶ L', (Scheme.Modules.restrictFunctor hU0.fromSpec).map φ = ψ U0 hU0
    L L' hL hL' e0 ∧
    (Scheme.Modules.restrictFunctor hU1.fromSpec).map φ = ψ U1 hU1 L L' hL hL' e1

theorem

isIso_of_restrict

L741 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.isIso_of_restrict

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Main
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
  (hsup : U0 ⊔ U1 = ⊤)
omit [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)] in
include hsup in

Lean source · statement

theorem isIso_of_restrict (φ : L ⟶ L') (h0 : (Scheme.Modules.restrictFunctor hU0.fromSpec).map φ
    = ψ U0 hU0 L L' hL hL' e0)
    (h1 : (Scheme.Modules.restrictFunctor hU1.fromSpec).map φ = ψ U1 hU1 L L' hL hL' e1) : IsIso
      φ

theorem

nonempty_iso

L766 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.nonempty_iso

Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
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
section Main
variable {X : Scheme.{u}} (U0 U1 : X.Opens)
  (hU0 : IsAffineOpen U0) (hU1 : IsAffineOpen U1) (hU01 : IsAffineOpen (U0 ⊓ U1))
  [IsOpenImmersion (g0 U0 U1)] [IsOpenImmersion (g1 U0 U1)]
  (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
  (e0 : Γ(L, U0) ≃ₗ[X.presheaf.obj (op U0)] Γ(L', U0))
  (e1 : Γ(L, U1) ≃ₗ[X.presheaf.obj (op U1)] Γ(L', U1))
  (e01 : Γ(L, U0 ⊓ U1) ≃ₗ[X.presheaf.obj (op (U0 ⊓ U1))] Γ(L', U0 ⊓ U1))
  (he0 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) =
    L'.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op (e0 m))
  (he1 : ∀ m, e01 (L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) =
    L'.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op (e1 m))
  (span0 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U0) => L.presheaf.map (homOfLE (inf_le_left : U0 ⊓ U1 ≤ U0)).op m) = ⊤)
  (span1 : Submodule.span (X.presheaf.obj (op (U0 ⊓ U1)))
    (Set.range fun m : Γ(L, U1) => L.presheaf.map (homOfLE (inf_le_right : U0 ⊓ U1 ≤ U1)).op m) = ⊤)
  (hsup : U0 ⊔ U1 = ⊤)
include hU0 hU1 hU01 hL hL' e0 e1 e01 he0 he1 span0 span1 hsup in

Lean source · statement

theorem nonempty_iso : Nonempty (L ≅ L')

theorem

span_eq_top_of_baseChange

L787 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible.AlgebraicGeometry.Scheme.TwoAffineOpenCover.GlueIso.span_eq_top_of_baseChange

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace GlueIso
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open TensorProduct in

Lean source · statement

theorem span_eq_top_of_baseChange {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] {M : Type*}
    [AddCommGroup M] [Module A M] {N : Type*} [AddCommGroup N] [Module B N]
    (r : M → N) (rbc : B ⊗[A] M ≃ₗ[B] N) (h : ∀ m, rbc (1 ⊗ₜ m) = r m) :
    Submodule.span B (Set.range r) = ⊤

theorem

nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible

L811 ↗

AlgebraicGeometry.Scheme.TwoAffineOpenCover.nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits _root_.AlgebraicGeometry
    AlgebraicGeometry TensorProduct Opposite in
with_weak_namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open GlueIso in
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_TwoAffineOpenCover_nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover

Lean source · statement

theorem nonempty_iso_of_sectionsOf_linearEquiv_of_isInvertible
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (L L' : X.Modules) (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
    (e0 : (𝒱.sectionsOf c L).M0 ≃ₗ[(𝒱.cover c).A0] (𝒱.sectionsOf c L').M0)
    (e1 : (𝒱.sectionsOf c L).M1 ≃ₗ[(𝒱.cover c).A1] (𝒱.sectionsOf c L').M1)
    (e01 : (𝒱.sectionsOf c L).M01 ≃ₗ[(𝒱.cover c).A01] (𝒱.sectionsOf c L').M01)
    (he0 : ∀ m, e01 ((𝒱.sectionsOf c L).r0 m) = (𝒱.sectionsOf c L').r0 (e0 m))
    (he1 : ∀ m, e01 ((𝒱.sectionsOf c L).r1 m) = (𝒱.sectionsOf c L').r1 (e1 m)) :
    Nonempty (L ≅ L')

Module documentation

Declarations