Mathlib.Geometry.RingedSpace.PresheafedSpace

AlgebraicGeometry.PresheafedSpace structure

Full source

/-- A `PresheafedSpace C` is a topological space equipped with a presheaf of `C`s. -/
structure PresheafedSpace where
  carrier : TopCat
  protected presheaf : carrier.Presheaf C

Presheafed space

Informal description

A presheafed space over a category $ C $ consists of a topological space $ X $ equipped with a presheaf of objects from $ C $ on $ X $. This means for every open subset $ U \subseteq X $, we have an object $ F(U) $ in $ C $, and for every inclusion $ V \subseteq U $ of open subsets, a restriction morphism $ F(U) \to F(V) $ in $ C $, satisfying the usual functoriality conditions.

AlgebraicGeometry.PresheafedSpace.coeCarrier instance

: CoeOut (PresheafedSpace C) TopCat

Full source

instance coeCarrier : CoeOut (PresheafedSpace C) TopCat where coe X := X.carrier

Presheafed Spaces as Topological Spaces

Informal description

For any presheafed space $X$ over a category $C$, there is a canonical way to view $X$ as an object in the category of topological spaces, where the underlying topological space is the base space of $X$.

AlgebraicGeometry.PresheafedSpace.instCoeSortType instance

: CoeSort (PresheafedSpace C) Type*

Full source

instance : CoeSort (PresheafedSpace C) Type* where coe X := X.carrier

Presheafed Spaces as Types

Informal description

For any presheafed space $X$ over a category $C$, there is a canonical way to view $X$ as a type, allowing us to treat $X$ as a set of points in the underlying topological space.

AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier instance

(X : PresheafedSpace C) : TopologicalSpace X

Full source

instance (X : PresheafedSpace C) : TopologicalSpace X :=
  X.carrier.str

Topological Space Structure on Presheafed Spaces

Informal description

For any presheafed space $X$ over a category $C$, the underlying type of $X$ carries a topological space structure.

AlgebraicGeometry.PresheafedSpace.const definition

(X : TopCat) (Z : C) : PresheafedSpace C

Full source

/-- The constant presheaf on `X` with value `Z`. -/
def const (X : TopCat) (Z : C) : PresheafedSpace C where
  carrier := X
  presheaf := (Functor.const _).obj Z

Constant presheaf on a topological space

Informal description

Given a topological space $ X $ and an object $ Z $ in a category $ C $, the constant presheaf on $ X $ with value $ Z $ is the presheafed space where: - The underlying topological space is $ X $. - The presheaf assigns the object $ Z $ to every open subset of $ X $, and the identity morphism on $ Z $ to every inclusion of open subsets.

AlgebraicGeometry.PresheafedSpace.instInhabited instance

[Inhabited C] : Inhabited (PresheafedSpace C)

Full source

instance [Inhabited C] : Inhabited (PresheafedSpace C) :=
  ⟨const (TopCat.of PEmpty) default⟩

Inhabited Presheafed Spaces over Inhabited Categories

Informal description

For any inhabited category $C$, the category of presheafed spaces over $C$ is also inhabited.

AlgebraicGeometry.PresheafedSpace.Hom structure

(X Y : PresheafedSpace C)

Full source

/-- A morphism between presheafed spaces `X` and `Y` consists of a continuous map
    `f` between the underlying topological spaces, and a (notice contravariant!) map
    from the presheaf on `Y` to the pushforward of the presheaf on `X` via `f`. -/
structure Hom (X Y : PresheafedSpace C) where
  base : (X : TopCat) ⟶ (Y : TopCat)
  c : Y.presheaf ⟶ base _* X.presheaf

Morphism of presheafed spaces

Informal description

A morphism between presheafed spaces $ X $ and $ Y $ consists of a continuous map $ f $ between the underlying topological spaces, and a contravariant morphism from the presheaf on $ Y $ to the pushforward of the presheaf on $ X $ via $ f $.

