Theorems · Theorem · category theory

LightCondMod.factorsThru_lightProfinite_epi_of_epi

∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) [CategoryTheory.Epi f] {S : LightProfinite}
  (p : (LightCondensed.free R).obj S.toCondensed ⟶ Y),
  ∃ T π g,
    CategoryTheory.Epi π ∧
      CategoryTheory.CategoryStruct.comp ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π) p =
        CategoryTheory.CategoryStruct.comp g f

Defined in

Mathlib.Condensed.Light.Epi

Cited by

1 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCategoryTheory.Epi