Module

FiniteProductRestriction.lean

Nyll.SchemeTheory.Topology.FiniteProductRestriction

1 declaration indexed from sourceView source ↗

Module documentation

Surjective global restriction and finite products

Global restriction through the actual inverse-image adjunction is surjective for a finite product whenever it is surjective for each factor. The proof uses actual sheaf product projections, preservation of finite products by inverse image, and preservation of products by sheaf sections. Lifts of the projected target section assemble by the product universal property; unit naturality identifies their restriction with the target.

The Lean proof is original.

Imports9

Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
Mathlib.CategoryTheory.Limits.Types.Products
Mathlib.CategoryTheory.Sites.Limits
Mathlib.CategoryTheory.Sites.Pullback
Mathlib.CategoryTheory.Types.Basic
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Limits
Mathlib.Topology.Sheaves.SheafCondition.Sites

Imported by2

theorem

sheafPullback_globalSections_surjective_pi

L42 ↗

SchemeTheory.sheafPullback_globalSections_surjective_pi

Documentation

Surjectivity of the actual global restriction map is stable under finite products of sheaves of types.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace Opposite
namespace SchemeTheory
variable {X Y : TopCat.{u}}

Lean source · statement

theorem sheafPullback_globalSections_surjective_pi (f : X ⟶ Y)
    {I : Type u} [Finite I]
    (G : I → CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u))
    (hG : ∀ i : I, Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app (G i)).hom.app
        (op (⊤ : Opens Y)))) :
    Function.Surjective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u) f).unit.app (∏ᶜ G)).hom.app
        (op (⊤ : Opens Y)))

Module documentation

Surjective global restriction and finite products

Declarations

sheafPullback_globalSections_surjective_pi