AlgebraicGeometry.PresheafedSpace.Hom.ext theorem

 {X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base)
  (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β

Full source

@[ext (iff := false)]
theorem Hom.ext {X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base)
    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β := by
  rcases α with ⟨base, c⟩
  rcases β with ⟨base', c'⟩
  dsimp at w
  subst w
  dsimp at h
  erw [whiskerRight_id', comp_id] at h
  subst h
  rfl

Extensionality of Morphisms of Presheafed Spaces

Informal description

Let $X$ and $Y$ be presheafed spaces over a category $C$, and let $\alpha, \beta \colon X \to Y$ be morphisms of presheafed spaces. If the underlying continuous maps $\alpha_{\text{base}}$ and $\beta_{\text{base}}$ are equal (i.e., $\alpha_{\text{base}} = \beta_{\text{base}}$), and the natural transformations $\alpha_c$ and $\beta_c$ satisfy the condition that $\alpha_c$ composed with the whiskering of the identity natural transformation (induced by the equality of the base maps) equals $\beta_c$, then $\alpha = \beta$.

AlgebraicGeometry.PresheafedSpace.hext theorem

{X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base) (h : HEq α.c β.c) : α = β

Full source

theorem hext {X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base) (h : HEq α.c β.c) :
    α = β := by
  cases α
  cases β
  congr

Hereditary Equality of Morphisms in Presheafed Spaces

Informal description

Let $ X $ and $ Y $ be presheafed spaces over a category $ C $, and let $ \alpha, \beta \colon X \to Y $ be morphisms of presheafed spaces. If the underlying continuous maps $ \alpha_{\text{base}} $ and $ \beta_{\text{base}} $ are equal (i.e., $ \alpha_{\text{base}} = \beta_{\text{base}} $), and the natural transformations $ \alpha_c $ and $ \beta_c $ are hereditarily equal (i.e., $ \alpha_c \approx \beta_c $), then $ \alpha = \beta $.

AlgebraicGeometry.PresheafedSpace.id definition

(X : PresheafedSpace C) : Hom X X

Full source

/-- The identity morphism of a `PresheafedSpace`. -/
def id (X : PresheafedSpace C) : Hom X X where
  base := 𝟙 (X : TopCat)
  c := 𝟙 _

Identity morphism of a presheafed space

Informal description

The identity morphism of a presheafed space $ X $ consists of the identity continuous map on the underlying topological space of $ X $ and the identity natural transformation on the presheaf of $ X $.

AlgebraicGeometry.PresheafedSpace.homInhabited instance

(X : PresheafedSpace C) : Inhabited (Hom X X)

Full source

instance homInhabited (X : PresheafedSpace C) : Inhabited (Hom X X) :=
  ⟨id X⟩

Existence of Identity Morphism for Presheafed Spaces

Informal description

For any presheafed space $X$ over a category $C$, the set of morphisms from $X$ to itself is nonempty, as it contains the identity morphism.

AlgebraicGeometry.PresheafedSpace.comp definition

{X Y Z : PresheafedSpace C} (α : Hom X Y) (β : Hom Y Z) : Hom X Z

Full source

/-- Composition of morphisms of `PresheafedSpace`s. -/
def comp {X Y Z : PresheafedSpace C} (α : Hom X Y) (β : Hom Y Z) : Hom X Z where
  base := α.base ≫ β.base
  c := β.c ≫ (Presheaf.pushforward _ β.base).map α.c

Composition of morphisms of presheafed spaces

Informal description

Given presheafed spaces $ X $, $ Y $, and $ Z $ over a category $ C $, and morphisms $ \alpha \colon X \to Y $ and $ \beta \colon Y \to Z $, the composition $ \beta \circ \alpha \colon X \to Z $ is defined as follows: - The underlying continuous map is the composition $ \alpha_{\text{base}} \circ \beta_{\text{base}} $ of the continuous maps from $ \alpha $ and $ \beta $. - The sheaf morphism is the composition $ \beta_c \circ (f_* \alpha_c) $, where $ f_* \alpha_c $ is the pushforward of $ \alpha_c $ along $ \beta_{\text{base}} $.

AlgebraicGeometry.PresheafedSpace.comp_c theorem

 {X Y Z : PresheafedSpace C} (α : Hom X Y) (β : Hom Y Z) : (comp α β).c = β.c ≫ (Presheaf.pushforward _ β.base).map α.c

Full source

theorem comp_c {X Y Z : PresheafedSpace C} (α : Hom X Y) (β : Hom Y Z) :
    (comp α β).c = β.c ≫ (Presheaf.pushforward _ β.base).map α.c :=
  rfl

Sheaf Component of Composition of Presheafed Space Morphisms

Informal description

For any presheafed spaces $X$, $Y$, and $Z$ over a category $C$, and morphisms $\alpha \colon X \to Y$ and $\beta \colon Y \to Z$, the sheaf component of the composition $\beta \circ \alpha$ is equal to the composition of $\beta_c$ with the pushforward of $\alpha_c$ along the continuous map $\beta_{\text{base}}$. That is, $(\beta \circ \alpha)_c = \beta_c \circ (f_* \alpha_c)$, where $f = \beta_{\text{base}}$.

AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces instance

: Category (PresheafedSpace C)

Full source

/-- The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map
    from the presheaf on the target to the pushforward of the presheaf on the source. -/
instance categoryOfPresheafedSpaces : Category (PresheafedSpace C) where
  Hom := Hom
  id := id
  comp := comp

The Category of Presheafed Spaces

Informal description

The category of presheafed spaces over a category $C$ has as objects pairs $(X, \mathcal{F})$ where $X$ is a topological space and $\mathcal{F}$ is a presheaf on $X$ with values in $C$. A morphism between $(X, \mathcal{F})$ and $(Y, \mathcal{G})$ consists of a continuous map $f \colon X \to Y$ and a natural transformation $\mathcal{G} \to f_* \mathcal{F}$.

AlgebraicGeometry.PresheafedSpace.Hom.toPshHom abbrev

{X Y : PresheafedSpace C} (f : Hom X Y) : X ⟶ Y

Full source

/-- Cast `Hom X Y` as an arrow `X ⟶ Y` of presheaves. -/
abbrev Hom.toPshHom {X Y : PresheafedSpace C} (f : Hom X Y) : X ⟶ Y := f

Casting Presheafed Space Morphisms as Presheaf Morphisms

Informal description

Given two presheafed spaces $X$ and $Y$ over a category $C$, and a morphism $f$ between them in the category of presheafed spaces, the function `toPshHom` casts $f$ as a morphism $X \longrightarrow Y$ in the category of presheaves.

AlgebraicGeometry.PresheafedSpace.ext theorem

 {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base) (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) :
  α = β

Full source

@[ext (iff := false)]
theorem ext {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
  Hom.ext α β w h

Extensionality of Morphisms of Presheafed Spaces

Informal description

Let $X$ and $Y$ be presheafed spaces over a category $C$, and let $\alpha, \beta \colon X \to Y$ be morphisms of presheafed spaces. If the underlying continuous maps $\alpha_{\text{base}}$ and $\beta_{\text{base}}$ are equal (i.e., $\alpha_{\text{base}} = \beta_{\text{base}}$), and the natural transformations $\alpha_c$ and $\beta_c$ satisfy the condition that $\alpha_c$ composed with the whiskering of the identity natural transformation (induced by the equality of the base maps) equals $\beta_c$, then $\alpha = \beta$.

AlgebraicGeometry.PresheafedSpace.id_base theorem

(X : PresheafedSpace C) : (𝟙 X : X ⟶ X).base = 𝟙 (X : TopCat)

Full source

@[simp]
theorem id_base (X : PresheafedSpace C) : (𝟙 X : X ⟶ X).base = 𝟙 (X : TopCat) :=
  rfl

Identity Morphism of Presheafed Space Preserves Base Space Identity

Informal description

For any presheafed space $X$ over a category $C$, the underlying continuous map of the identity morphism $\mathrm{id}_X \colon X \to X$ is equal to the identity morphism $\mathrm{id}_X$ in the category of topological spaces.

AlgebraicGeometry.PresheafedSpace.id_c theorem

(X : PresheafedSpace C) : (𝟙 X : X ⟶ X).c = 𝟙 X.presheaf

Full source

theorem id_c (X : PresheafedSpace C) :
    (𝟙 X : X ⟶ X).c = 𝟙 X.presheaf :=
  rfl

Identity Morphism of Presheafed Space Induces Identity on Presheaf

Informal description

For any presheafed space $X$ over a category $C$, the natural transformation component of the identity morphism $\mathrm{id}_X \colon X \to X$ is equal to the identity natural transformation of the presheaf $\mathcal{F}_X$ on $X$.

AlgebraicGeometry.PresheafedSpace.id_c_app theorem

(X : PresheafedSpace C) (U) : (𝟙 X : X ⟶ X).c.app U = X.presheaf.map (𝟙 U)

Full source

@[simp]
theorem id_c_app (X : PresheafedSpace C) (U) :
    (𝟙 X : X ⟶ X).c.app U = X.presheaf.map (𝟙 U) := by
  rw [id_c, map_id]
  rfl

Identity Natural Transformation Component Equals Identity Restriction Map

Informal description

For any presheafed space $X$ over a category $C$ and any open subset $U$ of the underlying topological space, the component of the identity natural transformation at $U$ is equal to the restriction map of the presheaf $\mathcal{F}_X$ induced by the identity morphism on $U$.

AlgebraicGeometry.PresheafedSpace.comp_base theorem

{X Y Z : PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).base = f.base ≫ g.base

Full source

@[simp]
theorem comp_base {X Y Z : PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).base = f.base ≫ g.base :=
  rfl

Composition of Morphisms of Presheafed Spaces Preserves Base Maps

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ between presheafed spaces over a category $C$, the underlying continuous map of the composition $f \circ g$ is equal to the composition of the underlying continuous maps of $f$ and $g$, i.e., $(f \circ g)_{\text{base}} = f_{\text{base}} \circ g_{\text{base}}$.

AlgebraicGeometry.PresheafedSpace.instCoeFunHomForallCarrierCarrier instance

(X Y : PresheafedSpace C) : CoeFun (X ⟶ Y) fun _ => (↑X → ↑Y)

Full source

instance (X Y : PresheafedSpace C) : CoeFun (X ⟶ Y) fun _ => (↑X → ↑Y) :=
  ⟨fun f => f.base⟩

Morphisms of Presheafed Spaces as Functions on Underlying Topological Spaces

Informal description

For any two presheafed spaces $X$ and $Y$ over a category $C$, a morphism $f \colon X \to Y$ in the category of presheafed spaces can be treated as a function from the underlying topological space of $X$ to the underlying topological space of $Y$.

AlgebraicGeometry.PresheafedSpace.comp_c_app theorem

 {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
  (α ≫ β).c.app U = β.c.app U ≫ α.c.app (op ((Opens.map β.base).obj (unop U)))

Full source

/-- Sometimes rewriting with `comp_c_app` doesn't work because of dependent type issues.
In that case, `erw comp_c_app_assoc` might make progress.
The lemma `comp_c_app_assoc` is also better suited for rewrites in the opposite direction. -/
@[reassoc, simp]
theorem comp_c_app {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
    (α ≫ β).c.app U = β.c.app U ≫ α.c.app (op ((Opens.map β.base).obj (unop U))) :=
  rfl

Composition of Natural Transformations in Presheafed Spaces

Informal description

For any morphisms $\alpha \colon X \to Y$ and $\beta \colon Y \to Z$ of presheafed spaces over a category $C$, and for any open subset $U$ in $Z$, the component of the natural transformation $(\alpha \circ \beta).c$ at $U$ is equal to the composition of the component of $\beta.c$ at $U$ with the component of $\alpha.c$ at the preimage of $U$ under $\beta$.

AlgebraicGeometry.PresheafedSpace.congr_app theorem

 {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
  α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl))

Full source

theorem congr_app {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
    α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl)) := by
  subst h
  simp

Equality of Presheafed Space Morphisms Implies Component-wise Equality of Natural Transformations

Informal description

Let $X$ and $Y$ be presheafed spaces over a category $C$, and let $\alpha, \beta: X \to Y$ be morphisms of presheafed spaces. If $\alpha = \beta$, then for any open set $U$ in $Y$, the component of the natural transformation $\alpha$ at $U$ equals the component of $\beta$ at $U$ composed with the restriction map induced by the equality $\alpha = \beta$. More precisely, for any open set $U$ in $Y$, we have: \[ \alpha_c(U) = \beta_c(U) \circ \mathcal{F}_X(\text{eqToHom}(h)) \] where $\mathcal{F}_X$ is the presheaf on $X$, $\alpha_c$ and $\beta_c$ are the natural transformations between presheaves, and $\text{eqToHom}(h)$ is the morphism induced by the equality $\alpha = \beta$.

AlgebraicGeometry.PresheafedSpace.forget definition

: PresheafedSpace C ⥤ TopCat

Full source

/-- The forgetful functor from `PresheafedSpace` to `TopCat`. -/
@[simps]
def forget : PresheafedSpacePresheafedSpace C ⥤ TopCat where
  obj X := (X : TopCat)
  map f := f.base

Forgetful functor from presheafed spaces to topological spaces

Informal description

The forgetful functor from the category of presheafed spaces over $C$ to the category of topological spaces. It maps a presheafed space $(X, \mathcal{F})$ to its underlying topological space $X$, and a morphism $(f, \alpha)$ between presheafed spaces to the underlying continuous map $f$.

AlgebraicGeometry.PresheafedSpace.isoOfComponents definition

(H : X.1 ≅ Y.1) (α : H.hom _* X.2 ≅ Y.2) : X ≅ Y

Full source

/-- An isomorphism of `PresheafedSpace`s is a homeomorphism of the underlying space, and a
natural transformation between the sheaves.
-/
@[simps hom inv]
def isoOfComponents (H : X.1 ≅ Y.1) (α : H.hom _* X.2H.hom _* X.2 ≅ Y.2) : X ≅ Y where
  hom :=
    { base := H.hom
      c := α.inv }
  inv :=
    { base := H.inv
      c := Presheaf.toPushforwardOfIso H α.hom }
  hom_inv_id := by ext <;> simp
  inv_hom_id := by
    ext
    · dsimp
      exact H.inv_hom_id_apply _
    dsimp
    simp only [Presheaf.toPushforwardOfIso_app, assoc, ← α.hom.naturality]
    simp only [eqToHom_map, eqToHom_app, eqToHom_trans_assoc, eqToHom_refl, id_comp]
    apply Iso.inv_hom_id_app

Isomorphism of Presheafed Spaces from Components

Informal description

Given two presheafed spaces $ X $ and $ Y $ over a category $ C $, an isomorphism $ H $ between their underlying topological spaces, and a natural isomorphism $ \alpha $ between the pushforward of $ X $'s presheaf along $ H $ and $ Y $'s presheaf, this constructs an isomorphism between the presheafed spaces $ X $ and $ Y $. The isomorphism consists of a homeomorphism $ H $ and a natural transformation $ \alpha $, satisfying the necessary coherence conditions.

AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso definition

(H : X ≅ Y) : Y.2 ≅ H.hom.base _* X.2

Full source

/-- Isomorphic `PresheafedSpace`s have naturally isomorphic presheaves. -/
@[simps]
def sheafIsoOfIso (H : X ≅ Y) : Y.2 ≅ H.hom.base _* X.2 where
  hom := H.hom.c
  inv := Presheaf.pushforwardToOfIso ((forget _).mapIso H).symm H.inv.c
  hom_inv_id := by
    ext U
    rw [NatTrans.comp_app]
    simpa using congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))
  inv_hom_id := by
    ext U
    dsimp
    rw [NatTrans.id_app]
    simp only [Presheaf.pushforwardToOfIso_app, Iso.symm_inv, mapIso_hom, forget_map,
      Iso.symm_hom, mapIso_inv, eqToHom_map, assoc]
    have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))
    have eq₂ := H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map
      ((forget C).congr_map H.inv_hom_id.symm)) U)).op
    rw [id_c, NatTrans.id_app, id_comp, eqToHom_map, comp_c_app] at eq₁
    rw [eqToHom_op, eqToHom_map] at eq₂
    erw [eq₂, reassoc_of% eq₁]
    simp

