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) : Subfunctor F

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

Equations

• CategoryTheory.Subfunctor.range p = { obj := fun (U : C) => Set.range ⇑(CategoryTheory.ConcreteCategory.hom (p.app U)), map := ⋯ }

@[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 ⇑(ConcreteCategory.hom (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) : range G.ι = G

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

• CategoryTheory.Subfunctor.lift f hf = { app := fun (U : C) => TypeCat.ofHom fun (x : F'.obj U) => ⟨(CategoryTheory.ConcreteCategory.hom (f.app U)) x, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subfunctor.lift_app {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) : (lift f hf).app U = TypeCat.ofHom fun (x : F'.obj U) => ⟨(ConcreteCategory.hom (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

• CategoryTheory.Subfunctor.toRange p = CategoryTheory.Subfunctor.lift p ⋯

@[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) : ↑((ConcreteCategory.hom ((toRange p).app i)) x) = (ConcreteCategory.hom (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] : range 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') : Subfunctor F'

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

Equations

• G.image f = { obj := fun (i : C) => ⇑(CategoryTheory.ConcreteCategory.hom (f.app i)) '' G.obj i, map := ⋯ }

@[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 = ⇑(ConcreteCategory.hom (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) : Subfunctor F'

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

Equations

• G.preimage p = { obj := fun (n : C) => ⇑(CategoryTheory.ConcreteCategory.hom (p.app n)) ⁻¹' G.obj n, map := ⋯ }

@[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 = ⇑(ConcreteCategory.hom (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

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

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