Lattice Homs that Preserve Limits and Colimits #
This file provides instances for when OrderHom.toFunctor preserves limits/colimits.
In particular, if f preserves finite infs/sups (i.e. is from a InfTopHomClass/SupBotHomClass)
then (toOrderHom f).toFunctor preserves finite limits/colimits. If f preserves
arbitrary infs/sups (i.e. is from a sInfHomClass/sSupHomClass) then (toOrderHom f).toFunctor
preserves all limits/colimits.
instance
CategoryTheory.Limits.CompleteLattice.preservesLimit_finite_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeInf α]
[OrderTop α]
[SemilatticeInf β]
[OrderTop β]
[InfTopHomClass F α β]
{J : Type w}
[SmallCategory J]
[FinCategory J]
(K : Functor J α)
:
PreservesLimit K (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_finite_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeInf α]
[OrderTop α]
[SemilatticeInf β]
[OrderTop β]
[InfTopHomClass F α β]
{J : Type w}
[SmallCategory J]
[FinCategory J]
:
PreservesLimitsOfShape J (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.instPreservesFiniteLimitsToFunctorToOrderHom
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeInf α]
[OrderTop α]
[SemilatticeInf β]
[OrderTop β]
[InfTopHomClass F α β]
:
instance
CategoryTheory.Limits.CompleteLattice.preservesColimit_finite_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeSup α]
[OrderBot α]
[SemilatticeSup β]
[OrderBot β]
[SupBotHomClass F α β]
{J : Type w}
[SmallCategory J]
[FinCategory J]
(K : Functor J α)
:
PreservesColimit K (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfShape_finite_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeSup α]
[OrderBot α]
[SemilatticeSup β]
[OrderBot β]
[SupBotHomClass F α β]
{J : Type w}
[SmallCategory J]
[FinCategory J]
:
instance
CategoryTheory.Limits.CompleteLattice.instPreservesFiniteColimitsToFunctorToOrderHom
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[SemilatticeSup α]
[OrderBot α]
[SemilatticeSup β]
[OrderBot β]
[SupBotHomClass F α β]
:
instance
CategoryTheory.Limits.CompleteLattice.preservesLimit_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
{J : Type w}
[Category.{w', w} J]
(K : Functor J α)
:
PreservesLimit K (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
{J : Type w}
[Category.{w', w} J]
:
PreservesLimitsOfShape J (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfSize_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
:
instance
CategoryTheory.Limits.CompleteLattice.preservesLimits_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sInfHomClass F α β]
:
PreservesLimits (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesColimit_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
{J : Type w}
[Category.{w', w} J]
(K : Functor J α)
:
PreservesColimit K (↑f).toFunctor
instance
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfShape_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
{J : Type w}
[Category.{w', w} J]
:
instance
CategoryTheory.Limits.CompleteLattice.preservesColimitsOfSize_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
:
instance
CategoryTheory.Limits.CompleteLattice.preservesColimits_toFunctor
{α : Type u}
{β : Type v}
{F : Type u_1}
[FunLike F α β]
(f : F)
[CompleteLattice α]
[CompleteLattice β]
[sSupHomClass F α β]
: