Module

Scheme_Modules_exists_app_eq_of_exact_of_app_eq_zero.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_app_eq_of_exact_of_app_eq_zero

5 declarations indexed from sourceView source ↗

Module documentation

Lifting kernel sections in an exact complex

When the first map is a monomorphism, a section killed by the second map comes from a section under the first map.

Imports4

Mathlib.Topology.Sheaves.AddCommGrpCat
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Ext
Mathlib.Tactic.TermCongr

Imported by8

instance

(anonymous instance)

L50 ↗

Source context 19 commands

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

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

Lean source · full declaration

instance : (toPresheaf X).Additive where
  map_add := by intros; rfl

abbrev

evalAt

L54 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_app_eq_of_exact_of_app_eq_zero.AlgebraicGeometry.Scheme.Modules.evalAt

Documentation

Evaluate a presheaf of abelian groups on the open subset U.

Source context 19 commands

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

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

Lean source · statement

abbrev evalAt (U : X.Opens) : TopCat.Presheaf Ab.{u} X ⥤ Ab.{u}

instance

(anonymous instance)

L57 ↗

Source context 19 commands

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

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

Lean source · full declaration

instance (U : X.Opens) : (evalAt (X := X) U).Additive where
  map_add := by intros; rfl

theorem

exists_app_eq_of_exact_of_app_eq_zero

L60 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_app_eq_of_exact_of_app_eq_zero.AlgebraicGeometry.Scheme.Modules.exists_app_eq_of_exact_of_app_eq_zero

Source context 19 commands

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

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

Lean source · statement

theorem exists_app_eq_of_exact_of_app_eq_zero (S : ShortComplex X.Modules) (hS : S.Exact) [Mono S.f]
    (U : X.Opens) (m : Γ(S.X₂, U)) (hm : S.g.app U m = 0) :
    ∃ e : Γ(S.X₁, U), S.f.app U e = m

theorem

exists_app_eq_of_exact_of_app_eq_zero

L87 ↗

AlgebraicGeometry.Scheme.Modules.exists_app_eq_of_exact_of_app_eq_zero

Source context 10 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_app_eq_of_exact_of_app_eq_zero {X :
  Scheme.{u}} (S : ShortComplex X.Modules) (hS : S.Exact) [Mono S.f]
    (U : X.Opens) (m : Γ(S.X₂, U)) (hm : S.g.app U m = 0) :
    ∃ e : Γ(S.X₁, U), S.f.app U e = m

Module documentation

Lifting kernel sections in an exact complex

Declarations

(anonymous instance)

evalAt

(anonymous instance)

exists_app_eq_of_exact_of_app_eq_zero

exists_app_eq_of_exact_of_app_eq_zero