Universally stable object properties of pseudofunctors

For an object property P on a Cat-valued pseudofunctor F, this file defines the subproperty consisting of objects whose image along every outgoing morphism again satisfies P. This universally stable closure is preserved by every transition by construction; the proof uses the compositor of F, so Mathlib's Pseudofunctor.ObjectProperty.fullsubcategory turns it into an actual replete sub-pseudofunctor.

This is the repository's generic subprestack root. A geometric locus should supply an object property and the relevant preservation theorem instead of defining a second subprestack carrier in its consumer directory.

def CategoryTheory.Pseudofunctor.ObjectProperty.universallyStable {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) : F.ObjectProperty

The objects satisfying P after every base change represented by an outgoing morphism in the source bicategory.

Equations

• P.universallyStable = { prop := fun (X : B) (M : ↑(F.obj X)) => ∀ (Y : B) (f : X ⟶ Y), P.prop Y ((F.map f).toFunctor.obj M) }

instance CategoryTheory.Pseudofunctor.ObjectProperty.universallyStable_isClosedUnderIsomorphisms {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderIsomorphisms] : P.universallyStable.IsClosedUnderIsomorphisms

instance CategoryTheory.Pseudofunctor.ObjectProperty.universallyStable_isClosedUnderMapObj {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderIsomorphisms] : P.universallyStable.IsClosedUnderMapObj

theorem CategoryTheory.Pseudofunctor.ObjectProperty.universallyStable_le_self {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderIsomorphisms] (X : B) : P.universallyStable.prop X ≤ P.prop X

A universally stable object satisfies the original property before base change. The comparison is the unit isomorphism of the pseudofunctor.

theorem CategoryTheory.Pseudofunctor.ObjectProperty.le_universallyStable {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.prop X ≤ P.universallyStable.prop X

If P is already preserved by every transition, every P-object is universally stable.

theorem CategoryTheory.Pseudofunctor.ObjectProperty.universallyStable_eq_self {B : Type u} [Bicategory B] {F : Pseudofunctor B Cat} (P : F.ObjectProperty) [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderMapObj] (X : B) : P.universallyStable.prop X = P.prop X

A transition-stable property agrees fiberwise with its universally stable closure.