Limits in concrete categories

In this file, we combine the description of limits in Types and the API about the preservation of products and pullbacks in order to describe these limits in a concrete category C.

If F : J → C is a family of objects in C, we define a bijection Limits.Concrete.productEquiv F : ToType (∏ᶜ F) ≃ ∀ j, ToType (F j).

Similarly, if f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S are two morphisms, the elements in pullback f₁ f₂ are identified by Limits.Concrete.pullbackEquiv to compatible tuples of elements in X₁ × X₂.

Some results are also obtained for the terminal object, binary products, wide-pullbacks, wide-pushouts, multiequalizers and cokernels.

noncomputable def CategoryTheory.Limits.Concrete.productEquiv {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : Type w} (F : J → C) [HasProduct F] [PreservesLimit (Discrete.functor F) (forget C)] : ToType (∏ᶜ F) ≃ ((j : J) → ToType (F j))

The equivalence ToType (∏ᶜ F) ≃ ∀ j, ToType (F j) if F : J → C is a family of objects in a concrete category C.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Concrete.productEquiv_apply_apply {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : Type w} (F : J → C) [HasProduct F] [PreservesLimit (Discrete.functor F) (forget C)] (x : ToType (∏ᶜ F)) (j : J) : (productEquiv F) x j = (ConcreteCategory.hom (Pi.π F j)) x

@[simp]

theorem CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : Type w} (F : J → C) [HasProduct F] [PreservesLimit (Discrete.functor F) (forget C)] (x : (j : J) → ToType (F j)) (j : J) : (ConcreteCategory.hom (Pi.π F j)) ((productEquiv F).symm x) = x j

theorem CategoryTheory.Limits.Concrete.Pi.map_ext {C : Type u} [Category.{v, u} C] {J : Type w} (f : J → C) [HasProduct f] {D : Type t} [Category.{r, t} D] {FD : D → D → Type u_1} {DD : D → Type (max w r)} [(X Y : D) → FunLike (FD X Y) (DD X) (DD Y)] [ConcreteCategory D FD] (F : Functor C D) [PreservesLimit (Discrete.functor f) F] [HasProduct fun (j : J) => F.obj (f j)] [PreservesLimitsOfShape WalkingCospan (forget D)] [PreservesLimit (Discrete.functor fun (b : J) => F.obj (f b)) (forget D)] (x y : ToType (F.obj (∏ᶜ f))) (h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y) : x = y

