CategoryTheory.Functor.Representable.has_representation
theorem CategoryTheory.Functor.Representable.has_representation :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
[self : F.Representable], ∃ X, Nonempty (CategoryTheory.yoneda.obj X ≅ F)
This theorem states that for any category `C` and any representable functor `F` from the opposite of `C` to the Type category, there exists an object `X` in `C` such that the functor represented by `X` (the functor `Hom(-,X)`) is naturally isomorphic to `F`. This is a statement of the Representable Functor Theorem in category theory, which says that a functor is representable if and only if it is naturally isomorphic to a Hom-functor.
More concisely: For any category `C` and any oppositive functor `F: C^op -> Type`, there exists an object `X` in `C` such that `F` is naturally isomorphic to the Hom functor `Hom(-, X)`.
|
CategoryTheory.Yoneda.isIso
theorem CategoryTheory.Yoneda.isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.IsIso (CategoryTheory.yoneda.map f)], CategoryTheory.IsIso f
This theorem states that if the Yoneda map of a morphism `f` in a category `C` is an isomorphism, then the original morphism `f` itself is also an isomorphism. Here, `f` is a morphism from object `X` to object `Y` in the category. The Yoneda map applies a functor to `f`, and the theorem says that if this leads to an isomorphism in the functor category, then `f` was already an isomorphism in `C`.
More concisely: If the Yoneda map of a morphism is an isomorphism in the functor category, then the morphism is an isomorphism in the original category.
|
CategoryTheory.Coyoneda.isIso
theorem CategoryTheory.Coyoneda.isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y)
[inst_1 : CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)], CategoryTheory.IsIso f
This theorem states that in a category `C`, for any objects `X` and `Y` in the opposite category `Cᵒᵖ` and any morphism `f` from `X` to `Y`, if the map `coyoneda.map f` is an isomorphism, then `f` was also an isomorphism. In other words, the `coyoneda` functor preserves the property of being an isomorphism.
More concisely: In the opposite category `Cᵒᵖ`, if the natural transformation `coyoneda.map` induced by a morphism `f` is an isomorphism, then `f` itself is an isomorphism.
|
CategoryTheory.Functor.Corepresentable.has_corepresentation
theorem CategoryTheory.Functor.Corepresentable.has_corepresentation :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)}
[self : F.Corepresentable], ∃ X, Nonempty (CategoryTheory.coyoneda.obj X ≅ F)
The theorem `CategoryTheory.Functor.Corepresentable.has_corepresentation` states that for any category `C` and functor `F` from `C` to the category of types, if `F` is corepresentable, then there exists an object `X` in the opposite category of `C` such that the functor represented by `X` (given by the hom-functor `Hom(X,-)`) is naturally isomorphic to `F`. Essentially, this theorem asserts that a corepresentable functor is actually represented by some object.
More concisely: If `F : C -> Type` is a corepresentable functor on a category `C`, then there exists an object `X` in the opposite category of `C` such that `F ≅ Hom(X, -)`.
|