Theorems · Theorem · category theory

CondensedMod.epi_iff_locallySurjective_on_compHaus

∀ (R : Type (u + 1)) [inst : Ring R] {X Y : CondensedMod R} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : CompHaus) (y : ↑(Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Defined in

Mathlib.Condensed.Epi

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring