Documentation

Mathlib.CategoryTheory.Subfunctor.Image

The image of a subfunctor #

Given a morphism of type-valued functors p : F' ⟶ F, we define its range Subfunctor.range p. More generally, if G' : Subfunctor F', we define G'.image p : Subfunctor F as the image of G' by f, and if G : Subfunctor F, we define its preimage G.preimage f : Subfunctor F'.

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

The range of a morphism of type-valued functors, as a subfunctor of the target.

Equations

Instances For

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.range_id {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) :

range (CategoryStruct.id F) = ⊤

@[simp]

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

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

F' ⟶ G.toFunctor

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

Equations

Instances For

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Subfunctor.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (f : F' ⟶ F) {G : Subfunctor 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.Subfunctor.toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :

F' ⟶ (range p).toFunctor

Given a morphism p : F' ⟶ F of type-valued functors, this is the morphism from F' to its range.

Equations

Instances For

@[simp]

theorem CategoryTheory.Subfunctor.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.Subfunctor.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.Subfunctor.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.Subfunctor.range_toRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :

range (toRange p) = ⊤

theorem CategoryTheory.Subfunctor.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.Subfunctor.range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) [Epi p] :

instance CategoryTheory.Subfunctor.instEpiFunctorTypeToRange {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) :

Epi (toRange p)

instance CategoryTheory.Subfunctor.instIsIsoFunctorTypeToRangeOfMono {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (p : F' ⟶ F) [Mono p] :

IsIso (toRange p)

theorem CategoryTheory.Subfunctor.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.Subfunctor.image {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F ⟶ F') :

The image of a subfunctor by a morphism of type-valued functors.

Equations

Instances For

@[simp]

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

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

theorem CategoryTheory.Subfunctor.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.Subfunctor.image_iSup {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} {ι : Type u_1} (G : ι → Subfunctor F) (f : F ⟶ F') :

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

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

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

theorem CategoryTheory.Subfunctor.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.Subfunctor.preimage {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :

The preimage of a subfunctor by a morphism of type-valued functors.

Equations

Instances For

@[simp]

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

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

@[simp]

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

G.preimage (CategoryStruct.id F) = G

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

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

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

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

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

(G.preimage p).toFunctor ⟶ G.toFunctor

Given a morphism p : F' ⟶ F of type-valued functors and G : Subfunctor F, this is the morphism from the preimage of G by p to G.

Equations

Instances For

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

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

theorem CategoryTheory.Subfunctor.fromPreimage_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor 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.Subfunctor.preimage_eq_top_iff {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (p : F' ⟶ F) :

G.preimage p = ⊤ ↔ range p ≤ G

@[simp]

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

(G.preimage p).image p = G

@[deprecated CategoryTheory.Subfunctor.range (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.range.

The range of a morphism of type-valued functors, as a subfunctor of the target.

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.range_id (since := "2025-12-11")]

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

Subfunctor.range (CategoryStruct.id F) = ⊤

Alias of CategoryTheory.Subfunctor.range_id.

@[deprecated CategoryTheory.Subfunctor.range_ι (since := "2025-12-11")]

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

Subfunctor.range G.ι = G

Alias of CategoryTheory.Subfunctor.range_ι.

@[deprecated CategoryTheory.Subfunctor.lift (since := "2025-12-11")]

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

F' ⟶ G.toFunctor

Alias of CategoryTheory.Subfunctor.lift.

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

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.lift_ι (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.lift_ι.

@[deprecated CategoryTheory.Subfunctor.toRange (since := "2025-12-11")]

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

F' ⟶ (Subfunctor.range p).toFunctor

Alias of CategoryTheory.Subfunctor.toRange.

Given a morphism p : F' ⟶ F of type-valued functors, this is the morphism from F' to its range.

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.toRange_ι (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.toRange_ι.

@[deprecated CategoryTheory.Subfunctor.toRange_app_val (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.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) :

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

Alias of CategoryTheory.Subfunctor.toRange_app_val.

@[deprecated CategoryTheory.Subfunctor.range_toRange (since := "2025-12-11")]

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

Subfunctor.range (Subfunctor.toRange p) = ⊤

Alias of CategoryTheory.Subfunctor.range_toRange.

@[deprecated CategoryTheory.Subfunctor.epi_iff_range_eq_top (since := "2025-12-11")]

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

Epi p ↔ Subfunctor.range p = ⊤

Alias of CategoryTheory.Subfunctor.epi_iff_range_eq_top.

@[deprecated CategoryTheory.Subfunctor.range_eq_top (since := "2025-12-11")]

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

Subfunctor.range p = ⊤

Alias of CategoryTheory.Subfunctor.range_eq_top.

@[deprecated CategoryTheory.Subfunctor.range_comp_le (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.range_comp_le.

@[deprecated CategoryTheory.Subfunctor.image (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.image.

The image of a subfunctor by a morphism of type-valued functors.

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.image_top (since := "2025-12-11")]

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

⊤.image f = Subfunctor.range f

Alias of CategoryTheory.Subfunctor.image_top.

@[deprecated CategoryTheory.Subfunctor.image_iSup (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.image_iSup.

@[deprecated CategoryTheory.Subfunctor.image_comp (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.image_comp.

@[deprecated CategoryTheory.Subfunctor.range_comp (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.range_comp.

@[deprecated CategoryTheory.Subfunctor.preimage (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.preimage.

The preimage of a subfunctor by a morphism of type-valued functors.

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.preimage_id (since := "2025-12-11")]

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

G.preimage (CategoryStruct.id F) = G

Alias of CategoryTheory.Subfunctor.preimage_id.

@[deprecated CategoryTheory.Subfunctor.preimage_comp (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.preimage_comp.

@[deprecated CategoryTheory.Subfunctor.image_le_iff (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.image_le_iff.

@[deprecated CategoryTheory.Subfunctor.fromPreimage (since := "2025-12-11")]

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

(G.preimage p).toFunctor ⟶ G.toFunctor

Alias of CategoryTheory.Subfunctor.fromPreimage.

Given a morphism p : F' ⟶ F of type-valued functors and G : Subfunctor F, this is the morphism from the preimage of G by p to G.

Equations

Instances For

@[deprecated CategoryTheory.Subfunctor.fromPreimage_ι (since := "2025-12-11")]

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

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

Alias of CategoryTheory.Subfunctor.fromPreimage_ι.

@[deprecated CategoryTheory.Subfunctor.preimage_eq_top_iff (since := "2025-12-11")]

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

G.preimage p = ⊤ ↔ Subfunctor.range p ≤ G

Alias of CategoryTheory.Subfunctor.preimage_eq_top_iff.

@[deprecated CategoryTheory.Subfunctor.preimage_image_of_epi (since := "2025-12-11")]

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

(G.preimage p).image p = G

Alias of CategoryTheory.Subfunctor.preimage_image_of_epi.