Images in the category of types

In this file, it is shown that the category of types has categorical images, and that these agree with the range of a function.

def CategoryTheory.Limits.Types.Image {α β : Type u} (f : α ⟶ β) : Type u

the image of a morphism in Type is just Set.range f

Equations

• CategoryTheory.Limits.Types.Image f = ↑(Set.range f)

instance CategoryTheory.Limits.Types.instInhabitedImage {α β : Type u} (f : α ⟶ β) [Inhabited α] : Inhabited (Image f)

Equations

• CategoryTheory.Limits.Types.instInhabitedImage f = { default := ⟨f default, ⋯⟩ }

def CategoryTheory.Limits.Types.Image.ι {α β : Type u} (f : α ⟶ β) : Image f ⟶ β

the inclusion of Image f into the target

Equations

• CategoryTheory.Limits.Types.Image.ι f = Subtype.val

instance CategoryTheory.Limits.Types.instMonoImageι {α β : Type u} (f : α ⟶ β) : Mono (Image.ι f)

noncomputable def CategoryTheory.Limits.Types.Image.lift {α β : Type u} {f : α ⟶ β} (F' : MonoFactorisation f) : Image f ⟶ F'.I

the universal property for the image factorisation

Equations

• CategoryTheory.Limits.Types.Image.lift F' x = F'.e ↑(Classical.indefiniteDescription (fun (x_1 : α) => f x_1 = ↑x) ⋯)

theorem CategoryTheory.Limits.Types.Image.lift_fac {α β : Type u} {f : α ⟶ β} (F' : MonoFactorisation f) : CategoryStruct.comp (lift F') F'.m = ι f

def CategoryTheory.Limits.Types.monoFactorisation {α β : Type u} (f : α ⟶ β) : MonoFactorisation f

the factorisation of any morphism in Type through a mono.

Equations

• CategoryTheory.Limits.Types.monoFactorisation f = { I := CategoryTheory.Limits.Types.Image f, m := CategoryTheory.Limits.Types.Image.ι f, m_mono := ⋯, e := Set.rangeFactorization f, fac := ⋯ }

noncomputable def CategoryTheory.Limits.Types.isImage {α β : Type u} (f : α ⟶ β) : IsImage (monoFactorisation f)

the factorisation through a mono has the universal property of the image.

Equations

• CategoryTheory.Limits.Types.isImage f = { lift := CategoryTheory.Limits.Types.Image.lift, lift_fac := ⋯ }

instance CategoryTheory.Limits.Types.instHasImage {α β : Type u} (f : α ⟶ β) : HasImage f

instance CategoryTheory.Limits.Types.instHasImagesType : HasImages (Type u)

instance CategoryTheory.Limits.Types.instHasImageMapsType : HasImageMaps (Type u)

theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux {F : Functor ℕᵒᵖ (Type u)} (hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)) : Function.Surjective ((limitCone F).π.app (Opposite.op 0))

Auxiliary lemma. Use limit_of_surjections_surjective instead.

theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map {F : Functor ℕᵒᵖ (Type u)} {c : Cone F} (hc : IsLimit c) (hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)) : Function.Surjective (c.π.app (Opposite.op 0))

Given surjections ⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀, the projection map lim Xₙ ⟶ X₀ is surjective.