AB5

Stream: condensed mathematics

[Adam Topaz]

Any takers for

-- Axiom AB5 for `AddCommGroup`
theorem exact_colim_map_iff_of_is_filtered
  (F G H : J ⥤ AddCommGroup.{u}) (η : F ⟶ G) (γ : G ⟶ H) :
  exact (limits.colim_map η) (limits.colim_map γ) ↔ (∀ j, exact (η.app j) (γ.app j)) :=
sorry

??? If so, take a look at for_mathlib/exact_filtered_colimits

[Adam Topaz]

(condensed/ab5 has a proof of ab5 for condensed ab using that theorem)

[Peter Scholze]

iff not if?

[Adam Topaz]

Oops

[Adam Topaz]

fixed

[Adam Topaz]

From for_mathlib/exact_filtered_colimits

-- Axiom AB5 for `AddCommGroup`
theorem exact_colim_of_exact_of_is_filtered
  (F G H : J ⥤ AddCommGroup.{u}) (η : F ⟶ G) (γ : G ⟶ H) :
  (∀ j, exact (η.app j) (γ.app j)) → exact (limits.colim_map η) (limits.colim_map γ) :=
sorry

[Adam Topaz]

The condensed proof is fixed as well.

[Adam Topaz]

Alright I was embarrassed enough that I had to prove exact_colim_of_exact_of_is_filtered...