Module

bijective_app_of_forall_isAffineOpen.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_app_of_forall_isAffineOpen

2 declarations indexed from sourceView source ↗

Module documentation

bijective app of forall is Affine Open

Imports7

Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Category.Ring.Colimits
Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.Algebra.Category.Ring.Limits
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Stalks

Imported by2

theorem

stalkFunctor_map_surjective_of_isBasis

L39 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_forall_isAffineOpen.SheafGlueGC3.stalkFunctor_map_surjective_of_isBasis

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.bijective_app_of_forall_isAffineOpen
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
open TopologicalSpace Opposite
namespace SheafGlueGC3
open TopCat TopCat.Presheaf

Lean source · statement

theorem stalkFunctor_map_surjective_of_isBasis {X : TopCat.{u}} {B : Set (Opens X)} (hB :
  Opens.IsBasis B)
    {F G : X.Presheaf CommRingCat.{u}} {α : F ⟶ G} (hα : ∀ U ∈ B, Function.Surjective (α.app (op
      U))) (x : X) :
    Function.Surjective ((stalkFunctor _ x).map α)

theorem

bijective_app_of_forall_isAffineOpen

L51 ↗

AlgebraicGeometry.bijective_app_of_forall_isAffineOpen

Source context 5 commands