Theorems · Theorem · category theory

LightCondSet.topCatAdjunctionUnit_hom_app

∀ (X : LightCondSet) (S : LightProfiniteᵒᵖ),
  X.topCatAdjunctionUnit.hom.app S =
    TypeCat.ofHom fun x =>
      {
        toFun := fun s =>
          (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) s).op))
            x,
        continuous_toFun := ⋯ }

Defined in

Mathlib.Condensed.Light.TopCatAdjunction

Cited by

0 results in Mathlib

Foundations

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