Pro-zero diagrams and pro-isomorphisms

A diagram F : J ⥤ C in a category with zero morphisms is pro-zero if every object F j is killed by some map of the diagram: for every j there is f : i ⟶ j with F.map f = 0. For an inverse system A₀ ← A₁ ← A₂ ← ⋯ this says that for every n some composite transition Aₘ → Aₙ with m ≥ n is zero; for a cofiltered J it says that F is the zero pro-object. Being pro-zero is a condition on the transition maps, not on the limit: the tower ℤ ← ℤ ← ⋯ with transitions multiplication by a prime p has zero limit but is not pro-zero.

In an abelian category, pro-zero diagrams form a Serre class of the functor category. The pro-isomorphisms are the morphisms of diagrams whose kernel and cokernel are pro-zero; this is Mathlib's ObjectProperty.isoModSerre for that Serre class, so pro-isomorphisms are stable under composition and retracts and satisfy two-out-of-three. Pro-zero diagrams, and pro-isomorphisms, are the error terms that derived limits of towers cannot see.

Main declarations

• CategoryTheory.Functor.IsProZero: pro-zero diagrams.
• CategoryTheory.Functor.isProZero_iff_forall_exists_le: the form of the condition for inverse systems indexed by a preorder.
• CategoryTheory.Functor.IsProZero.isZero_of_isLimit: a limit of a pro-zero diagram is zero.
• CategoryTheory.Functor.isProZero_comp_iff: being pro-zero is invariant under reindexing along an initial functor out of a cofiltered category; CategoryTheory.Functor.isProZero_monotone_comp_iff is the case of a cofinal monotone reindexing of inverse systems.
• CategoryTheory.Functor.isSerreClass_isProZero: in an abelian category, pro-zero diagrams form a Serre class.
• CategoryTheory.Functor.proIsomorphisms: the pro-isomorphisms of diagrams.

References

• B. Bhatt, On the direct summand conjecture and its derived variant, Invent. Math. 212 (2018), §3 (pro-zero towers, in their almost form).

def CategoryTheory.Functor.IsProZero {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] (F : Functor J C) : Prop

A diagram F : J ⥤ C is pro-zero if every object F j is killed by some map of the diagram: for every j there is f : i ⟶ j with F.map f = 0. For towers ℕᵒᵖ ⥤ C this says that every term is killed by some later composite transition (isProZero_iff_forall_exists_le).

theorem CategoryTheory.Functor.isProZero_iff {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] (F : Functor J C) : F.IsProZero ↔ ∀ (j : J), ∃ (i : J) (f : i ⟶ j), F.map f = 0

theorem CategoryTheory.Functor.isProZero_of_isZero {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] {F : Functor J C} (hF : Limits.IsZero F) : F.IsProZero

A zero diagram is pro-zero.

@[simp]

theorem CategoryTheory.Functor.isProZero_zero {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] : IsProZero 0

theorem CategoryTheory.Functor.isProZero_iff_forall_exists_le {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] {ι : Type u₃} [Preorder ι] (F : Functor ιᵒᵖ C) : F.IsProZero ↔ ∀ (i : ι), ∃ (j : ι) (h : i ≤ j), F.map (homOfLE h).op = 0

A diagram indexed by the opposite of a preorder is pro-zero exactly when every term is killed by the transition from some later term.

theorem CategoryTheory.Functor.isProZero_of_map_succ_eq_zero {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] (F : Functor ℕᵒᵖ C) (hF : ∀ (n : ℕ), F.map (homOfLE ⋯).op = 0) : F.IsProZero

A tower whose successive transitions are zero is pro-zero, whatever its terms.

theorem CategoryTheory.Functor.IsProZero.isZero_of_isLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] {F : Functor J C} (hF : F.IsProZero) {c : Limits.Cone F} (hc : Limits.IsLimit c) : Limits.IsZero c.pt

The limit of a pro-zero diagram is a zero object.

theorem CategoryTheory.Functor.isProZero_comp_iff {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] {I : Type u₃} [Category.{v₃, u₃} I] [IsCofilteredOrEmpty I] (G : Functor I J) [G.Initial] (F : Functor J C) : (G.comp F).IsProZero ↔ F.IsProZero

Cofinal reindexing. For an initial functor G : I ⥤ J out of a cofiltered category, a diagram F : J ⥤ C is pro-zero exactly when G ⋙ F is.

theorem CategoryTheory.Functor.isProZero_monotone_comp_iff {C : Type u₂} [Category.{v₂, u₂} C] [Limits.HasZeroMorphisms C] {ι : Type u₃} {κ : Type u₄} [Preorder ι] [IsDirectedOrder ι] [Preorder κ] {φ : ι → κ} (hφ : Monotone φ) (hcof : ∀ (k : κ), ∃ (i : ι), k ≤ φ i) (F : Functor κᵒᵖ C) : (hφ.functor.op.comp F).IsProZero ↔ F.IsProZero

Cofinal monotone reindexing of inverse systems. If φ : ι → κ is monotone and cofinal and ι is directed, then an inverse system F indexed by κ is pro-zero exactly when its reindexing along φ is.

instance CategoryTheory.Functor.isSerreClass_isProZero {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Abelian C] : ObjectProperty.IsSerreClass IsProZero

In an abelian category, pro-zero diagrams form a Serre class of the functor category: they contain zero and are closed under subobjects, quotients and extensions.

@[reducible, inline]

abbrev CategoryTheory.Functor.proIsomorphisms (J : Type u₁) [Category.{v₁, u₁} J] (C : Type u₂) [Category.{v₂, u₂} C] [Abelian C] : MorphismProperty (Functor J C)

The pro-isomorphisms of diagrams J ⥤ C: the morphisms whose kernel and cokernel are pro-zero (proIsomorphisms_iff). This is Mathlib's class ObjectProperty.isoModSerre of isomorphisms modulo the Serre class of pro-zero diagrams, so pro-isomorphisms are stable under composition and retracts and satisfy two-out-of-three.

theorem CategoryTheory.Functor.proIsomorphisms_iff {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Abelian C] {F G : Functor J C} (f : F ⟶ G) : proIsomorphisms J C f ↔ (Limits.kernel f).IsProZero ∧ (Limits.cokernel f).IsProZero