Natural isomorphism of presheaves induced by an isomorphism of presheafed spaces

Informal description

Given an isomorphism $ H \colon X \cong Y $ between presheafed spaces $ X $ and $ Y $ over a category $ C $, there is a natural isomorphism between the presheaf $ Y.2 $ on $ Y $ and the pushforward of the presheaf $ X.2 $ along the underlying homeomorphism $ H.hom.base $. This isomorphism is constructed using the natural transformations $ H.hom.c $ and $ H.inv.c $, and it satisfies the coherence conditions of an isomorphism in the category of presheaves.

AlgebraicGeometry.PresheafedSpace.base_isIso_of_iso instance

(f : X ⟶ Y) [IsIso f] : IsIso f.base

Full source

instance base_isIso_of_iso (f : X ⟶ Y) [IsIso f] : IsIso f.base :=
  ((forget _).mapIso (asIso f)).isIso_hom

Isomorphism of Underlying Topological Spaces from Presheafed Space Isomorphism

Informal description

For any morphism $f \colon X \to Y$ of presheafed spaces that is an isomorphism, the underlying continuous map $f_{\text{base}} \colon X \to Y$ is also an isomorphism in the category of topological spaces.

AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso instance

(f : X ⟶ Y) [IsIso f] : IsIso f.c