noncomputable def CategoryTheory.Limits.Concrete.uniqueOfTerminalOfPreserves {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [PreservesLimit (Functor.empty C) (forget C)] (X : C) (h : IsTerminal X) : Unique (ToType X)

If forget C preserves terminals and X is terminal, then ToType X is a singleton.

Equations

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

noncomputable def CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [ReflectsLimit (Functor.empty C) (forget C)] (X : C) (h : Unique (ToType X)) : IsTerminal X

If forget C reflects terminals and ToType X is a singleton, then X is terminal.

Equations

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

noncomputable def CategoryTheory.Limits.Concrete.terminalIffUnique {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [PreservesLimit (Functor.empty C) (forget C)] [ReflectsLimit (Functor.empty C) (forget C)] (X : C) : IsTerminal X ≃ Unique (ToType X)

The equivalence IsTerminal X ≃ Unique (ToType X) if the forgetful functor preserves and reflects terminals.

Equations

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

noncomputable def CategoryTheory.Limits.Concrete.terminalEquiv (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasTerminal C] [PreservesLimit (Functor.empty C) (forget C)] : ToType (⊤_ C) ≃ PUnit.{w + 1}

The equivalence ToType (⊤_ C) ≃ PUnit when C is a concrete category.

Equations

• CategoryTheory.Limits.Concrete.terminalEquiv C = (CategoryTheory.Limits.PreservesTerminal.iso (CategoryTheory.forget C) ≪≫ CategoryTheory.Limits.Types.terminalIso).toEquiv

noncomputable instance CategoryTheory.Limits.Concrete.instUniqueToTypeTerminal (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasTerminal C] [PreservesLimit (Functor.empty C) (forget C)] : Unique (ToType (⊤_ C))

Equations

• CategoryTheory.Limits.Concrete.instUniqueToTypeTerminal C = { default := (CategoryTheory.Limits.Concrete.terminalEquiv C).symm PUnit.unit, uniq := ⋯ }

theorem CategoryTheory.Limits.Concrete.empty_of_initial_of_preserves {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [PreservesColimit (Functor.empty C) (forget C)] (X : C) (h : Nonempty (IsInitial X)) : IsEmpty (ToType X)

If forget C preserves initials and X is initial, then ToType X is empty.

theorem CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [ReflectsColimit (Functor.empty C) (forget C)] (X : C) (h : IsEmpty (ToType X)) : Nonempty (IsInitial X)

If forget C reflects initials and ToType X is empty, then X is initial.

theorem CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [PreservesColimit (Functor.empty C) (forget C)] [ReflectsColimit (Functor.empty C) (forget C)] (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

If forget C preserves and reflects initials, then X is initial if and only if ToType X is empty.

noncomputable def CategoryTheory.Limits.Concrete.prodEquiv {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X₁ X₂ : C) [HasBinaryProduct X₁ X₂] [PreservesLimit (pair X₁ X₂) (forget C)] : ToType (X₁ ⨯ X₂) ≃ ToType X₁ × ToType X₂

The equivalence ToType (X₁ ⨯ X₂) ≃ (ToType X₁) × (ToType X₂) if X₁ and X₂ are objects in a concrete category C.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_fst {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X₁ X₂ : C) [HasBinaryProduct X₁ X₂] [PreservesLimit (pair X₁ X₂) (forget C)] (x : ToType (X₁ ⨯ X₂)) : ((prodEquiv X₁ X₂) x).1 = (ConcreteCategory.hom prod.fst) x

@[simp]

theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_snd {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X₁ X₂ : C) [HasBinaryProduct X₁ X₂] [PreservesLimit (pair X₁ X₂) (forget C)] (x : ToType (X₁ ⨯ X₂)) : ((prodEquiv X₁ X₂) x).2 = (ConcreteCategory.hom prod.snd) x

@[simp]

theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X₁ X₂ : C) [HasBinaryProduct X₁ X₂] [PreservesLimit (pair X₁ X₂) (forget C)] (x : ToType X₁ × ToType X₂) : (ConcreteCategory.hom prod.fst) ((prodEquiv X₁ X₂).symm x) = x.1

@[simp]

theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] (X₁ X₂ : C) [HasBinaryProduct X₁ X₂] [PreservesLimit (pair X₁ X₂) (forget C)] (x : ToType X₁ × ToType X₂) : (ConcreteCategory.hom prod.snd) ((prodEquiv X₁ X₂).symm x) = x.2

noncomputable def CategoryTheory.Limits.Concrete.pullbackEquiv {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [HasPullback f₁ f₂] [PreservesLimit (cospan f₁ f₂) (forget C)] : ToType (pullback f₁ f₂) ≃ { p : ToType X₁ × ToType X₂ // (ConcreteCategory.hom f₁) p.1 = (ConcreteCategory.hom f₂) p.2 }

In a concrete category C, given two morphisms f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S, the elements in pullback f₁ f₁ can be identified to compatible tuples of elements in X₁ and X₂.

Equations

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

noncomputable def CategoryTheory.Limits.Concrete.pullbackMk {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [HasPullback f₁ f₂] [PreservesLimit (cospan f₁ f₂) (forget C)] (x₁ : ToType X₁) (x₂ : ToType X₂) (h : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂) : ToType (pullback f₁ f₂)

Constructor for elements in a pullback in a concrete category.

Equations

• CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h = (CategoryTheory.Limits.Concrete.pullbackEquiv f₁ f₂).symm ⟨(x₁, x₂), h⟩

theorem CategoryTheory.Limits.Concrete.pullbackMk_surjective {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [HasPullback f₁ f₂] [PreservesLimit (cospan f₁ f₂) (forget C)] (x : ToType (pullback f₁ f₂)) : ∃ (x₁ : ToType X₁) (x₂ : ToType X₂) (h : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂), x = pullbackMk f₁ f₂ x₁ x₂ h

@[simp]

theorem CategoryTheory.Limits.Concrete.pullbackMk_fst {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [HasPullback f₁ f₂] [PreservesLimit (cospan f₁ f₂) (forget C)] (x₁ : ToType X₁) (x₂ : ToType X₂) (h : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂) : (ConcreteCategory.hom (pullback.fst f₁ f₂)) (pullbackMk f₁ f₂ x₁ x₂ h) = x₁

@[simp]

theorem CategoryTheory.Limits.Concrete.pullbackMk_snd {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [HasPullback f₁ f₂] [PreservesLimit (cospan f₁ f₂) (forget C)] (x₁ : ToType X₁) (x₂ : ToType X₂) (h : (ConcreteCategory.hom f₁) x₁ = (ConcreteCategory.hom f₂) x₂) : (ConcreteCategory.hom (pullback.snd f₁ f₂)) (pullbackMk f₁ f₂ x₁ x₂ h) = x₂

theorem CategoryTheory.Limits.Concrete.widePullback_ext {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {B : C} {ι : Type w} {X : ι → C} (f : (j : ι) → X j ⟶ B) [HasWidePullback B X f] [PreservesLimit (WidePullbackShape.wideCospan B X f) (forget C)] (x y : ToType (widePullback B X f)) (h₀ : (ConcreteCategory.hom (WidePullback.base f)) x = (ConcreteCategory.hom (WidePullback.base f)) y) (h : ∀ (j : ι), (ConcreteCategory.hom (WidePullback.π f j)) x = (ConcreteCategory.hom (WidePullback.π f j)) y) : x = y

theorem CategoryTheory.Limits.Concrete.widePullback_ext' {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {B : C} {ι : Type w} [Nonempty ι] {X : ι → C} (f : (j : ι) → X j ⟶ B) [HasWidePullback B X f] [PreservesLimit (WidePullbackShape.wideCospan B X f) (forget C)] (x y : ToType (widePullback B X f)) (h : ∀ (j : ι), (ConcreteCategory.hom (WidePullback.π f j)) x = (ConcreteCategory.hom (WidePullback.π f j)) y) : x = y

theorem CategoryTheory.Limits.Concrete.multiequalizer_ext {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : MulticospanShape} {I : MulticospanIndex J C} [HasMultiequalizer I] [PreservesLimit I.multicospan (forget C)] (x y : ToType (multiequalizer I)) (h : ∀ (t : J.L), (ConcreteCategory.hom (Multiequalizer.ι I t)) x = (ConcreteCategory.hom (Multiequalizer.ι I t)) y) : x = y

def CategoryTheory.Limits.Concrete.multiequalizerEquivAux {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : MulticospanShape} (I : MulticospanIndex J C) : ↑(I.multicospan.comp (forget C)).sections ≃ { x : (i : J.L) → ToType (I.left i) // ∀ (i : J.R), (ConcreteCategory.hom (I.fst i)) (x (J.fst i)) = (ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }

An auxiliary equivalence to be used in multiequalizerEquiv below.

Equations

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

noncomputable def CategoryTheory.Limits.Concrete.multiequalizerEquiv {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] [PreservesLimit I.multicospan (forget C)] : ToType (multiequalizer I) ≃ { x : (i : J.L) → ToType (I.left i) // ∀ (i : J.R), (ConcreteCategory.hom (I.fst i)) (x (J.fst i)) = (ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }

The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] [PreservesLimit I.multicospan (forget C)] (x : ToType (multiequalizer I)) (i : J.L) : ↑((multiequalizerEquiv I) x) i = (ConcreteCategory.hom (Multiequalizer.ι I i)) x

theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {B : C} {α : Type v} {X : α → C} (f : (j : α) → B ⟶ X j) [HasWidePushout B X f] [PreservesColimit (WidePushoutShape.wideSpan B X f) (forget C)] (x : ToType (widePushout B X f)) : (∃ (y : ToType B), (ConcreteCategory.hom (WidePushout.head f)) y = x) ∨ ∃ (i : α) (y : ToType (X i)), (ConcreteCategory.hom (WidePushout.ι f i)) y = x

theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep' {C : Type u} [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {B : C} {α : Type v} [Nonempty α] {X : α → C} (f : (j : α) → B ⟶ X j) [HasWidePushout B X f] [PreservesColimit (WidePushoutShape.wideSpan B X f) (forget C)] (x : ToType (widePushout B X f)) : ∃ (i : α) (y : ToType (X i)), (ConcreteCategory.hom (WidePushout.ι f i)) y = x

theorem CategoryTheory.Limits.Concrete.cokernel_funext {C : Type u_1} [Category.{u_4, u_1} C] [HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {M N K : C} {f : M ⟶ N} [HasCokernel f] {g h : cokernel f ⟶ K} (w : ∀ (n : ToType N), (ConcreteCategory.hom g) ((ConcreteCategory.hom (cokernel.π f)) n) = (ConcreteCategory.hom h) ((ConcreteCategory.hom (cokernel.π f)) n)) : g = h