Module

Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen

9 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules forall exists basis map eq of forall is Affine Open

Imports6

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.LinearAlgebra.Basis.Basic
Mathlib.LinearAlgebra.LinearIndependent.Defs
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Tactic.Choose
Nyll.SchemeTheory.Modules.Monoidal

Imported by3

theorem

res_res

L60 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.res_res

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem res_res {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (x : Γ(M, U)) :
    M.presheaf.map (homOfLE h₂).op (M.presheaf.map (homOfLE h₁).op x) =
      M.presheaf.map (homOfLE (h₂.trans h₁)).op x

theorem

res_res'

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.res_res'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem res_res' {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (x : Γ(X, U)) :
    X.presheaf.map (homOfLE h₂).op (X.presheaf.map (homOfLE h₁).op x) =
      X.presheaf.map (homOfLE (h₂.trans h₁)).op x

theorem

res_sum_smul

L72 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.res_sum_smul

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem res_sum_smul {U W : X.Opens} (h : W ≤ U) {d : ℕ} (c : Fin d → Γ(X, U)) (v : Fin d → Γ(M,
  U)) :
    M.presheaf.map (homOfLE h).op (∑ i, c i • v i) =
      ∑ i, X.presheaf.map (homOfLE h).op (c i) • M.presheaf.map (homOfLE h).op (v i)

abbrev

ι

L84 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.ι

Documentation

The type of affine open subsets contained in the given open subset.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))

Lean source · statement

abbrev ι (W : X.Opens) : Type u

theorem

cover

L86 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.cover

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))

Lean source · statement

theorem cover (W : X.Opens) : W ≤ ⨆ i : ι W, i.1

theorem

linearIndependent

L92 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.linearIndependent

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in

Lean source · statement

theorem linearIndependent (W : X.Opens) (hW : W ≤ V) :
    ∀ c : Fin d → Γ(X, W), ∑ i, c i • M.presheaf.map (homOfLE hW).op (e i) = 0 → c = 0

theorem

exists_coords

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.exists_coords

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in

Lean source · statement

theorem exists_coords (W : X.Opens) (hW : W ≤ V) (s : Γ(M, W)) :
    ∃ c : Fin d → Γ(X, W), ∑ i, c i • M.presheaf.map (homOfLE hW).op (e i) = s

theorem

main

L152 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen.AlgebraicGeometry.Scheme.Modules.RGlue.main

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace RGlue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}} (M : X.Modules)
variable {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
  (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in

Lean source · statement

theorem main (W : X.Opens) (hW : W ≤ V) :
    ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)

theorem

forall_exists_basis_map_eq_of_forall_isAffineOpen

L167 ↗

AlgebraicGeometry.Scheme.Modules.forall_exists_basis_map_eq_of_forall_isAffineOpen

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_forall_exists_basis_map_eq_of_forall_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.forall_exists_basis_map_eq_of_forall_isAffineOpen
    {X : Scheme.{u}} (M : X.Modules) {V : X.Opens} {d : ℕ} (e : Fin d → Γ(M, V))
    (he : ∀ (W : X.Opens) (hW : W ≤ V), IsAffineOpen W →
      ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)) :
    ∀ (W : X.Opens) (hW : W ≤ V),
      ∃ b : Module.Basis (Fin d) Γ(X, W) Γ(M, W), ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)

Module documentation

Scheme Modules forall exists basis map eq of forall is Affine Open

Declarations