Mathlib.Topology.Sheaves.Presheaf

TopCat.Presheaf definition

(X : TopCat.{w}) : Type max u v w

Full source

/-- The category of `C`-valued presheaves on a (bundled) topological space `X`. -/
def Presheaf (X : TopCatTopCat.{w}) : Type max u v w :=
  (Opens X)ᵒᵖ(Opens X)ᵒᵖ ⥤ C

$C$-valued presheaves on a topological space

Informal description

The category of $C$-valued presheaves on a topological space $X$ is defined as the functor category from the opposite category of open subsets of $X$ to the category $C$.

TopCat.instCategoryPresheaf instance

(X : TopCat.{w}) : Category (Presheaf.{w, v, u} C X)

Full source

instance (X : TopCatTopCat.{w}) : Category (Presheaf.{w, v, u} C X) :=
  inferInstanceAs (Category ((Opens X)ᵒᵖ(Opens X)ᵒᵖ ⥤ C : Type max u v w))

Category Structure on Presheaves of a Topological Space

Informal description

For any topological space $X$ and any category $C$, the category of $C$-valued presheaves on $X$ is defined as the functor category from the opposite category of open subsets of $X$ to $C$. This category has natural transformations as morphisms between presheaves.

TopCat.Presheaf.comp_app theorem

 {X : TopCat} {U : (Opens X)ᵒᵖ} {P Q R : Presheaf C X} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).app U = f.app U ≫ g.app U

Full source

@[simp] theorem comp_app {X : TopCat} {U : (Opens X)ᵒᵖ} {P Q R : Presheaf C X}
    (f : P ⟶ Q) (g : Q ⟶ R) :
    (f ≫ g).app U = f.app U ≫ g.app U := rfl

Composition of Natural Transformations of Presheaves Commutes with Application

Informal description

For any topological space $X$, any open subset $U$ of $X$ (viewed in the opposite category), and any natural transformations $f \colon P \to Q$ and $g \colon Q \to R$ between presheaves $P, Q, R$ on $X$, the application of the composition $f \circ g$ to $U$ is equal to the composition of the applications of $f$ and $g$ to $U$, i.e., $(f \circ g)(U) = f(U) \circ g(U)$.

TopCat.Presheaf.ext theorem

{X : TopCat} {P Q : Presheaf C X} {f g : P ⟶ Q} (w : ∀ U : Opens X, f.app (op U) = g.app (op U)) : f = g

Full source

@[ext]
lemma ext {X : TopCat} {P Q : Presheaf C X} {f g : P ⟶ Q}
    (w : ∀ U : Opens X, f.app (op U) = g.app (op U)) :
    f = g := by
  apply NatTrans.ext
  ext U
  induction U with | _ U => ?_
  apply w

Extensionality of Natural Transformations between Presheaves

Informal description

Let $X$ be a topological space and $C$ be a category. For any two natural transformations $f, g \colon P \to Q$ between presheaves $P, Q \colon (\text{Opens } X)^{\mathrm{op}} \to C$, if $f_U = g_U$ for every open subset $U$ of $X$, then $f = g$.

TopCat.Presheaf.attrSheaf_restrict definition

: Lean.ParserDescr✝

Full source

macromacro "sheaf_restrict" : attr =>
  `(attr|aesop safe 50 apply (rule_sets := [$(Lean.mkIdent `Restrict):ident]))

Sheaf restriction attribute

Informal description

The attribute `sheaf_restrict` is used to mark lemmas related to restricting sheaves, enabling them to be automatically applied by the Aesop tactic with a safety level of 50 in the `Restrict` rule set.

TopCat.Presheaf.restrict_tac definition

: Lean.ParserDescr✝

Full source

macro (name := restrict_tac) "restrict_tac" c:Aesop.tactic_clause* : tactic =>
`(tactic| first | assumption |
  aesop $c*
    (config := { terminal := true
                 assumptionTransparency := .reducible
                 enableSimp := false })
    (rule_sets := [-default, -builtin, $(Lean.mkIdent `Restrict):ident]))

Tactic for solving subset relations in presheaves

Informal description

The tactic `restrict_tac` is used to solve relations among subsets in the context of presheaves on topological spaces. It combines Aesop's automation capabilities with a specific rule set focused on restriction operations, excluding default and builtin rules.

TopCat.Presheaf.restrict_tac? definition

: Lean.ParserDescr✝

Full source