Full source

instance c_isIso_of_iso (f : X ⟶ Y) [IsIso f] : IsIso f.c :=
  (sheafIsoOfIso (asIso f)).isIso_hom

Isomorphism of Presheaf Natural Transformations from Presheafed Space Isomorphism

Informal description

For any isomorphism $f \colon X \to Y$ of presheafed spaces over a category $C$, the natural transformation $f_c$ between the presheaves is an isomorphism.

AlgebraicGeometry.PresheafedSpace.isIso_of_components theorem

(f : X ⟶ Y) [IsIso f.base] [IsIso f.c] : IsIso f

Full source

/-- This could be used in conjunction with `CategoryTheory.NatIso.isIso_of_isIso_app`. -/
theorem isIso_of_components (f : X ⟶ Y) [IsIso f.base] [IsIso f.c] : IsIso f :=
  (isoOfComponents (asIso f.base) (asIso f.c).symm).isIso_hom

Isomorphism of Presheafed Spaces from Component Isomorphisms

Informal description

Let $X$ and $Y$ be presheafed spaces over a category $C$, and let $f \colon X \to Y$ be a morphism of presheafed spaces. If both the underlying continuous map $f_{\text{base}} \colon X \to Y$ is an isomorphism of topological spaces and the natural transformation $f_c$ between the presheaves is an isomorphism, then $f$ itself is an isomorphism in the category of presheafed spaces.

