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.instPreservesFiniteLimitsToFunctorOfClass {α : Type u} {β : Type v} {F : Type u_1} [FunLike F α β] (f : F) [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [InfTopHomClass F α β] : PreservesFiniteLimits (↑f).toFunctor

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] : PreservesColimitsOfShape J (↑f).toFunctor

instance CategoryTheory.Limits.CompleteLattice.instPreservesFiniteColimitsToFunctorOfClass {α : Type u} {β : Type v} {F : Type u_1} [FunLike F α β] (f : F) [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [SupBotHomClass F α β] : PreservesFiniteColimits (↑f).toFunctor

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 α β] : PreservesLimitsOfSize.{w', w, u, v, u, v} (↑f).toFunctor

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] : PreservesColimitsOfShape J (↑f).toFunctor

instance CategoryTheory.Limits.CompleteLattice.preservesColimitsOfSize_toFunctor {α : Type u} {β : Type v} {F : Type u_1} [FunLike F α β] (f : F) [CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] : PreservesColimitsOfSize.{w', w, u, v, u, v} (↑f).toFunctor

instance CategoryTheory.Limits.CompleteLattice.preservesColimits_toFunctor {α : Type u} {β : Type v} {F : Type u_1} [FunLike F α β] (f : F) [CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] : PreservesColimits (↑f).toFunctor