Documentation

Mathlib.CategoryTheory.Functor.Const

The constant functor #

const J : C ā„¤ (J ā„¤ C) is the functor that sends an object X : C to the functor J ā„¤ C sending every object in J to X, and every morphism to šŸ™ X.

When J is nonempty, const is faithful.

We have (const J).obj X ā‹™ F ā‰… (const J).obj (F.obj X) for any F : C ā„¤ D.

@[simp]

The functor sending X : C to the constant functor J ā„¤ C sending everything to X.

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

    The constant functor Jįµ’įµ– ā„¤ Cįµ’įµ– sending everything to op X is (naturally isomorphic to) the opposite of the constant functor J ā„¤ C sending everything to X.

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

      The constant functor Jįµ’įµ– ā„¤ C sending everything to unop X is (naturally isomorphic to) the opposite of the constant functor J ā„¤ Cįµ’įµ– sending everything to X.

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

        These are actually equal, of course, but not definitionally equal (the equality requires F.map (šŸ™ _) = šŸ™ _). A natural isomorphism is more convenient than an equality between functors (compare id_to_iso).

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

          If J is nonempty, then the constant functor over J is faithful.

          Equations
          • ā‹Æ = ā‹Æ

          The canonical isomorphism F ā‹™ Functor.const J ā‰… Functor.const F ā‹™ (whiskeringRight J _ _).obj L.

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