AlgebraicGeometry.PresheafedSpace.restrict definition

{U : TopCat} (X : PresheafedSpace C) {f : U ⟶ (X : TopCat)} (h : IsOpenEmbedding f) : PresheafedSpace C

Full source

/-- The restriction of a presheafed space along an open embedding into the space.
-/
@[simps]
def restrict {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ (X : TopCat)}
    (h : IsOpenEmbedding f) : PresheafedSpace C where
  carrier := U
  presheaf := h.isOpenMap.functor.op ⋙ X.presheaf

Restriction of a presheafed space along an open embedding

Informal description

Given a presheafed space $ X $ over a category $ C $ and an open embedding $ f \colon U \to X $ from a topological space $ U $, the restriction $ X|_U $ is a presheafed space whose underlying topological space is $ U $ and whose presheaf is the composition of the functor induced by $ f $ on open sets (precomposed with the opposite functor) with the original presheaf of $ X $.

AlgebraicGeometry.PresheafedSpace.ofRestrict definition

{U : TopCat} (X : PresheafedSpace C) {f : U ⟶ (X : TopCat)} (h : IsOpenEmbedding f) : X.restrict h ⟶ X

Full source

/-- The map from the restriction of a presheafed space.
-/
@[simps]
def ofRestrict {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ (X : TopCat)}
    (h : IsOpenEmbedding f) : X.restrict h ⟶ X where
  base := f
  c :=
    { app := fun V => X.presheaf.map (h.isOpenMap.adjunction.counit.app V.unop).op
      naturality := fun U V f =>
        show _ = _ ≫ X.presheaf.map _ by
          rw [← map_comp, ← map_comp]
          rfl }

Inclusion morphism of a restricted presheafed space

