Presheaves on a topological space #

We define TopCat.Presheaf C X simply as (TopologicalSpace.Opens X)ᵒᵖ ⥤ C, and inherit the category structure with natural transformations as morphisms.

We define

TopCat.Presheaf.pushforwardObj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : X.Presheaf C) : Y.Presheaf C with notation f _* ℱ and for ℱ : X.Presheaf C provide the natural isomorphisms
TopCat.Presheaf.Pushforward.id : (𝟙 X) _* ℱ ≅ ℱ
TopCat.Presheaf.Pushforward.comp : (f ≫ g) _* ℱ ≅ g _* (f _* ℱ) along with their @[simp] lemmas.

We also define the functors pushforward and pullback between the categories X.Presheaf C and Y.Presheaf C, and provide their adjunction at TopCat.Presheaf.pushforwardPullbackAdjunction.

source

def TopCat.Presheaf (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) :

Type (max u v w)

The category of C-valued presheaves on a (bundled) topological space X.

Equations

TopCat.Presheaf C X = CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C

Instances For

source

instance TopCat.instCategoryPresheaf (C : Type u) [CategoryTheory.Category.{v, u} C] (X : TopCat) :

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

Equations

TopCat.instCategoryPresheaf C X = inferInstanceAs (CategoryTheory.Category.{max v w, max (max u v) w} (CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C))

source

@[simp]

theorem TopCat.Presheaf.comp_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {P : TopCat.Presheaf C X} {Q : TopCat.Presheaf C X} {R : TopCat.Presheaf C X} (f : P ⟶ Q) (g : Q ⟶ R) :

(CategoryTheory.CategoryStruct.comp f g).app U = CategoryTheory.CategoryStruct.comp (f.app U) (g.app U)

source

theorem TopCat.Presheaf.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {P : TopCat.Presheaf C X} {Q : TopCat.Presheaf C X} {f : P ⟶ Q} {g : P ⟶ Q} (w : ∀ (U : TopologicalSpace.Opens ↑X), f.app (Opposite.op U) = g.app (Opposite.op U)) :

f = g

source

def TopCat.Presheaf.attrSheaf_restrict :

Lean.ParserDescr

attribute sheaf_restrict to mark lemmas related to restricting sheaves

Equations

