AB axioms in condensed modules

This file proves that the category of condensed modules over a ring satisfies Grothendieck's axioms AB5, AB4, and AB4*.

theorem Condensed.hasExactColimitsOfShape (A : Type u_1) (J : Type u_2) [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A] [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasExactColimitsOfShape J A] [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.HasExactColimitsOfShape J (Condensed A)

theorem Condensed.hasExactLimitsOfShape (A : Type u_1) (J : Type u_2) [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A] [∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A] [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A] [CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A] [CategoryTheory.Limits.HasFiniteColimits A] : CategoryTheory.HasExactLimitsOfShape J (Condensed A)

theorem Condensed.instHasLimitsOfSizeModuleCat (R : Type (u + 1)) [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)

instance Condensed.instAB5CondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.AB5 (CondensedMod R)

instance Condensed.instAB4CondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.AB4 (CondensedMod R)

instance Condensed.instAB4StarCondensedMod (R : Type (u + 1)) [Ring R] : CategoryTheory.AB4Star (CondensedMod R)