Small sets in the category of structured arrows

Here we prove a technical result about small sets in the category of structured arrows that will be used in the proof of the Special Adjoint Functor Theorem.

instance CategoryTheory.StructuredArrow.instSmallOfLocallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : D} {T : Functor C D} [Small.{w, u₁} C] [LocallySmall.{w, v₂, u₂} D] : Small.{w, max u₁ v₂} (StructuredArrow S T)

instance CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : D} {T : Functor C D} {P : ObjectProperty C} [ObjectProperty.Small.{v₁, v₁, u₁} P] [LocallySmall.{v₁, v₂, u₂} D] : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

instance CategoryTheory.StructuredArrow.essentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : D} {T : Functor C D} [EssentiallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] : EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)

@[deprecated CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall (since := "2025-10-07")]

theorem CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : D} {T : Functor C D} {P : ObjectProperty C} [ObjectProperty.Small.{v₁, v₁, u₁} P] [LocallySmall.{v₁, v₂, u₂} D] : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Alias of CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall.

instance CategoryTheory.CostructuredArrow.instSmallOfLocallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : Functor C D} {T : D} [Small.{w, u₁} C] [LocallySmall.{w, v₂, u₂} D] : Small.{w, max u₁ v₂} (CostructuredArrow S T)

instance CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : Functor C D} {T : D} {P : ObjectProperty C} [ObjectProperty.Small.{v₁, v₁, u₁} P] [LocallySmall.{v₁, v₂, u₂} D] : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

instance CategoryTheory.CostructuredArrow.essentiallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : Functor C D} {T : D} [EssentiallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] : EssentiallySmall.{w, v₁, max u₁ v₂} (CostructuredArrow S T)

@[deprecated CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall (since := "2025-10-07")]

theorem CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {S : Functor C D} {T : D} {P : ObjectProperty C} [ObjectProperty.Small.{v₁, v₁, u₁} P] [LocallySmall.{v₁, v₂, u₂} D] : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Alias of CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall.