Documentation

Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

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.

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

    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

      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

        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

          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

            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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X₁ : C} {X₂ : C} {S : C} (f₁ : X₁ S) (f₂ : X₂ S) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)] (x₁ : (CategoryTheory.forget C).obj X₁) (x₂ : (CategoryTheory.forget C).obj X₂) (h : f₁ x₁ = f₂ x₂) :

              Constructor for elements in a pullback in a concrete category.

              Equations
              Instances For
                theorem CategoryTheory.Limits.Concrete.pullbackMk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X₁ : C} {X₂ : C} {S : C} (f₁ : X₁ S) (f₂ : X₂ S) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)] (x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.pullback f₁ f₂)) :
                ∃ (x₁ : (CategoryTheory.forget C).obj X₁) (x₂ : (CategoryTheory.forget C).obj X₂) (h : f₁ x₁ = f₂ x₂), x = CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h
                @[simp]
                theorem CategoryTheory.Limits.Concrete.pullbackMk_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X₁ : C} {X₂ : C} {S : C} (f₁ : X₁ S) (f₂ : X₂ S) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)] (x₁ : (CategoryTheory.forget C).obj X₁) (x₂ : (CategoryTheory.forget C).obj X₂) (h : f₁ x₁ = f₂ x₂) :
                @[simp]
                theorem CategoryTheory.Limits.Concrete.pullbackMk_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X₁ : C} {X₂ : C} {S : C} (f₁ : X₁ S) (f₂ : X₂ S) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)] (x₁ : (CategoryTheory.forget C).obj X₁) (x₂ : (CategoryTheory.forget C).obj X₂) (h : f₁ x₁ = f₂ x₂) :
                def CategoryTheory.Limits.Concrete.multiequalizerEquivAux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] (I : CategoryTheory.Limits.MulticospanIndex C) :
                (I.multicospan.comp (CategoryTheory.forget C)).sections { x : (i : I.L) → (CategoryTheory.forget C).obj (I.left i) // ∀ (i : I.R), (I.fst i) (x (I.fstTo i)) = (I.snd i) (x (I.sndTo i)) }

                An auxiliary equivalence to be used in multiequalizerEquiv below.

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

                  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