Internal projectivity

This file defines internal projectivity of objects P in a category C as a class InternallyProjective P. This means that the functor taking internal homs out of P preserves epimorphisms. It also proves that a retract of an internally projective object is internally projective (see InternallyProjective.ofRetract).

This property is important in the setting of light condensed abelian groups, when establishing the solid theory (see the lecture series on analytic stacks: https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO).

def CategoryTheory.isInternallyProjective {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [MonoidalClosed C] : ObjectProperty C

An object P : C is internally projective if the functor P ⟶[C] - taking internal homs out of P preserves epimorphisms.

Equations

• CategoryTheory.isInternallyProjective P = (CategoryTheory.ihom P).PreservesEpimorphisms

@[reducible, inline]

abbrev CategoryTheory.InternallyProjective {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (P : C) : Prop

An object P : C is internally projective if the functor P ⟶[C] - taking internal homs out of P preserves epimorphisms.

Equations

• CategoryTheory.InternallyProjective P = CategoryTheory.isInternallyProjective.Is P

instance CategoryTheory.InternallyProjective.preserves_epi {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [MonoidalClosed C] (P : C) [InternallyProjective P] : (ihom P).PreservesEpimorphisms

instance CategoryTheory.instIsStableUnderRetractsIsInternallyProjective {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [MonoidalClosed C] : isInternallyProjective.IsStableUnderRetracts

theorem CategoryTheory.InternallyProjective.ofRetract {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] [MonoidalClosed C] {X Y : C} (r : Retract Y X) [InternallyProjective X] : InternallyProjective Y