Abstract boundedness problems

A minimal categorical interface for a collection of moduli problems and the predicate that each is bounded. Stability-family and geometric packages may consume this interface, but boundedness itself does not depend on a triangulated category, a stability condition, or a geometric realization.

structure CategoryTheory.Moduli.BoundednessProblem (M : Type u) : Type u

Abstract moduli problems and the predicate expressing their boundedness.

• IsBounded : M → Prop

  The boundedness predicate for each supplied moduli problem.

def CategoryTheory.Moduli.UniversalBoundedness {M : Type u} (P : BoundednessProblem M) : Prop

Every supplied moduli problem is bounded.

Equations

• CategoryTheory.Moduli.UniversalBoundedness P = ∀ (m : M), P.IsBounded m