Module

PullbackFiniteSkyscraperEmbedding.lean

Nyll.SchemeTheory.Topology.PullbackFiniteSkyscraperEmbedding

2 declarations indexed from sourceView source ↗

Module documentation

Pullback of the finite stalk-skyscraper embedding

Mapping the components of the actual stalk-skyscraper embedding gives a morphism from the inverse image of a sheaf to the product of the inverse images of its stalk skyscrapers. For a finite target space, this is a monomorphism: inverse image preserves monomorphisms and the finite product, whose comparison is Mathlib's PreservesProduct.iso.

The Lean proofs are original.

Imports9

Nyll.SchemeTheory.Topology.FiniteSkyscraperEmbedding
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Constructions.EpiMono
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
Mathlib.CategoryTheory.Limits.Types.Products
Mathlib.CategoryTheory.Sites.Pullback
Mathlib.Topology.Sheaves.Functors
Mathlib.Topology.Sheaves.Limits
Mathlib.Topology.Sheaves.SheafCondition.Sites

Imported by2

def

pullbackToStalkSkyscrapers

L40 ↗

SchemeTheory.pullbackToStalkSkyscrapers

Documentation

The product of the inverse images of the actual skyscraper-unit maps.

Source context 5 commands

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

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

Lean source · full declaration

def pullbackToStalkSkyscrapers (q : X ⟶ Y)
    (G : CategoryTheory.Sheaf (Opens.grothendieckTopology Y) (Type u)) :
    (TopCat.Sheaf.pullback (Type u) q).obj G ⟶
      ∏ᶜ (fun y : Y => (TopCat.Sheaf.pullback (Type u) q).obj (stalkSkyscraper G y)) := by
  let JX : GrothendieckTopology (Opens X) := Opens.grothendieckTopology X
  let JY : GrothendieckTopology (Opens Y) := Opens.grothendieckTopology Y
  let L : CategoryTheory.Sheaf JY (Type u) ⥤ CategoryTheory.Sheaf JX (Type u) :=
    (Opens.map q).sheafPullback (Type u) JY JX
  let S : Y → CategoryTheory.Sheaf JY (Type u) := stalkSkyscraper G
  let m : G ⟶ ∏ᶜ S := toStalkSkyscrapers G
  exact Pi.lift (fun y : Y => L.map (m ≫ Pi.π S y))

theorem

mono_pullbackToStalkSkyscrapers

L54 ↗

SchemeTheory.mono_pullbackToStalkSkyscrapers