TopCat.Presheaf.attrSheaf_restrict = Lean.ParserDescr.node `TopCat.Presheaf.attrSheaf_restrict 1024 (Lean.ParserDescr.nonReservedSymbol "sheaf_restrict" false)

Instances For

source

def TopCat.Presheaf.restrict_tac :

Lean.ParserDescr

restrict_tac solves relations among subsets (copied from aesop cat)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TopCat.Presheaf.restrict_tac? :

Lean.ParserDescr

restrict_tac? passes along Try this from aesop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TopCat.Presheaf.restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op V))) {U : TopologicalSpace.Opens ↑X} (h : U ⟶ V) :

(CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op U))

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.

Equations

TopCat.Presheaf.restrict x h = (F.toPrefunctor.map h.op) x

Instances For

source

def AlgebraicGeometry.«term_|_ₕ_» :

Lean.TrailingParserDescr

restriction of a section along an inclusion

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AlgebraicGeometry.«term_|_ₗ_⟪_⟫» :

Lean.TrailingParserDescr

restriction of a section along a subset relation

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[inline, reducible]

abbrev TopCat.Presheaf.restrictOpen {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {V : TopologicalSpace.Opens ↑X} (x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op V))) (U : TopologicalSpace.Opens ↑X) (e : autoParam (U ≤ V) _auto✝) :

(CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op U))

The restriction of a section along an inclusion of open sets. For x : F.obj (op V), we provide the notation x |_ U, where the proof U ≤ V is inferred by the tactic Top.presheaf.restrict_tac'

Equations

TopCat.Presheaf.restrictOpen x U = TopCat.Presheaf.restrict x (CategoryTheory.homOfLE e)

Instances For

source

def AlgebraicGeometry.«term_|__» :

Lean.TrailingParserDescr

restriction of a section to open subset

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem TopCat.Presheaf.restrict_restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} {W : TopologicalSpace.Opens ↑X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op W))) :

TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen x V) U = TopCat.Presheaf.restrictOpen x U

source

theorem TopCat.Presheaf.map_restrict {X : TopCat} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] {F : TopCat.Presheaf C X} {G : TopCat.Presheaf C X} (e : F ⟶ G) {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} (h : U ≤ V) (x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op V))) :

(e.app (Opposite.op U)) (TopCat.Presheaf.restrictOpen x U) = TopCat.Presheaf.restrictOpen ((e.app (Opposite.op V)) x) U

source

def TopCat.Presheaf.pushforwardObj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) :

TopCat.Presheaf C Y

Pushforward a presheaf on X along a continuous map f : X ⟶ Y, obtaining a presheaf on Y.

Equations

f _* ℱ = CategoryTheory.Functor.comp (TopologicalSpace.Opens.map f).op ℱ

Instances For

source

def TopCat.Presheaf.«term__*_» :

Lean.TrailingParserDescr

push forward of a presheaf

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TopCat.Presheaf.pushforwardObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

(f _* ℱ).toPrefunctor.obj U = ℱ.toPrefunctor.obj ((TopologicalSpace.Opens.map f).op.toPrefunctor.obj U)

source

@[simp]

theorem TopCat.Presheaf.pushforwardObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ} {V : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (i : U ⟶ V) :

(f _* ℱ).toPrefunctor.map i = ℱ.toPrefunctor.map ((TopologicalSpace.Opens.map f).op.toPrefunctor.map i)

source

def TopCat.Presheaf.pushforwardEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) :

f _* ℱ ≅ g _* ℱ

An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf along those maps.

Equations

TopCat.Presheaf.pushforwardEq h ℱ = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapIso f g h).symm) ℱ

Instances For

source

theorem TopCat.Presheaf.pushforward_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) :

f _* ℱ = g _* ℱ

source

@[simp]

theorem TopCat.Presheaf.pushforwardEq_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

(TopCat.Presheaf.pushforwardEq h ℱ).hom.app U = ℱ.toPrefunctor.map (id (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map g).toPrefunctor.obj U.unop = (TopologicalSpace.Opens.map f).toPrefunctor.obj U.unop)).op)

source

theorem TopCat.Presheaf.pushforward_eq'_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

(CategoryTheory.eqToHom (_ : f _* ℱ = g _* ℱ)).app U = ℱ.toPrefunctor.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map f).op.toPrefunctor.obj U = (TopologicalSpace.Opens.map g).op.toPrefunctor.obj U))

source

@[simp]

theorem TopCat.Presheaf.pushforwardEq_rfl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑Y) :

(TopCat.Presheaf.pushforwardEq (_ : f = f) ℱ).hom.app (Opposite.op U) = CategoryTheory.CategoryStruct.id ((f _* ℱ).toPrefunctor.obj (Opposite.op U))

source

theorem TopCat.Presheaf.pushforwardEq_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} {f : X ⟶ Y} {g : X ⟶ Y} (h₁ : f = g) (h₂ : f = g) (ℱ : TopCat.Presheaf C X) :

TopCat.Presheaf.pushforwardEq h₁ ℱ = TopCat.Presheaf.pushforwardEq h₂ ℱ

source

def TopCat.Presheaf.Pushforward.id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) :

CategoryTheory.CategoryStruct.id X _* ℱ ≅ ℱ

The natural isomorphism between the pushforward of a presheaf along the identity continuous map and the original presheaf.

Equations

TopCat.Presheaf.Pushforward.id ℱ = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapId X).symm) ℱ ≪≫ CategoryTheory.Functor.leftUnitor ℱ

Instances For

source

theorem TopCat.Presheaf.Pushforward.id_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) :

CategoryTheory.CategoryStruct.id X _* ℱ = ℱ

source

@[simp]

theorem TopCat.Presheaf.Pushforward.id_hom_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set ↑X) (p : IsOpen U) :

(TopCat.Presheaf.Pushforward.id ℱ).hom.app (Opposite.op { carrier := U, is_open' := p }) = ℱ.toPrefunctor.map (CategoryTheory.CategoryStruct.id (Opposite.op { carrier := U, is_open' := p }))

source

@[simp]

theorem TopCat.Presheaf.Pushforward.id_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :

(TopCat.Presheaf.Pushforward.id ℱ).hom.app U = ℱ.toPrefunctor.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).op.toPrefunctor.obj U = U))

source

@[simp]

theorem TopCat.Presheaf.Pushforward.id_inv_app' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) (U : Set ↑X) (p : IsOpen U) :

(TopCat.Presheaf.Pushforward.id ℱ).inv.app (Opposite.op { carrier := U, is_open' := p }) = ℱ.toPrefunctor.map (CategoryTheory.CategoryStruct.id (Opposite.op { carrier := U, is_open' := p }))

source

def TopCat.Presheaf.Pushforward.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp f g _* ℱ ≅ g _* (f _* ℱ)

The natural isomorphism between the pushforward of a presheaf along the composition of two continuous maps and the corresponding pushforward of a pushforward.

Equations

TopCat.Presheaf.Pushforward.comp ℱ f g = CategoryTheory.isoWhiskerRight (CategoryTheory.NatIso.op (TopologicalSpace.Opens.mapComp f g).symm) ℱ

Instances For

source

theorem TopCat.Presheaf.Pushforward.comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp f g _* ℱ = g _* (f _* ℱ)

source

@[simp]

theorem TopCat.Presheaf.Pushforward.comp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ) :

(TopCat.Presheaf.Pushforward.comp ℱ f g).hom.app U = CategoryTheory.CategoryStruct.id ((CategoryTheory.CategoryStruct.comp f g _* ℱ).toPrefunctor.obj U)

source

@[simp]

theorem TopCat.Presheaf.Pushforward.comp_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (ℱ : TopCat.Presheaf C X) {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ) :

(TopCat.Presheaf.Pushforward.comp ℱ f g).inv.app U = CategoryTheory.CategoryStruct.id ((g _* (f _* ℱ)).toPrefunctor.obj U)

source

@[simp]

theorem TopCat.Presheaf.pushforwardMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

(TopCat.Presheaf.pushforwardMap f α).app U = α.app ((TopologicalSpace.Opens.map f).op.toPrefunctor.obj U)

source

def TopCat.Presheaf.pushforwardMap {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) :

f _* ℱ ⟶ f _* 𝒢

A morphism of presheaves gives rise to a morphisms of the pushforwards of those presheaves.

Equations

TopCat.Presheaf.pushforwardMap f α = CategoryTheory.NatTrans.mk fun (U : (TopologicalSpace.Opens ↑Y)ᵒᵖ) => α.app ((TopologicalSpace.Opens.map f).op.toPrefunctor.obj U)

Instances For

source

@[simp]

theorem TopCat.Presheaf.pullbackObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) {x : (TopologicalSpace.Opens ↑X)ᵒᵖ} {y : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : x ⟶ y) :

(TopCat.Presheaf.pullbackObj f✝ ℱ).toPrefunctor.map f = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f✝).op ℱ y) (CategoryTheory.CostructuredArrow.map f)

source

@[simp]

theorem TopCat.Presheaf.pullbackObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (x : (TopologicalSpace.Opens ↑X)ᵒᵖ) :

(TopCat.Presheaf.pullbackObj f ℱ).toPrefunctor.obj x = CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ x)

source

def TopCat.Presheaf.pullbackObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) :

TopCat.Presheaf C X

Pullback a presheaf on Y along a continuous map f : X ⟶ Y, obtaining a presheaf on X.

This is defined in terms of left Kan extensions, which is just a fancy way of saying "take the colimits over the open sets whose preimage contains U".

Equations

TopCat.Presheaf.pullbackObj f ℱ = (CategoryTheory.lan (TopologicalSpace.Opens.map f).op).toPrefunctor.obj ℱ

Instances For

source

def TopCat.Presheaf.pullbackMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C Y} (α : ℱ ⟶ 𝒢) :

TopCat.Presheaf.pullbackObj f ℱ ⟶ TopCat.Presheaf.pullbackObj f 𝒢

Pulling back along continuous maps is functorial.

Equations

TopCat.Presheaf.pullbackMap f α = (CategoryTheory.lan (TopologicalSpace.Opens.map f).op).toPrefunctor.map α

Instances For

source

@[simp]

theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) :

(TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ U H).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ (Opposite.op U)) (CategoryTheory.Limits.coconeOfDiagramTerminal (CategoryTheory.Limits.IsLimit.mk fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty (CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op (Opposite.op U)))) => CategoryTheory.CostructuredArrow.homMk (CategoryTheory.homOfLE (_ : ⇑f '' ↑((CategoryTheory.Functor.fromPUnit (Opposite.op U)).toPrefunctor.obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op) (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ (Opposite.op U)))

source

@[simp]

theorem TopCat.Presheaf.pullbackObjObjOfImageOpen_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) :

(TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ U H).inv = (CategoryTheory.Limits.colimitOfDiagramTerminal (CategoryTheory.Limits.IsLimit.mk fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty (CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op (Opposite.op U)))) => CategoryTheory.CostructuredArrow.homMk (CategoryTheory.homOfLE (_ : ⇑f '' ↑((CategoryTheory.Functor.fromPUnit (Opposite.op U)).toPrefunctor.obj s.pt.right).unop ⊆ ↑s.pt.1.unop)).op) (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ (Opposite.op U))).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map f).op ℱ (Opposite.op U)))

source

def TopCat.Presheaf.pullbackObjObjOfImageOpen {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑X) (H : IsOpen (⇑f '' ↑U)) :

(TopCat.Presheaf.pullbackObj f ℱ).toPrefunctor.obj (Opposite.op U) ≅ ℱ.toPrefunctor.obj (Opposite.op { carrier := ⇑f '' ↑U, is_open' := H })

If f '' U is open, then f⁻¹ℱ U ≅ ℱ (f '' U).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def TopCat.Presheaf.Pullback.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {Y : TopCat} (ℱ : TopCat.Presheaf C Y) :

TopCat.Presheaf.pullbackObj (CategoryTheory.CategoryStruct.id Y) ℱ ≅ ℱ

The pullback along the identity is isomorphic to the original presheaf.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem TopCat.Presheaf.Pullback.id_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {Y : TopCat} (ℱ : TopCat.Presheaf C Y) (U : TopologicalSpace.Opens ↑Y) :

(TopCat.Presheaf.Pullback.id ℱ).inv.app (Opposite.op U) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Lan.diagram (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id Y)).op ℱ (Opposite.op U)) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id Y)).op.toPrefunctor.obj (Opposite.op U) = Opposite.op U)))

source

def TopCat.Presheaf.pushforward (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) :

CategoryTheory.Functor (TopCat.Presheaf C X) (TopCat.Presheaf C Y)

The pushforward functor.

Equations

TopCat.Presheaf.pushforward C f = CategoryTheory.Functor.mk { obj := TopCat.Presheaf.pushforwardObj f, map := @TopCat.Presheaf.pushforwardMap C inst X Y f }

Instances For

source

@[simp]

theorem TopCat.Presheaf.pushforward_map_app' (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (f : X ⟶ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C X} (α : ℱ ⟶ 𝒢) {U : (TopologicalSpace.Opens ↑Y)ᵒᵖ} :

((TopCat.Presheaf.pushforward C f).toPrefunctor.map α).app U = α.app (Opposite.op ((TopologicalSpace.Opens.map f).toPrefunctor.obj U.unop))

source

theorem TopCat.Presheaf.id_pushforward (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} :

TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (TopCat.Presheaf C X)

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝ ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).inverse.toPrefunctor.obj G).toPrefunctor.obj X = G.toPrefunctor.obj (Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X.unop))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.hom.app X✝).app X = X✝.toPrefunctor.map (CategoryTheory.eqToHom (_ : Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj X.unop)) = Opposite.op X.unop))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝ ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).functor.toPrefunctor.obj G).toPrefunctor.obj X = G.toPrefunctor.obj (Opposite.op ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj X.unop))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).unit.app X)) (CategoryTheory.CategoryStruct.comp (X✝.toPrefunctor.map ((TopologicalSpace.Opens.map H.hom).toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).counitInv.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X.unop))).unop).op) (X✝.toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).unitInv.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X.unop))))))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑Y)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.inv.app X✝).app X = X✝.toPrefunctor.map (CategoryTheory.eqToHom (_ : Opposite.op X.unop = Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj X.unop))))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) :

∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.toPrefunctor.map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X_2.unop))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) :

∀ {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X_1 ⟶ Y_1) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.toPrefunctor.map α).app X_2 = α.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj X_2.unop))

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) :

∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).functor.toPrefunctor.obj G).toPrefunctor.map f = G.toPrefunctor.map ((TopologicalSpace.Opens.map H.hom).toPrefunctor.map f.unop).op

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) :

∀ {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ} (f : X_1 ⟶ Y_1), ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.toPrefunctor.obj G).toPrefunctor.map f = G.toPrefunctor.map ((TopologicalSpace.Opens.map H.inv).toPrefunctor.map f.unop).op

source

@[simp]

theorem TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X✝¹ ≅ Y) (X : CategoryTheory.Functor (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ C) (X : (TopologicalSpace.Opens ↑X✝¹)ᵒᵖ) :

((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.comp (X✝.toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).unit.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).toPrefunctor.obj ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X.unop))))) (CategoryTheory.CategoryStruct.comp (X✝.toPrefunctor.map ((TopologicalSpace.Opens.map H.hom).toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).counit.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).toPrefunctor.obj X.unop))).unop).op) (X✝.toPrefunctor.map ((CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm).unitInv.app X)))

source

def TopCat.Presheaf.presheafEquivOfIso (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) :

TopCat.Presheaf C X ≌ TopCat.Presheaf C Y

A homeomorphism of spaces gives an equivalence of categories of presheaves.

Equations

TopCat.Presheaf.presheafEquivOfIso C H = CategoryTheory.Equivalence.congrLeft (CategoryTheory.Equivalence.op (TopologicalSpace.Opens.mapMapIso H).symm)

Instances For

source

def TopCat.Presheaf.toPushforwardOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H : X ≅ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (α : H.hom _* ℱ ⟶ 𝒢) :

ℱ ⟶ H.inv _* 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations

TopCat.Presheaf.toPushforwardOfIso H α = ((TopCat.Presheaf.presheafEquivOfIso C H).toAdjunction.homEquiv ℱ 𝒢) α

Instances For

source

@[simp]

theorem TopCat.Presheaf.toPushforwardOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C X} {𝒢 : TopCat.Presheaf C Y} (H₂ : H₁.hom _* ℱ ⟶ 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :

(TopCat.Presheaf.toPushforwardOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (ℱ.toPrefunctor.map (CategoryTheory.eqToHom (_ : U = Opposite.op { carrier := ⇑H₁.hom ⁻¹' ↑(Opposite.op { carrier := ⇑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (⇑H₁.inv ⁻¹' ↑U.unop)) }).unop, is_open' := (_ : IsOpen (⇑H₁.hom ⁻¹' ↑(Opposite.op { carrier := ⇑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (⇑H₁.inv ⁻¹' ↑U.unop)) }).unop)) }))) (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).toPrefunctor.obj U.unop)))

source

def TopCat.Presheaf.pushforwardToOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) :

H₁.inv _* ℱ ⟶ 𝒢

If H : X ≅ Y is a homeomorphism, then given an H _* ℱ ⟶ 𝒢, we may obtain an ℱ ⟶ H ⁻¹ _* 𝒢.

Equations

TopCat.Presheaf.pushforwardToOfIso H₁ H₂ = ((TopCat.Presheaf.presheafEquivOfIso C H₁.symm).toAdjunction.homEquiv ℱ 𝒢).symm H₂

Instances For

source

@[simp]

theorem TopCat.Presheaf.pushforwardToOfIso_app {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {Y : TopCat} (H₁ : X ≅ Y) {ℱ : TopCat.Presheaf C Y} {𝒢 : TopCat.Presheaf C X} (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :

(TopCat.Presheaf.pushforwardToOfIso H₁ H₂).app U = CategoryTheory.CategoryStruct.comp (H₂.app (Opposite.op ((TopologicalSpace.Opens.map H₁.inv).toPrefunctor.obj U.unop))) (𝒢.toPrefunctor.map (CategoryTheory.eqToHom (_ : Opposite.op { carrier := ⇑H₁.hom ⁻¹' ↑(Opposite.op { carrier := ⇑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (⇑H₁.inv ⁻¹' ↑U.unop)) }).unop, is_open' := (_ : IsOpen (⇑H₁.hom ⁻¹' ↑(Opposite.op { carrier := ⇑H₁.inv ⁻¹' ↑U.unop, is_open' := (_ : IsOpen (⇑H₁.inv ⁻¹' ↑U.unop)) }).unop)) } = U)))

source

@[simp]