PhysLean Documentation

PhysLean.Relativity.Tensors.OverColor.Functors

source
def IndexNotation.OverColor.map {C D : Type} (f : C → D) :
CategoryTheory.Functor (OverColor C) (OverColor D)

The monoidal functor from OverColor C to OverColor D constructed from a map f : C → D.

Equations
Instances For
    source
    instance IndexNotation.OverColor.map_laxMonoidal {C D : Type} (f : C → D) :
    (map f).LaxMonoidal

    The functor map f is lax-monoidal.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance IndexNotation.OverColor.map_monoidal {C D : Type} (f : C → D) :
    (map f).Monoidal

    The functor map f is lax-monoidal.

    Equations
    source
    def IndexNotation.OverColor.tensor (C : Type) :
    CategoryTheory.Functor (OverColor C × OverColor C) (OverColor C)

    The tensor product on OverColor C as a monoidal functor.

    Equations
    Instances For
      source
      instance IndexNotation.OverColor.tensor_laxMonoidal (C : Type) :
      (tensor C).LaxMonoidal

      The functor tensor is lax-monoidal.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      noncomputable instance IndexNotation.OverColor.tensor_monoidal (C : Type) :
      (tensor C).Monoidal

      The functor tensor is monoidal.

      Equations
      source
      def IndexNotation.OverColor.const (C : Type) :
      CategoryTheory.Functor (OverColor C) (OverColor C)

      The constant monoidal functor from OverColor C to itself landing on 𝟙_ (OverColor C).

      Equations
      Instances For
        source
        instance IndexNotation.OverColor.const_laxMonoidal (C : Type) :
        (const C).LaxMonoidal

        The functor const C is lax monoidal.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        noncomputable instance IndexNotation.OverColor.const_monoidal (C : Type) :
        (const C).Monoidal

        The functor const C is monoidal.

        Equations
        source
        def IndexNotation.OverColor.contrPair (C : Type) (τ : C → C) :
        CategoryTheory.Functor (OverColor C) (OverColor C)

        The monoidal functor from OverColor C to OverColor C taking f to f ⊗ τ_* f.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance IndexNotation.OverColor.contrPair_laxMonoidal (C : Type) (τ : C → C) :
          (contrPair C τ).LaxMonoidal

          The functor contrPair is lax-monoidal.

          Equations
          • One or more equations did not get rendered due to their size.
          source
          noncomputable instance IndexNotation.OverColor.contrPair_monoidal (C : Type) (τ : C → C) :
          (contrPair C τ).Monoidal

          The functor contrPair is monoidal.

          Equations