Informal description

Given a presheafed space $ X $ over a category $ C $ and an open embedding $ f \colon U \to X $ from a topological space $ U $, the morphism $ X|_U \to X $ is defined by the continuous map $ f $ and a natural transformation between the presheaves. Specifically, the natural transformation is constructed by applying the original presheaf $ X.\text{presheaf} $ to the counit of the adjunction induced by the open map $ f $.

AlgebraicGeometry.PresheafedSpace.ofRestrict_mono instance

{U : TopCat} (X : PresheafedSpace C) (f : U ⟶ X.1) (hf : IsOpenEmbedding f) : Mono (X.ofRestrict hf)

Full source

instance ofRestrict_mono {U : TopCat} (X : PresheafedSpace C) (f : U ⟶ X.1)
    (hf : IsOpenEmbedding f) : Mono (X.ofRestrict hf) := by
  haveI : Mono f := (TopCat.mono_iff_injective _).mpr hf.injective
  constructor
  intro Z g₁ g₂ eq
  ext1
  · have := congr_arg PresheafedSpace.Hom.base eq
    simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
    rw [cancel_mono] at this
    exact this
  · ext V
    have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.isOpenMap.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    haveI :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.isOpenMap.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.isOpenMap.functor hf.isOpenMap.adjunction.counit) V
    have := PresheafedSpace.congr_app eq (op (hf.isOpenMap.functor.obj V))
    rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this
    have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
    simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h
    simp only [eqToHom_op, eqToHom_unop, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h
    simpa using h

Inclusion Morphism of a Restricted Presheafed Space is a Monomorphism

Informal description

For any presheafed space $X$ over a category $C$ and any open embedding $f \colon U \to X$ from a topological space $U$, the inclusion morphism $X|_U \to X$ is a monomorphism in the category of presheafed spaces.

AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf theorem

 (X : PresheafedSpace C) :
  (X.restrict (Opens.isOpenEmbedding ⊤)).presheaf = (Opens.inclusionTopIso X.carrier).inv _* X.presheaf

Full source

theorem restrict_top_presheaf (X : PresheafedSpace C) :
    (X.restrict (Opens.isOpenEmbedding ⊤)).presheaf =
      (Opens.inclusionTopIso X.carrier).inv _* X.presheaf := by
  dsimp
  rw [Opens.inclusion'_top_functor X.carrier]
  rfl

Equality of Presheaves for Whole Space Restriction

Informal description

For a presheafed space $X$ over a category $C$, the presheaf of the restriction of $X$ to the entire space (as an open subset) is equal to the pushforward of the original presheaf $X.\text{presheaf}$ along the inverse of the isomorphism between the whole space and its inclusion as an open subset.

AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c theorem

 (X : PresheafedSpace C) :
  (X.ofRestrict (Opens.isOpenEmbedding ⊤)).c =
    eqToHom
      (by
        rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
        erw [Iso.inv_hom_id]
        rw [Presheaf.id_pushforward]
        dsimp)

Full source

theorem ofRestrict_top_c (X : PresheafedSpace C) :
    (X.ofRestrict (Opens.isOpenEmbedding ⊤)).c =
      eqToHom
        (by
          rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
          erw [Iso.inv_hom_id]
          rw [Presheaf.id_pushforward]
          dsimp) := by
  /- another approach would be to prove the left hand side
       is a natural isomorphism, but I encountered a universe
       issue when `apply NatIso.isIso_of_isIso_app`. -/
  ext
  dsimp [ofRestrict]
  erw [eqToHom_map, eqToHom_app]
  simp

Natural transformation identity for whole-space restriction of a presheafed space

Informal description

Let $X$ be a presheafed space over a category $C$. The natural transformation component of the inclusion morphism $X|_{\top} \to X$ (where $X|_{\top}$ is the restriction of $X$ to the whole space) is equal to the identity morphism, up to the equality: 1. The presheaf of $X|_{\top}$ equals the pushforward of $X$'s presheaf along the inverse of the isomorphism between $X$ and its inclusion as an open subset. 2. The composition of pushforwards along the isomorphism and its inverse equals the identity pushforward. 3. The identity pushforward equals the identity functor on presheaves.

AlgebraicGeometry.PresheafedSpace.toRestrictTop definition

(X : PresheafedSpace C) : X ⟶ X.restrict (Opens.isOpenEmbedding ⊤)

Full source

/-- The map to the restriction of a presheafed space along the canonical inclusion from the top
subspace.
-/
@[simps]
def toRestrictTop (X : PresheafedSpace C) : X ⟶ X.restrict (Opens.isOpenEmbedding ⊤) where
  base := (Opens.inclusionTopIso X.carrier).inv
  c := eqToHom (restrict_top_presheaf X)

Morphism to the restriction of a presheafed space to the whole space

Informal description

Given a presheafed space $ X $ over a category $ C $, the morphism $ \text{toRestrictTop} $ from $ X $ to its restriction along the inclusion of the entire space (as an open subset) is defined as follows: - The underlying continuous map is the inverse of the isomorphism $ X \cong X $ (as the whole space). - The natural transformation between the presheaves is the identity, adjusted by the equality of presheaves established in $ \text{restrict\_top\_presheaf} $.

AlgebraicGeometry.PresheafedSpace.restrictTopIso definition

(X : PresheafedSpace C) : X.restrict (Opens.isOpenEmbedding ⊤) ≅ X

Full source

/-- The isomorphism from the restriction to the top subspace.
-/
@[simps]
def restrictTopIso (X : PresheafedSpace C) : X.restrict (Opens.isOpenEmbedding ⊤) ≅ X where
  hom := X.ofRestrict _
  inv := X.toRestrictTop
  hom_inv_id := by
    ext
    · rfl
    · erw [comp_c, toRestrictTop_c, whiskerRight_id',
        comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]
      rfl
  inv_hom_id := by
    ext
    · rfl
    · erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]
      rfl

Isomorphism between a presheafed space and its restriction to the whole space

Informal description

The isomorphism between a presheafed space $ X $ and its restriction to the entire topological space (as an open subset). Specifically, this isomorphism consists of: - A morphism $ X \to X|_{\text{top}} $ given by the inclusion of the whole space. - An inverse morphism $ X|_{\text{top}} \to X $ given by the identity map, adjusted by the equality of presheaves on the whole space.

AlgebraicGeometry.PresheafedSpace.Γ definition

: (PresheafedSpace C)ᵒᵖ ⥤ C

Full source

/-- The global sections, notated Gamma.
-/
@[simps]
def Γ : (PresheafedSpace C)ᵒᵖ(PresheafedSpace C)ᵒᵖ ⥤ C where
  obj X := (unop X).presheaf.obj (op ⊤)
  map f := f.unop.c.app (op ⊤)

Global sections functor for presheafed spaces

Informal description

The global sections functor $\Gamma$ for presheafed spaces is a contravariant functor from the opposite category of presheafed spaces over $C$ to $C$ itself. For a presheafed space $X$, $\Gamma(X)$ is defined as the value of the presheaf of $X$ on the entire space (i.e., $X.\text{presheaf}.\text{obj}(\text{op}\,\top)$). For a morphism $f \colon X \to Y$ of presheafed spaces, $\Gamma(f^{\text{op}})$ is given by the component of the natural transformation $f.c$ at the entire space.

AlgebraicGeometry.PresheafedSpace.Γ_obj_op theorem

(X : PresheafedSpace C) : Γ.obj (op X) = X.presheaf.obj (op ⊤)

Full source

theorem Γ_obj_op (X : PresheafedSpace C) : Γ.obj (op X) = X.presheaf.obj (op ⊤) :=
  rfl

Global Sections Functor Evaluation on Opposite Presheafed Space

Informal description

For any presheafed space $X$ over a category $C$, the value of the global sections functor $\Gamma$ at the opposite object $\mathrm{op}\,X$ is equal to the value of the presheaf of $X$ at the opposite of the entire space $\mathrm{op}\,\top$.

AlgebraicGeometry.PresheafedSpace.Γ_map_op theorem

{X Y : PresheafedSpace C} (f : X ⟶ Y) : Γ.map f.op = f.c.app (op ⊤)

Full source

theorem Γ_map_op {X Y : PresheafedSpace C} (f : X ⟶ Y) : Γ.map f.op = f.c.app (op ⊤) :=
  rfl

Global Sections Functor Maps Morphisms via Natural Transformation Components

Informal description

For any morphism $f \colon X \to Y$ of presheafed spaces over a category $C$, the map $\Gamma(f^{\mathrm{op}})$ induced by the global sections functor $\Gamma$ is equal to the component of the natural transformation $f.c$ at the entire space (i.e., at $\mathrm{op}\,\top$).

CategoryTheory.Functor.mapPresheaf definition

(F : C ⥤ D) : PresheafedSpace C ⥤ PresheafedSpace D

Full source

/-- We can apply a functor `F : C ⥤ D` to the values of the presheaf in any `PresheafedSpace C`,
    giving a functor `PresheafedSpace C ⥤ PresheafedSpace D` -/
def mapPresheaf (F : C ⥤ D) : PresheafedSpacePresheafedSpace C ⥤ PresheafedSpace D where
  obj X :=
    { carrier := X.carrier
      presheaf := X.presheaf ⋙ F }
  map f :=
    { base := f.base
      c := whiskerRight f.c F }
  -- Porting note: these proofs were automatic in mathlib3
  map_id X := by
    ext U
    · rfl
    · simp
  map_comp f g := by
    ext U
    · rfl
    · simp

Functor application to presheafed spaces

Informal description

Given a functor $ F \colon C \to D $ between categories, the functor `mapPresheaf` applies $ F $ to the values of the presheaf in any presheafed space over $ C $, producing a presheafed space over $ D $. Concretely, for a presheafed space $ X $ over $ C $, the resulting presheafed space has: - The same underlying topological space as $ X $. - A presheaf obtained by composing $ X $'s original presheaf with $ F $. For a morphism $ f \colon X \to Y $ of presheafed spaces over $ C $, the induced morphism $ F.mapPresheaf.map f $ has: - The same underlying continuous map as $ f $. - A natural transformation obtained by whiskering $ f $'s natural transformation with $ F $. This construction preserves identities and composition of morphisms.

CategoryTheory.Functor.mapPresheaf_obj_X theorem

(F : C ⥤ D) (X : PresheafedSpace C) : (F.mapPresheaf.obj X : TopCat) = (X : TopCat)

Full source

@[simp]
theorem mapPresheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace C) :
    (F.mapPresheaf.obj X : TopCat) = (X : TopCat) :=
  rfl

