Theorems · Theorem · category theory

Condensed.epi_iff_surjective_on_stonean

∀ (A : Type u') [inst : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)]
  [∀ (X : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A]
  [(CategoryTheory.extensiveTopology Stonean).WEqualsLocallyBijective A]
  [CategoryTheory.HasSheafify (CategoryTheory.extensiveTopology Stonean) A]
  [(CategoryTheory.extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology Stonean) A)],
  CategoryTheory.Epi f ↔
    ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.compHaus)))

Defined in

Mathlib.Condensed.Epi

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorizationCategoryTheory.Limits.PreservesFiniteProductsCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.HasSheafComposeCategoryTheory.Balanced