macro (name := restrict_tac?) "restrict_tac?" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  aesop? $c*
    (config := { terminal := true
                 assumptionTransparency := .reducible
                 enableSimp := false
                 maxRuleApplications := 300 })
  (rule_sets := [-default, -builtin, $(Lean.mkIdent `Restrict):ident]))

Restriction tactic suggestion macro

Informal description

The macro `restrict_tac?` is a tactic that invokes the `aesop?` tactic with specific configuration settings for use in presheaf restriction proofs. It sets: - Terminal mode to true - Assumption transparency to reducible - Disables simp - Limits to 300 rule applications - Uses a custom rule set excluding default and builtin rules, while including rules marked for restriction

TopCat.Presheaf.restrict definition

{F : X.Presheaf C} {V : Opens X} (x : ToType (F.obj (op V))) {U : Opens X} (h : U ⟶ V) : ToType (F.obj (op U))

Full source

/-- The restriction of a section along an inclusion of open sets.
For `x : F.obj (op V)`, we provide the notation `x |_ₕ i` (`h` stands for `hom`) for `i : U ⟶ V`,
and the notation `x |_ₗ U ⟪i⟫` (`l` stands for `le`) for `i : U ≤ V`.
-/
def restrict {F : X.Presheaf C}
    {V : Opens X} (x : ToType (F.obj (op V))) {U : Opens X} (h : U ⟶ V) : ToType (F.obj (op U)) :=
  F.map h.op x

Restriction of a presheaf section along an inclusion of open sets

Informal description

Given a presheaf $ F $ on a topological space $ X $, an open set $ V \subseteq X $, and a section $ x \in F(V) $, the restriction of $ x $ along an inclusion $ h : U \hookrightarrow V $ of open sets is the element $ F(h)(x) \in F(U) $, where $ F(h) $ is the restriction map associated to the inclusion $ h $. Notation: For $ x \in F(V) $ and $ h : U \hookrightarrow V $, the restriction is denoted $ x \mid_h U $ or $ x \mid_{\leq} U \llcorner h \lrcorner $.

AlgebraicGeometry.term_|_ₕ_ definition

: Lean.TrailingParserDescr✝

Full source

/-- restriction of a section along an inclusion -/
scoped[AlgebraicGeometry] infixl:80 " |_ₕ " => TopCat.Presheaf.restrict

Restriction of a presheaf section

Informal description

The notation $ s \mid_h U $ denotes the restriction of a section $ s $ of a presheaf $ F $ on a topological space $ X $ to an open subset $ U $, where $ h $ is the inclusion $ U \hookrightarrow V $ for some open subset $ V $ containing $ U $.

AlgebraicGeometry.term_|_ₗ_⟪_⟫ definition

: Lean.TrailingParserDescr✝

Full source

/-- restriction of a section along a subset relation -/
scoped[AlgebraicGeometry] notation:80 x " |_ₗ " U " ⟪" e "⟫ " =>
  @TopCat.Presheaf.restrict _ _ _ _ _ _ _ _ _ x U (@homOfLE (Opens _) _ U _ e)

Restriction of presheaf sections along inclusion

Informal description

Given a presheaf $\mathcal{F}$ on a topological space $X$, an open subset $U \subseteq X$, and an inclusion $e : V \subseteq U$ of open subsets, the notation $\mathcal{F} \big|_{V} \llbracket e \rrbracket$ denotes the restriction of a section of $\mathcal{F}$ from $U$ to $V$ along the inclusion $e$.

AlgebraicGeometry.term_|__ definition

: Lean.TrailingParserDescr✝

Full source

/-- restriction of a section to open subset -/
scoped[AlgebraicGeometry] infixl:80 " |_ " => TopCat.Presheaf.restrictOpen

Restriction of a presheaf section to an open subset

Informal description

The notation $s \mid_U$ denotes the restriction of a section $s$ of a presheaf to an open subset $U$.

TopCat.Presheaf.restrict_restrict theorem

 {F : X.Presheaf C} {U V W : Opens X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : ToType (F.obj (op W))) : x |_ V |_ U = x |_ U

Full source

theorem restrict_restrict
    {F : X.Presheaf C} {U V W : Opens X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : ToType (F.obj (op W))) :
    x |_ Vx |_ V |_ U = x |_ U := by
  delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]
  rfl

Composition of Restrictions of Presheaf Sections

Informal description

Let $X$ be a topological space and $\mathcal{F}$ a $C$-valued presheaf on $X$. For any open subsets $U \subseteq V \subseteq W$ of $X$ and any section $x \in \mathcal{F}(W)$, the restriction of $x$ to $V$ followed by restriction to $U$ equals the direct restriction of $x$ to $U$, i.e., $$ x|_{V}|_{U} = x|_{U}. $$

TopCat.Presheaf.map_restrict theorem

 {F G : X.Presheaf C} (e : F ⟶ G) {U V : Opens X} (h : U ≤ V) (x : ToType (F.obj (op V))) :
  e.app _ (x |_ U) = e.app _ x |_ U

Full source

theorem map_restrict
    {F G : X.Presheaf C} (e : F ⟶ G) {U V : Opens X} (h : U ≤ V) (x : ToType (F.obj (op V))) :
    e.app _ (x |_ U) = e.app _ x |_ U := by
  delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, NatTrans.naturality, ConcreteCategory.comp_apply]

Naturality of Restriction for Presheaf Morphisms

Informal description

Let $X$ be a topological space and $C$ a category. For any presheaves $F, G$ on $X$ with values in $C$, any natural transformation $e : F \to G$, any open subsets $U \subseteq V$ of $X$, and any section $x \in F(V)$, the following diagram commutes: $$ e_U(x|_U) = (e_V(x))|_U $$ where $x|_U$ denotes the restriction of $x$ to $U$ and $e_U$ is the component of $e$ at $U$.

TopCat.Presheaf.pushforward definition

{X Y : TopCat.{w}} (f : X ⟶ Y) : X.Presheaf C ⥤ Y.Presheaf C

Full source

/-- The pushforward functor. -/
@[simps!]
def pushforward {X Y : TopCatTopCat.{w}} (f : X ⟶ Y) : X.Presheaf C ⥤ Y.Presheaf C :=
  (whiskeringLeft _ _ _).obj (Opens.map f).op

Pushforward of a presheaf along a continuous map

Informal description

Given topological spaces $ X $ and $ Y $ and a continuous map $ f \colon X \to Y $, the pushforward functor $ f_* $ sends a presheaf $ \mathcal{F} $ on $ X $ to a presheaf $ f_*\mathcal{F} $ on $ Y $, where for each open set $ V \subseteq Y $, $ (f_*\mathcal{F})(V) = \mathcal{F}(f^{-1}(V)) $. This is constructed using the left whiskering functor applied to the opposite of the preimage functor $ \text{Opens.map}\, f $.

AlgebraicGeometry.term__*_ definition

: Lean.TrailingParserDescr✝

Full source

/-- push forward of a presheaf -/
scoped[AlgebraicGeometry] notation f:80 " _* " P:81 =>
  Prefunctor.obj (Functor.toPrefunctor (TopCat.Presheaf.pushforward _ f)) P

Pushforward of a presheaf

Informal description

Given a continuous map $f \colon X \to Y$ between topological spaces and a presheaf $\mathcal{F}$ on $X$, the pushforward $f_*\mathcal{F}$ is the presheaf on $Y$ defined by $(f_*\mathcal{F})(V) = \mathcal{F}(f^{-1}(V))$ for each open set $V \subseteq Y$.

TopCat.Presheaf.pushforward_map_app' theorem

 {X Y : TopCat.{w}} (f : X ⟶ Y) {ℱ 𝒢 : X.Presheaf C} (α : ℱ ⟶ 𝒢) {U : (Opens Y)ᵒᵖ} :
  ((pushforward C f).map α).app U = α.app (op <| (Opens.map f).obj U.unop)

Full source

@[simp]
theorem pushforward_map_app' {X Y : TopCatTopCat.{w}} (f : X ⟶ Y) {ℱ 𝒢 : X.Presheaf C} (α : ℱ ⟶ 𝒢)
    {U : (Opens Y)ᵒᵖ} : ((pushforward C f).map α).app U = α.app (op <| (Opens.map f).obj U.unop) :=
  rfl

Naturality of Pushforward at Open Sets

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous map, and $\mathcal{F}, \mathcal{G}$ be $C$-valued presheaves on $X$. For any natural transformation $\alpha \colon \mathcal{F} \to \mathcal{G}$ and any open set $U \subseteq Y$, the component of the pushforward natural transformation $f_*\alpha$ at $U$ is equal to the component of $\alpha$ at the preimage $f^{-1}(U)$. That is, $(f_*\alpha)_U = \alpha_{f^{-1}(U)}$.

TopCat.Presheaf.id_pushforward theorem

(X : TopCat.{w}) : pushforward C (𝟙 X) = 𝟭 (X.Presheaf C)

Full source

lemma id_pushforward (X : TopCatTopCat.{w}) : pushforward C (𝟙 X) = 𝟭 (X.Presheaf C) := rfl

Identity Pushforward Functor Equals Identity Functor on Presheaves

Informal description

For any topological space $X$, the pushforward functor along the identity morphism $\mathrm{id}_X$ is equal to the identity functor on the category of $C$-valued presheaves on $X$. That is, $(\mathrm{id}_X)_* = \mathrm{id}_{\mathrm{Presheaf}\,C\,X}$.

TopCat.Presheaf.Pushforward.id definition

{X : TopCat.{w}} (ℱ : X.Presheaf C) : 𝟙 X _* ℱ ≅ ℱ

Full source

/-- The natural isomorphism between the pushforward of a presheaf along the identity continuous map
and the original presheaf. -/
def id {X : TopCatTopCat.{w}} (ℱ : X.Presheaf C) : 𝟙𝟙 X _* ℱ𝟙 X _* ℱ ≅ ℱ := Iso.refl _

Identity pushforward isomorphism for presheaves

Informal description

For any topological space $ X $ and any presheaf $ \mathcal{F} $ on $ X $, there is a natural isomorphism between the pushforward of $ \mathcal{F} $ along the identity continuous map $ \text{id}_X $ and $ \mathcal{F} $ itself. This isomorphism is given by the identity natural transformation.

TopCat.Presheaf.Pushforward.id_hom_app theorem

{X : TopCat.{w}} (ℱ : X.Presheaf C) (U) : (id ℱ).hom.app U = 𝟙 _

Full source

@[simp]
theorem id_hom_app {X : TopCatTopCat.{w}} (ℱ : X.Presheaf C) (U) : (id ℱ).hom.app U = 𝟙 _ := rfl

Identity Pushforward Natural Transformation Component at Open Set

Informal description

For any topological space $X$, any presheaf $\mathcal{F}$ on $X$ with values in a category $C$, and any open subset $U \subseteq X$, the component at $U$ of the natural isomorphism homomorphism between $(\mathrm{id}_X)_* \mathcal{F}$ and $\mathcal{F}$ is equal to the identity morphism on $\mathcal{F}(U)$.

TopCat.Presheaf.Pushforward.id_inv_app theorem

{X : TopCat.{w}} (ℱ : X.Presheaf C) (U) : (id ℱ).inv.app U = 𝟙 _

Full source

@[simp]
theorem id_inv_app {X : TopCatTopCat.{w}} (ℱ : X.Presheaf C) (U) :
    (id ℱ).inv.app U = 𝟙 _ := rfl

Inverse Component of Identity Pushforward Isomorphism is Identity

Informal description

For any topological space $X$, any presheaf $\mathcal{F}$ on $X$, and any open subset $U \subseteq X$, the inverse component of the identity pushforward isomorphism at $U$ is equal to the identity morphism on $\mathcal{F}(U)$.

TopCat.Presheaf.Pushforward.id_eq theorem

{X : TopCat.{w}} (ℱ : X.Presheaf C) : 𝟙 X _* ℱ = ℱ

Full source

theorem id_eq {X : TopCatTopCat.{w}} (ℱ : X.Presheaf C) : 𝟙𝟙 X _* ℱ = ℱ := rfl

Identity Pushforward Preserves Presheaf Isomorphism

Informal description

For any topological space $X$ and any presheaf $\mathcal{F}$ on $X$, the pushforward of $\mathcal{F}$ along the identity morphism $\mathrm{id}_X$ is isomorphic to $\mathcal{F}$ itself, i.e., $(\mathrm{id}_X)_* \mathcal{F} \cong \mathcal{F}$.

TopCat.Presheaf.Pushforward.comp definition

{X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ)

Full source

/-- The natural isomorphism between
the pushforward of a presheaf along the composition of two continuous maps and
the corresponding pushforward of a pushforward. -/
def comp {X Y Z : TopCatTopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) :
    (f ≫ g) _* ℱ(f ≫ g) _* ℱ ≅ g _* (f _* ℱ) := Iso.refl _

Natural isomorphism for composition of pushforwards of presheaves

Informal description

Given topological spaces $ X, Y, Z $, continuous maps $ f \colon X \to Y $ and $ g \colon Y \to Z $, and a presheaf $ \mathcal{F} $ on $ X $, there is a natural isomorphism between the pushforward of $ \mathcal{F} $ along the composition $ f \circ g $ and the pushforward of $ f_*\mathcal{F} $ along $ g $.

TopCat.Presheaf.Pushforward.comp_eq theorem

{X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) : (f ≫ g) _* ℱ = g _* (f _* ℱ)

Full source

theorem comp_eq {X Y Z : TopCatTopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) :
    (f ≫ g) _* ℱ = g _* (f _* ℱ) :=
  rfl

Composition Law for Pushforward of Presheaves

Informal description

For any topological spaces $X$, $Y$, and $Z$, continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, and a presheaf $\mathcal{F}$ on $X$, the pushforward of $\mathcal{F}$ along the composition $f \circ g$ is equal to the pushforward along $g$ of the pushforward of $\mathcal{F}$ along $f$, i.e., $(f \circ g)_* \mathcal{F} = g_* (f_* \mathcal{F})$.

TopCat.Presheaf.Pushforward.comp_hom_app theorem

{X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) : (comp f g ℱ).hom.app U = 𝟙 _

Full source

@[simp]
theorem comp_hom_app {X Y Z : TopCatTopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) :
    (comp f g ℱ).hom.app U = 𝟙 _ := rfl

Identity Component of Pushforward Composition Natural Transformation

Informal description

For any topological spaces $X$, $Y$, and $Z$, continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, a presheaf $\mathcal{F}$ on $X$, and any open set $U$ in $Z$, the component of the natural transformation $(f \circ g)_* \mathcal{F} \to g_* (f_* \mathcal{F})$ at $U$ is equal to the identity morphism on $(g_* (f_* \mathcal{F}))(U)$.

TopCat.Presheaf.Pushforward.comp_inv_app theorem

{X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) : (comp f g ℱ).inv.app U = 𝟙 _

Full source

@[simp]
theorem comp_inv_app {X Y Z : TopCatTopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) :
    (comp f g ℱ).inv.app U = 𝟙 _ := rfl

Identity Property of Pushforward Composition Inverse Components

Informal description

For topological spaces $X$, $Y$, $Z$, continuous maps $f \colon X \to Y$ and $g \colon Y \to Z$, a presheaf $\mathcal{F}$ on $X$, and any open set $U \subseteq Z$, the inverse component of the natural isomorphism $(f \circ g)_* \mathcal{F} \cong g_* (f_* \mathcal{F})$ at $U$ is equal to the identity morphism on $(g_* (f_* \mathcal{F}))(U)$.

TopCat.Presheaf.pushforwardEq definition

{X Y : TopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) : f _* ℱ ≅ g _* ℱ

Full source

/--
An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf
along those maps.
-/
def pushforwardEq {X Y : TopCatTopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) :
    f _* ℱf _* ℱ ≅ g _* ℱ :=
  isoWhiskerRight (NatIso.op (Opens.mapIso f g h).symm) ℱ

Natural isomorphism of pushforward presheaves for equal continuous maps

Informal description

Given topological spaces $ X $ and $ Y $, two continuous maps $ f, g \colon X \to Y $ that are equal (i.e., $ f = g $), and a presheaf $ \mathcal{F} $ on $ X $, there is a natural isomorphism between the pushforward presheaves $ f_* \mathcal{F} $ and $ g_* \mathcal{F} $. This isomorphism is constructed by whiskering the opposite of the natural isomorphism between the preimage functors $ \text{Opens.map}\, f $ and $ \text{Opens.map}\, g $ (induced by $ f = g $) with the presheaf $ \mathcal{F} $.

TopCat.Presheaf.pushforward_eq' theorem

{X Y : TopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) : f _* ℱ = g _* ℱ

Full source

theorem pushforward_eq' {X Y : TopCatTopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) :
    f _* ℱ = g _* ℱ := by rw [h]

Equality of Pushforward Presheaves for Equal Continuous Maps

Informal description

For any topological spaces $X$ and $Y$, given continuous maps $f, g \colon X \to Y$ that are equal (i.e., $f = g$), and any presheaf $\mathcal{F}$ on $X$, the pushforward presheaves $f_*\mathcal{F}$ and $g_*\mathcal{F}$ are equal.

TopCat.Presheaf.pushforwardEq_hom_app theorem

 {X Y : TopCat.{w}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.Presheaf C) (U) :
  (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom (by aesop_cat))

Full source

@[simp]
theorem pushforwardEq_hom_app {X Y : TopCatTopCat.{w}} {f g : X ⟶ Y}
    (h : f = g) (ℱ : X.Presheaf C) (U) :
    (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom (by aesop_cat)) := by
  simp [pushforwardEq]

Component of Pushforward Isomorphism for Equal Maps

Informal description

Let $X$ and $Y$ be topological spaces, and let $f, g : X \to Y$ be continuous maps such that $f = g$. For any presheaf $\mathcal{F}$ on $X$ and any open set $U \subseteq Y$, the component of the natural isomorphism $(f_*\mathcal{F} \cong g_*\mathcal{F})$ at $U$ is equal to the map $\mathcal{F}(f^{-1}(U)) \to \mathcal{F}(g^{-1}(U))$ induced by the identity morphism (since $f^{-1}(U) = g^{-1}(U)$).

TopCat.Presheaf.presheafEquivOfIso definition

{X Y : TopCat} (H : X ≅ Y) : X.Presheaf C ≌ Y.Presheaf C

Full source

/-- A homeomorphism of spaces gives an equivalence of categories of presheaves. -/
@[simps!]
def presheafEquivOfIso {X Y : TopCat} (H : X ≅ Y) : X.Presheaf C ≌ Y.Presheaf C :=
  Equivalence.congrLeft (Opens.mapMapIso H).symm.op

Equivalence of presheaf categories induced by a homeomorphism

Informal description

Given a homeomorphism $H \colon X \cong Y$ between topological spaces $X$ and $Y$, there is an equivalence of categories between the categories of $C$-valued presheaves on $X$ and $Y$. This equivalence is constructed by precomposing with the equivalence of categories of open sets induced by $H^{-1}$ (viewed as a contravariant operation via the opposite category construction).

TopCat.Presheaf.toPushforwardOfIso definition

 {X Y : TopCat} (H : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C} (α : H.hom _* ℱ ⟶ 𝒢) : ℱ ⟶ H.inv _* 𝒢

Full source

/-- If `H : X ≅ Y` is a homeomorphism,
then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
-/
def toPushforwardOfIso {X Y : TopCat} (H : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C}
    (α : H.hom _* ℱH.hom _* ℱ ⟶ 𝒢) : ℱ ⟶ H.inv _* 𝒢 :=
  (presheafEquivOfIso _ H).toAdjunction.homEquiv ℱ 𝒢 α

Morphism from pushforward along homeomorphism to pullback along inverse homeomorphism

Informal description

Given a homeomorphism $H \colon X \cong Y$ between topological spaces $X$ and $Y$, and presheaves $\mathcal{F}$ on $X$ and $\mathcal{G}$ on $Y$, any morphism $\alpha \colon H_*\mathcal{F} \to \mathcal{G}$ induces a morphism $\mathcal{F} \to H^{-1}_*\mathcal{G}$ via the adjunction equivalence between the pushforward and pullback functors induced by $H$.

TopCat.Presheaf.toPushforwardOfIso_app theorem

 {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C} (H₂ : H₁.hom _* ℱ ⟶ 𝒢) (U : (Opens X)ᵒᵖ) :
  (toPushforwardOfIso H₁ H₂).app U =
    ℱ.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))

Full source

@[simp]
theorem toPushforwardOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C}
    (H₂ : H₁.hom _* ℱH₁.hom _* ℱ ⟶ 𝒢) (U : (Opens X)ᵒᵖ) :
    (toPushforwardOfIso H₁ H₂).app U =
      ℱ.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) ≫
        H₂.app (op ((Opens.map H₁.inv).obj (unop U))) := by
  simp [toPushforwardOfIso, Adjunction.homEquiv_unit]

Component Formula for Induced Presheaf Morphism via Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces with a homeomorphism $H \colon X \cong Y$, and let $\mathcal{F}$ and $\mathcal{G}$ be presheaves on $X$ and $Y$ respectively. Given a natural transformation $\alpha \colon H_*\mathcal{F} \to \mathcal{G}$ and an open set $U \subseteq X$, the component of the induced morphism $\mathcal{F} \to H^{-1}_*\mathcal{G}$ at $U$ is given by: \[ (\mathcal{F} \to H^{-1}_*\mathcal{G})_U = \mathcal{F}(\text{id}_U) \circ \alpha_{H^{-1}(U)} \] where $\text{id}_U$ denotes the identity morphism on $U$ and $\alpha_{H^{-1}(U)}$ is the component of $\alpha$ at the open set $H^{-1}(U) \subseteq Y$.

TopCat.Presheaf.pushforwardToOfIso definition

 {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) : H₁.inv _* ℱ ⟶ 𝒢

Full source

/-- If `H : X ≅ Y` is a homeomorphism,
then given an `H _* ℱ ⟶ 𝒢`, we may obtain an `ℱ ⟶ H ⁻¹ _* 𝒢`.
-/
def pushforwardToOfIso {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C}
    (H₂ : ℱ ⟶ H₁.hom _* 𝒢) : H₁.inv _* ℱH₁.inv _* ℱ ⟶ 𝒢 :=
  ((presheafEquivOfIso _ H₁.symm).toAdjunction.homEquiv ℱ 𝒢).symm H₂

Transformation from pushforward along homeomorphism inverse

Informal description

Given a homeomorphism $ H : X \cong Y $ between topological spaces $ X $ and $ Y $, and a natural transformation $ \alpha : \mathcal{F} \to H_* \mathcal{G} $ where $ \mathcal{F} $ is a presheaf on $ Y $ and $ \mathcal{G} $ is a presheaf on $ X $, the function constructs a natural transformation $ H^{-1}_* \mathcal{F} \to \mathcal{G} $. This is obtained by applying the inverse of the hom-set equivalence from the adjunction induced by the equivalence of presheaf categories given by $ H^{-1} $.

TopCat.Presheaf.pushforwardToOfIso_app theorem

 {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (Opens X)ᵒᵖ) :
  (pushforwardToOfIso H₁ H₂).app U =
    H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom (by simp [Opens.map, Set.preimage_preimage]))

Full source

@[simp]
theorem pushforwardToOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C}
    (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (Opens X)ᵒᵖ) :
    (pushforwardToOfIso H₁ H₂).app U =
      H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫
        𝒢.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) := by
  simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]

Component Formula for Pushforward Transformation Along Homeomorphism Inverse

Informal description

Let $X$ and $Y$ be topological spaces with a homeomorphism $H_1 : X \cong Y$, and let $\mathcal{F}$ be a presheaf on $Y$ and $\mathcal{G}$ a presheaf on $X$. Given a natural transformation $\alpha : \mathcal{F} \to H_{1*}\mathcal{G}$ and an open set $U$ in $X$ (viewed as an object in the opposite category of open sets), the component of the natural transformation $\text{pushforwardToOfIso}\, H_1\, \alpha$ at $U$ is given by: \[ (\text{pushforwardToOfIso}\, H_1\, \alpha)_U = \alpha_{H_1^{-1}(U)} \circ \mathcal{G}(\text{id}_{H_1^{-1}(H_1(U))}) \] where $H_1^{-1}(U)$ denotes the preimage of $U$ under $H_1^{-1}$, and $\text{id}_{H_1^{-1}(H_1(U))}$ is the identity morphism on the open set $H_1^{-1}(H_1(U))$ in $X$.

TopCat.Presheaf.pullback definition

{X Y : TopCat.{v}} (f : X ⟶ Y) : Y.Presheaf C ⥤ X.Presheaf C

Full source

/-- Pullback a presheaf on `Y` along a continuous map `f : X ⟶ Y`, obtaining a presheaf
on `X`. -/
def pullback {X Y : TopCatTopCat.{v}} (f : X ⟶ Y) : Y.Presheaf C ⥤ X.Presheaf C :=
  (Opens.map f).op.lan

Pullback of a presheaf along a continuous map

Informal description

Given a continuous map $ f : X \to Y $ between topological spaces, the pullback functor $ \text{pullback}\, C\, f $ maps a $ C $-valued presheaf $ \mathcal{F} $ on $ Y $ to a presheaf on $ X $. This is constructed as the left Kan extension along the opposite of the preimage functor $ \text{Opens.map}\, f $, which sends open sets in $ Y $ to their preimages in $ X $.

TopCat.Presheaf.pushforwardPullbackAdjunction definition

{X Y : TopCat.{v}} (f : X ⟶ Y) : pullback C f ⊣ pushforward C f

Full source

/-- The pullback and pushforward along a continuous map are adjoint to each other. -/
def pushforwardPullbackAdjunction {X Y : TopCatTopCat.{v}} (f : X ⟶ Y) :
    pullbackpullback C f ⊣ pushforward C f :=
  Functor.lanAdjunction _ _

Adjunction between pullback and pushforward of presheaves

Informal description

Given topological spaces $ X $ and $ Y $ and a continuous map $ f \colon X \to Y $, the pullback functor $ \text{pullback}\, C\, f $ is left adjoint to the pushforward functor $ \text{pushforward}\, C\, f $. This adjunction means that for any $ C $-valued presheaf $ \mathcal{F} $ on $ Y $ and $ \mathcal{G} $ on $ X $, there is a natural bijection between morphisms $ \text{pullback}\, C\, f\, \mathcal{F} \to \mathcal{G} $ and morphisms $ \mathcal{F} \to \text{pushforward}\, C\, f\, \mathcal{G} $.

TopCat.Presheaf.pullbackHomIsoPushforwardInv definition

{X Y : TopCat.{v}} (H : X ≅ Y) : pullback C H.hom ≅ pushforward C H.inv

Full source

/-- Pulling back along a homeomorphism is the same as pushing forward along its inverse. -/
def pullbackHomIsoPushforwardInv {X Y : TopCatTopCat.{v}} (H : X ≅ Y) :
    pullbackpullback C H.hom ≅ pushforward C H.inv :=
  Adjunction.leftAdjointUniq (pushforwardPullbackAdjunction C H.hom)
    (presheafEquivOfIso C H.symm).toAdjunction

Isomorphism between pullback and pushforward via homeomorphism

Informal description

Given a homeomorphism $ H \colon X \cong Y $ between topological spaces $ X $ and $ Y $, the pullback functor along $ H $ is naturally isomorphic to the pushforward functor along the inverse homeomorphism $ H^{-1} $. In other words, there is a natural isomorphism \[ \text{pullback}\, C\, H \cong \text{pushforward}\, C\, H^{-1}. \]

TopCat.Presheaf.pullbackInvIsoPushforwardHom definition

{X Y : TopCat.{v}} (H : X ≅ Y) : pullback C H.inv ≅ pushforward C H.hom

Full source

/-- Pulling back along the inverse of a homeomorphism is the same as pushing forward along it. -/
def pullbackInvIsoPushforwardHom {X Y : TopCatTopCat.{v}} (H : X ≅ Y) :
    pullbackpullback C H.inv ≅ pushforward C H.hom :=
  Adjunction.leftAdjointUniq (pushforwardPullbackAdjunction C H.inv)
    (presheafEquivOfIso C H).toAdjunction

Isomorphism between pullback along inverse and pushforward along homeomorphism

Informal description

Given a homeomorphism $ H \colon X \cong Y $ between topological spaces $ X $ and $ Y $, the pullback functor along the inverse $ H^{-1} $ is naturally isomorphic to the pushforward functor along $ H $. In other words, there is a natural isomorphism \[ \text{pullback}\, C\, H^{-1} \cong \text{pushforward}\, C\, H. \]

TopCat.Presheaf.pullbackObjObjOfImageOpen definition

 {X Y : TopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf C) (U : Opens X) (H : IsOpen (f '' SetLike.coe U)) :
  ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op ⟨_, H⟩)

Full source

/-- If `f '' U` is open, then `f⁻¹ℱ U ≅ ℱ (f '' U)`. -/
def pullbackObjObjOfImageOpen {X Y : TopCatTopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf C) (U : Opens X)
    (H : IsOpen (f '' SetLike.coe U)) : ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op ⟨_, H⟩) := by
  let x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk
    (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op
  have hx : IsTerminal x :=
    { lift := fun s ↦ by
        fapply CostructuredArrow.homMk
        · change opop (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_subset f s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
        · simp [eq_iff_true_of_subsingleton] }
  exact IsColimit.coconePointUniqueUpToIso
    ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
    (colimitOfDiagramTerminal hx _)

Isomorphism between pullback presheaf and original presheaf on open image sets

Informal description

Given a continuous map $ f : X \to Y $ between topological spaces, a $ C $-valued presheaf $ \mathcal{F} $ on $ Y $, and an open subset $ U \subseteq X $ such that the image $ f(U) $ is open in $ Y $, there is a natural isomorphism \[ (f^* \mathcal{F})(U) \cong \mathcal{F}(f(U)), \] where $ f^* \mathcal{F} $ denotes the pullback presheaf of $ \mathcal{F} $ along $ f $.