Theorems · Theorem · category theory

LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite

∀ (A : Type u') [inst : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)] {X Y : LightCondensed A} (f : X ⟶ Y),
  CategoryTheory.Sheaf.IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : CategoryTheory.ToType (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.Light.Epi

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Limits.PreservesFiniteProducts