Theorems · Theorem · category theory

CompHausLike.LocallyConstant.counit_app_hom_app_hom_apply

∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
  (x : (CompHausLike P)ᵒᵖ)
  (r : LocallyConstant (↑(Opposite.unop x).toTop) (X.obj.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))),
  (CategoryTheory.ConcreteCategory.hom (((CompHausLike.LocallyConstant.counit P hs).app X).hom.app x)) r =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.LocallyConstant.sigmaIso r).inv.op))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv (CompHausLike.sigmaComparison X.obj fun a => ↑↑a)))
        (CompHausLike.LocallyConstant.counitAppAppImage r))

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasPropCompHausLike.HasPropCompHausLike.HasExplicitFiniteCoproductsCompHausLike.HasExplicitPullbacksCompHausLike.HasExplicitFiniteCoproducts