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 ⇑(CategoryTheory.ConcreteCategory.hom f))

@[instance_reducible]

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

Equations

• CategoryTheory.Limits.Types.instInhabitedImage f = { default := ⟨(CategoryTheory.ConcreteCategory.hom 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 = TypeCat.ofHom 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

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

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

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

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 ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))) : Function.Surjective ⇑(ConcreteCategory.hom ((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 ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))) : Function.Surjective ⇑(ConcreteCategory.hom (c.π.app (Opposite.op 0)))

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