Documentation

Mathlib.CategoryTheory.Subpresheaf.Image

The image of a subpresheaf #

Given a morphism of presheaves of types p : F' ⟶ F, we define its range Subpresheaf.range p. More generally, if G' : Subpresheaf F', we define G'.image p : Subpresheaf F as the image of G' by f, and if G : Subpresheaf F, we define its preimage G.preimage f : Subpresheaf F'.

def CategoryTheory.Subpresheaf.range {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

The range of a morphism of presheaves of types, as a subpresheaf of the target.

Equations

CategoryTheory.Subpresheaf.range p = { obj := fun (U : Cᵒᵖ) => Set.range (p.app U), map := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.range_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) (U : Cᵒᵖ) :

(range p).obj U = Set.range (p.app U)

theorem CategoryTheory.Subpresheaf.range_id {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) :

range (CategoryStruct.id F) = ⊤

@[simp]

theorem CategoryTheory.Subpresheaf.range_ι {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) :

def CategoryTheory.Subpresheaf.lift {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G) :

F' ⟶ G.toPresheaf

If the image of a morphism falls in a subpresheaf, then the morphism factors through it.

Equations

CategoryTheory.Subpresheaf.lift f hf = { app := fun (U : Cᵒᵖ) (x : F'.obj U) => ⟨f.app U x, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.lift_app_coe {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G) (U : Cᵒᵖ) (x : F'.obj U) :

↑((lift f hf).app U x) = f.app U x

@[simp]

theorem CategoryTheory.Subpresheaf.lift_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G) :

CategoryStruct.comp (lift f hf) G.ι = f

@[simp]

theorem CategoryTheory.Subpresheaf.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :

CategoryStruct.comp (lift f hf) (CategoryStruct.comp G.ι h) = CategoryStruct.comp f h

def CategoryTheory.Subpresheaf.toRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

F' ⟶ (range p).toPresheaf

Given a morphism p : F' ⟶ F of presheaves of types, this is the morphism from F' to its range.

Equations

CategoryTheory.Subpresheaf.toRange p = CategoryTheory.Subpresheaf.lift p ⋯

@[simp]

theorem CategoryTheory.Subpresheaf.toRange_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

CategoryStruct.comp (toRange p) (range p).ι = p

@[simp]

theorem CategoryTheory.Subpresheaf.toRange_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :

CategoryStruct.comp (toRange p) (CategoryStruct.comp (range p).ι h) = CategoryStruct.comp p h

theorem CategoryTheory.Subpresheaf.toRange_app_val {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) {i : Cᵒᵖ} (x : F'.obj i) :

↑((toRange p).app i x) = p.app i x

@[simp]

theorem CategoryTheory.Subpresheaf.range_toRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

range (toRange p) = ⊤

theorem CategoryTheory.Subpresheaf.epi_iff_range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

Epi p ↔ range p = ⊤

theorem CategoryTheory.Subpresheaf.range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) [Epi p] :

instance CategoryTheory.Subpresheaf.instEpiFunctorOppositeTypeToRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

Epi (toRange p)

instance CategoryTheory.Subpresheaf.instIsIsoFunctorOppositeTypeToRangeOfMono {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) [Mono p] :

IsIso (toRange p)

theorem CategoryTheory.Subpresheaf.range_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :

range (CategoryStruct.comp f g) ≤ range g

def CategoryTheory.Subpresheaf.image {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') :

The image of a subpresheaf by a morphism of presheaves of types.

Equations

G.image f = { obj := fun (i : Cᵒᵖ) => f.app i '' G.obj i, map := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.image_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') (i : Cᵒᵖ) :

(G.image f).obj i = f.app i '' G.obj i

theorem CategoryTheory.Subpresheaf.image_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') :

⊤.image f = range f

@[simp]

theorem CategoryTheory.Subpresheaf.image_iSup {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} {ι : Type u_1} (G : ι → Subpresheaf F) (f : F ⟶ F') :

(⨆ (i : ι), G i).image f = ⨆ (i : ι), (G i).image f

theorem CategoryTheory.Subpresheaf.image_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') (g : F' ⟶ F'') :

G.image (CategoryStruct.comp f g) = (G.image f).image g

theorem CategoryTheory.Subpresheaf.range_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :

range (CategoryStruct.comp f g) = (range f).image g

def CategoryTheory.Subpresheaf.preimage {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :

The preimage of a subpresheaf by a morphism of presheaves of types.

Equations

G.preimage p = { obj := fun (n : Cᵒᵖ) => p.app n ⁻¹' G.obj n, map := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.preimage_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) (n : Cᵒᵖ) :

(G.preimage p).obj n = p.app n ⁻¹' G.obj n

@[simp]

theorem CategoryTheory.Subpresheaf.preimage_id {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) :

G.preimage (CategoryStruct.id F) = G

theorem CategoryTheory.Subpresheaf.preimage_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F'' ⟶ F') (g : F' ⟶ F) :

G.preimage (CategoryStruct.comp f g) = (G.preimage g).preimage f

theorem CategoryTheory.Subpresheaf.image_le_iff {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') :

G.image f ≤ G' ↔ G ≤ G'.preimage f

def CategoryTheory.Subpresheaf.fromPreimage {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :

(G.preimage p).toPresheaf ⟶ G.toPresheaf

Given a morphism p : F' ⟶ F of presheaves of types and G : Subpresheaf F, this is the morphism from the preimage of G by p to G.

Equations

G.fromPreimage p = CategoryTheory.Subpresheaf.lift (CategoryTheory.CategoryStruct.comp (G.preimage p).ι p) ⋯

theorem CategoryTheory.Subpresheaf.fromPreimage_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :

CategoryStruct.comp (G.fromPreimage p) G.ι = CategoryStruct.comp (G.preimage p).ι p

theorem CategoryTheory.Subpresheaf.fromPreimage_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :

CategoryStruct.comp (G.fromPreimage p) (CategoryStruct.comp G.ι h) = CategoryStruct.comp (G.preimage p).ι (CategoryStruct.comp p h)

theorem CategoryTheory.Subpresheaf.preimage_eq_top_iff {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :

G.preimage p = ⊤ ↔ range p ≤ G

@[simp]

theorem CategoryTheory.Subpresheaf.preimage_image_of_epi {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) [hp : Epi p] :

(G.preimage p).image p = G

@[deprecated CategoryTheory.Subpresheaf.range (since := "2025-01-25")]

def CategoryTheory.imagePresheaf {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

Alias of CategoryTheory.Subpresheaf.range.

The range of a morphism of presheaves of types, as a subpresheaf of the target.

Equations

@CategoryTheory.imagePresheaf = @CategoryTheory.Subpresheaf.range

@[deprecated CategoryTheory.Subpresheaf.range_id (since := "2025-01-25")]

theorem CategoryTheory.imagePresheaf_id {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) :

Subpresheaf.range (CategoryStruct.id F) = ⊤

Alias of CategoryTheory.Subpresheaf.range_id.

@[deprecated CategoryTheory.Subpresheaf.toRange (since := "2025-01-25")]

def CategoryTheory.toImagePresheaf {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

F' ⟶ (Subpresheaf.range p).toPresheaf

Alias of CategoryTheory.Subpresheaf.toRange.

Given a morphism p : F' ⟶ F of presheaves of types, this is the morphism from F' to its range.

Equations

@CategoryTheory.toImagePresheaf = @CategoryTheory.Subpresheaf.toRange

@[deprecated CategoryTheory.Subpresheaf.toRange_ι (since := "2025-01-25")]

theorem CategoryTheory.toImagePresheaf_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :

CategoryStruct.comp (Subpresheaf.toRange p) (Subpresheaf.range p).ι = p

Alias of CategoryTheory.Subpresheaf.toRange_ι.

@[deprecated CategoryTheory.Subpresheaf.range_comp_le (since := "2025-01-25")]

theorem CategoryTheory.imagePresheaf_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :

Subpresheaf.range (CategoryStruct.comp f g) ≤ Subpresheaf.range g

Alias of CategoryTheory.Subpresheaf.range_comp_le.