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 : (forget C).obj (∏ᶜ F) ≃ ∀ j, 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]
[HasForget C]
{J : Type w}
(F : J → C)
[HasProduct F]
[PreservesLimit (Discrete.functor F) (forget C)]
:
The equivalence (forget C).obj (∏ᶜ F) ≃ ∀ j, 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Concrete.productEquiv_apply_apply
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
(F : J → C)
[HasProduct F]
[PreservesLimit (Discrete.functor F) (forget C)]
(x : (forget C).obj (∏ᶜ F))
(j : J)
:
(productEquiv F) x j = (Pi.π F j) x
@[simp]
theorem
CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
(F : J → C)
[HasProduct F]
[PreservesLimit (Discrete.functor F) (forget C)]
(x : (j : J) → (forget C).obj (F j))
(j : J)
:
(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]
[HasForget D]
(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 : (forget D).obj (F.obj (∏ᶜ f)))
(h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y)
:
x = y
noncomputable def
CategoryTheory.Limits.Concrete.uniqueOfTerminalOfPreserves
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[PreservesLimit (Functor.empty C) (forget C)]
(X : C)
(h : IsTerminal X)
:
If forget C preserves terminals and X is terminal, then (forget C).obj X is a
singleton.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[ReflectsLimit (Functor.empty C) (forget C)]
(X : C)
(h : Unique ((forget C).obj X))
:
If forget C reflects terminals and (forget C).obj X is a singleton, then X is terminal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.terminalIffUnique
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[PreservesLimit (Functor.empty C) (forget C)]
[ReflectsLimit (Functor.empty C) (forget C)]
(X : C)
:
IsTerminal X ≃ Unique ((forget C).obj X)
The equivalence IsTerminal X ≃ Unique ((forget C).obj X) if the forgetful functor
preserves and reflects terminals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.terminalEquiv
(C : Type u)
[Category.{v, u} C]
[HasForget C]
[HasTerminal C]
[PreservesLimit (Functor.empty C) (forget C)]
:
(forget C).obj (⊤_ C) ≃ PUnit.{w + 1}
The equivalence (forget C).obj (⊤_ C) ≃ PUnit when C is a concrete category.
Equations
Instances For
noncomputable instance
CategoryTheory.Limits.Concrete.instUniqueObjForgetTerminal
(C : Type u)
[Category.{v, u} C]
[HasForget C]
[HasTerminal C]
[PreservesLimit (Functor.empty C) (forget C)]
:
Equations
- CategoryTheory.Limits.Concrete.instUniqueObjForgetTerminal 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]
[HasForget C]
[PreservesColimit (Functor.empty C) (forget C)]
(X : C)
(h : Nonempty (IsInitial X))
:
If forget C preserves initials and X is initial, then (forget C).obj X is empty.
theorem
CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[ReflectsColimit (Functor.empty C) (forget C)]
(X : C)
(h : IsEmpty ((forget C).obj X))
:
If forget C reflects initials and (forget C).obj 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]
[HasForget C]
[PreservesColimit (Functor.empty C) (forget C)]
[ReflectsColimit (Functor.empty C) (forget C)]
(X : C)
:
If forget C preserves and reflects initials, then X is initial if and only if
(forget C).obj X is empty.
noncomputable def
CategoryTheory.Limits.Concrete.prodEquiv
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(X₁ X₂ : C)
[HasBinaryProduct X₁ X₂]
[PreservesLimit (pair X₁ X₂) (forget C)]
:
The equivalence (forget C).obj (X₁ ⨯ X₂) ≃ ((forget C).obj X₁) × ((forget C).obj 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.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_apply_fst
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(X₁ X₂ : C)
[HasBinaryProduct X₁ X₂]
[PreservesLimit (pair X₁ X₂) (forget C)]
(x : (forget C).obj (X₁ ⨯ X₂))
:
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_apply_snd
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(X₁ X₂ : C)
[HasBinaryProduct X₁ X₂]
[PreservesLimit (pair X₁ X₂) (forget C)]
(x : (forget C).obj (X₁ ⨯ X₂))
:
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(X₁ X₂ : C)
[HasBinaryProduct X₁ X₂]
[PreservesLimit (pair X₁ X₂) (forget C)]
(x : (forget C).obj X₁ × (forget C).obj X₂)
:
@[simp]
theorem
CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(X₁ X₂ : C)
[HasBinaryProduct X₁ X₂]
[PreservesLimit (pair X₁ X₂) (forget C)]
(x : (forget C).obj X₁ × (forget C).obj X₂)
:
noncomputable def
CategoryTheory.Limits.Concrete.pullbackEquiv
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{X₁ X₂ S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[HasPullback f₁ f₂]
[PreservesLimit (cospan f₁ f₂) (forget C)]
:
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.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.pullbackMk
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{X₁ X₂ S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[HasPullback f₁ f₂]
[PreservesLimit (cospan f₁ f₂) (forget C)]
(x₁ : (forget C).obj X₁)
(x₂ : (forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
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⟩
Instances For
theorem
CategoryTheory.Limits.Concrete.pullbackMk_surjective
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{X₁ X₂ S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[HasPullback f₁ f₂]
[PreservesLimit (cospan f₁ f₂) (forget C)]
(x : (forget C).obj (pullback f₁ f₂))
:
∃ (x₁ : (forget C).obj X₁) (x₂ : (forget C).obj X₂) (h : f₁ x₁ = f₂ x₂), x = pullbackMk f₁ f₂ x₁ x₂ h
@[simp]
theorem
CategoryTheory.Limits.Concrete.pullbackMk_fst
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{X₁ X₂ S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[HasPullback f₁ f₂]
[PreservesLimit (cospan f₁ f₂) (forget C)]
(x₁ : (forget C).obj X₁)
(x₂ : (forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
(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]
[HasForget C]
{X₁ X₂ S : C}
(f₁ : X₁ ⟶ S)
(f₂ : X₂ ⟶ S)
[HasPullback f₁ f₂]
[PreservesLimit (cospan f₁ f₂) (forget C)]
(x₁ : (forget C).obj X₁)
(x₂ : (forget C).obj X₂)
(h : f₁ x₁ = f₂ x₂)
:
(pullback.snd f₁ f₂) (pullbackMk f₁ f₂ x₁ x₂ h) = x₂
theorem
CategoryTheory.Limits.Concrete.widePullback_ext
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{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 : (forget C).obj (widePullback B X f))
(h₀ : (WidePullback.base f) x = (WidePullback.base f) y)
(h : ∀ (j : ι), (WidePullback.π f j) x = (WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.widePullback_ext'
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{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 : (forget C).obj (widePullback B X f))
(h : ∀ (j : ι), (WidePullback.π f j) x = (WidePullback.π f j) y)
:
x = y
theorem
CategoryTheory.Limits.Concrete.multiequalizer_ext
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{I : MulticospanIndex C}
[HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)]
(x y : (forget C).obj (multiequalizer I))
(h : ∀ (t : I.L), (Multiequalizer.ι I t) x = (Multiequalizer.ι I t) y)
:
x = y
def
CategoryTheory.Limits.Concrete.multiequalizerEquivAux
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(I : MulticospanIndex C)
:
An auxiliary equivalence to be used in multiequalizerEquiv below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.Concrete.multiequalizerEquiv
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(I : MulticospanIndex C)
[HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)]
:
(forget C).obj (multiequalizer I) ≃ { x : (i : I.L) → (forget C).obj (I.left i) // ∀ (i : I.R), (I.fst i) (x (I.fstTo i)) = (I.snd i) (x (I.sndTo i)) }
The equivalence between the noncomputable multiequalizer and the concrete multiequalizer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply
{C : Type u}
[Category.{v, u} C]
[HasForget C]
(I : MulticospanIndex C)
[HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)]
(x : (forget C).obj (multiequalizer I))
(i : I.L)
:
↑((multiequalizerEquiv I) x) i = (Multiequalizer.ι I i) x
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{B : C}
{α : Type v}
{X : α → C}
(f : (j : α) → B ⟶ X j)
[HasWidePushout B X f]
[PreservesColimit (WidePushoutShape.wideSpan B X f) (forget C)]
(x : (forget C).obj (widePushout B X f))
:
(∃ (y : (forget C).obj B), (WidePushout.head f) y = x) ∨ ∃ (i : α) (y : (forget C).obj (X i)), (WidePushout.ι f i) y = x
theorem
CategoryTheory.Limits.Concrete.widePushout_exists_rep'
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{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 : (forget C).obj (widePushout B X f))
:
∃ (i : α) (y : (forget C).obj (X i)), (WidePushout.ι f i) y = x
theorem
CategoryTheory.Limits.Concrete.cokernel_funext
{C : Type u_1}
[Category.{u_2, u_1} C]
[HasZeroMorphisms C]
[HasForget C]
{M N K : C}
{f : M ⟶ N}
[HasCokernel f]
{g h : cokernel f ⟶ K}
(w : ∀ (n : (forget C).obj N), g ((cokernel.π f) n) = h ((cokernel.π f) n))
:
g = h