Preservation of Underlying Topological Space by Functor Application to Presheafed Spaces

Informal description

Given a functor $F \colon C \to D$ between categories and a presheafed space $X$ over $C$, the underlying topological space of the presheafed space obtained by applying $F$ to $X$ is equal to the underlying topological space of $X$. That is, $(F.mapPresheaf.obj X : \text{TopCat}) = (X : \text{TopCat})$.

CategoryTheory.Functor.mapPresheaf_obj_presheaf theorem

(F : C ⥤ D) (X : PresheafedSpace C) : (F.mapPresheaf.obj X).presheaf = X.presheaf ⋙ F

Full source

@[simp]
theorem mapPresheaf_obj_presheaf (F : C ⥤ D) (X : PresheafedSpace C) :
    (F.mapPresheaf.obj X).presheaf = X.presheaf ⋙ F :=
  rfl

Presheaf Composition under Functor Application to Presheafed Spaces

Informal description

Given a functor $F \colon C \to D$ between categories and a presheafed space $X$ over $C$, the presheaf of the image of $X$ under the functor `mapPresheaf F` is equal to the composition of $X$'s original presheaf with $F$. That is, $(F.\text{mapPresheaf}.obj\,X).\text{presheaf} = X.\text{presheaf} \circ F$.

CategoryTheory.Functor.mapPresheaf_map_f theorem

