Theorems · Definition · category theory

LightCondensed.lanPresheafExt

{F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} →
  (FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G) →
    (LightCondensed.lanPresheaf F ≅ LightCondensed.lanPresheaf G)

To presheaves on LightProfinite whose restrictions to finite sets are isomorphic have isomorphic left Kan extensions.

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

3 results in Mathlib

Foundations

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