(F : C ⥤ D) {X Y : PresheafedSpace C} (f : X ⟶ Y) : (F.mapPresheaf.map f).base = f.base

Full source

@[simp]
theorem mapPresheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace C} (f : X ⟶ Y) :
    (F.mapPresheaf.map f).base = f.base :=
  rfl

Functor Application Preserves Underlying Continuous Maps in Presheafed Spaces

Informal description

Given a functor $F \colon C \to D$ between categories and a morphism $f \colon X \to Y$ of presheafed spaces over $C$, the underlying continuous map of the induced morphism $F.\text{mapPresheaf}.map f$ is equal to the underlying continuous map of $f$, i.e., $(F.\text{mapPresheaf}.map f).\text{base} = f.\text{base}$.

CategoryTheory.Functor.mapPresheaf_map_c theorem

(F : C ⥤ D) {X Y : PresheafedSpace C} (f : X ⟶ Y) : (F.mapPresheaf.map f).c = whiskerRight f.c F

Full source

@[simp]
theorem mapPresheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace C} (f : X ⟶ Y) :
    (F.mapPresheaf.map f).c = whiskerRight f.c F :=
  rfl

Natural Transformation Component under Functor Application to Presheafed Spaces

Informal description

Given a functor $F \colon C \to D$ between categories and a morphism $f \colon X \to Y$ of presheafed spaces over $C$, the natural transformation component of the induced morphism $F.\text{mapPresheaf}.map f$ is equal to the right whiskering of $f$'s natural transformation with $F$, i.e., $(F.\text{mapPresheaf}.map f).c = f.c \circ F$.

CategoryTheory.NatTrans.onPresheaf definition

{F G : C ⥤ D} (α : F ⟶ G) : G.mapPresheaf ⟶ F.mapPresheaf

Full source

/-- A natural transformation induces a natural transformation between the `map_presheaf` functors.
-/
def onPresheaf {F G : C ⥤ D} (α : F ⟶ G) : G.mapPresheaf ⟶ F.mapPresheaf where
  app X :=
    { base := 𝟙 _
      c := whiskerLeft X.presheaf α ≫ eqToHom (Presheaf.Pushforward.id_eq _).symm }

-- TODO Assemble the last two constructions into a functor
--   `(C ⥤ D) ⥤ (PresheafedSpace C ⥤ PresheafedSpace D)`

Natural transformation induced on presheafed spaces

Informal description

Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to D$, the induced natural transformation $\text{onPresheaf}\, \alpha$ between the functors $\text{mapPresheaf}\, G$ and $\text{mapPresheaf}\, F$ on presheafed spaces is defined as follows: For each presheafed space $X$ over $C$, the component at $X$ consists of: - The identity morphism on the underlying topological space of $X$. - A natural transformation obtained by left whiskering the presheaf of $X$ with $\alpha$, followed by an isomorphism adjusting for the pushforward identity.