The sheaf of locally constant maps on CompHausLike P

This file proves that under suitable conditions, the functor from the category of sets to the category of sheaves for the coherent topology on CompHausLike P, given by mapping a set to the sheaf of locally constant maps to it, is left adjoint to the "underlying set" functor (evaluation at the point).

We apply this to prove that the constant sheaf functor into (light) condensed sets is isomorphic to the functor of sheaves of locally constant maps described above.

Proof sketch

The hard part of this adjunction is to define the counit. Its components are defined as follows:

Let S : CompHausLike P and let Y be a finite-product preserving presheaf on CompHausLike P (e.g. a sheaf for the coherent topology). We need to define a map LocallyConstant S Y(*) ⟶ Y(S). Given a locally constant map f : S → Y(*), let S = S₁ ⊔ ⋯ ⊔ Sₙ be the corresponding decomposition of S into the fibers. Let yᵢ ∈ Y(*) denote the value of f on Sᵢ and denote by gᵢ the canonical map Y(*) → Y(Sᵢ). Our map then takes f to the image of (g₁(y₁), ⋯, gₙ(yₙ)) under the isomorphism Y(S₁) × ⋯ × Y(Sₙ) ≅ Y(S₁ ⊔ ⋯ ⊔ Sₙ) = Y(S).

Now we need to prove that the counit is natural in S : CompHausLike P and Y : Sheaf (coherentTopology (CompHausLike P)) (Type _). There are two key lemmas in all naturality proofs in this file (both lemmas are in the CompHausLike.LocallyConstant namespace):

• presheaf_ext: given S, Y and f : LocallyConstant S Y(*) like above, another presheaf X, and two elements x y : X(S), to prove that x = y it suffices to prove that for every inclusion map ιᵢ : Sᵢ ⟶ S, X(ιᵢ)(x) = X(ιᵢ)(y). Here it is important that we set everything up in such a way that the Sᵢ are literally subtypes of S.

• incl_of_counitAppApp: given S, Y and f : LocallyConstant S Y(*) like above, we have Y(ιᵢ)(ε_{S, Y}(f)) = gᵢ(yᵢ) where ε denotes the counit and the other notation is like above.

Main definitions

• CompHausLike.LocallyConstant.functor: the functor from the category of sets to the category of sheaves for the coherent topology on CompHausLike P, which takes a set X to LocallyConstant - X

  • CondensedSet.LocallyConstant.functor is the above functor in the case of condensed sets.
  • LightCondSet.LocallyConstant.functor is the above functor in the case of light condensed sets.

• CompHausLike.LocallyConstant.adjunction: the functor described above is left adjoint to the "underlying set" functor (sheafSections _ _).obj ⟨CompHausLike.of P PUnit.{u+1}⟩, which takes a sheaf X to the set X(*).

• CondensedSet.LocallyConstant.iso: the functor CondensedSet.LocallyConstant.functor is isomorphic to the functor Condensed.discrete (Type _) (the constant sheaf functor from sets to condensed sets).

• LightCondSet.LocallyConstant.iso: the functor LightCondSet.LocallyConstant.functor is isomorphic to the functor LightCondensed.discrete (Type _) (the constant sheaf functor from sets to light condensed sets).

def CompHausLike.LocallyConstant.functorToPresheaves {P : TopCat → Prop} : CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))

The functor from the category of sets to presheaves on CompHausLike P given by locally constant maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.functorToPresheaves_obj_map {P : TopCat → Prop} (X : Type (max u w)) {X✝ Y✝ : (CompHausLike P)ᵒᵖ} (f : X✝ ⟶ Y✝) (g : match X✝ with | Opposite.op S => LocallyConstant (↑S.toTop) X) : (CompHausLike.LocallyConstant.functorToPresheaves.obj X).map f g = LocallyConstant.comap f.unop g

@[simp]

theorem CompHausLike.LocallyConstant.functorToPresheaves_map_app {P : TopCat → Prop} {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) (t : ((fun (X : Type (max u w)) => { obj := fun (x : (CompHausLike P)ᵒᵖ) => match x with | Opposite.op S => LocallyConstant (↑S.toTop) X, map := fun {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y) (g : (fun (x : (CompHausLike P)ᵒᵖ) => match x with | Opposite.op S => LocallyConstant (↑S.toTop) X) X_1) => LocallyConstant.comap f.unop g, map_id := ⋯, map_comp := ⋯ }) X✝).obj x✝) : (CompHausLike.LocallyConstant.functorToPresheaves.map f).app x✝ t = LocallyConstant.map f t

@[simp]

theorem CompHausLike.LocallyConstant.functorToPresheaves_obj_obj {P : TopCat → Prop} (X : Type (max u w)) (x✝ : (CompHausLike P)ᵒᵖ) : (CompHausLike.LocallyConstant.functorToPresheaves.obj X).obj x✝ = match x✝ with | Opposite.op S => LocallyConstant (↑S.toTop) X

def CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap (Y : Type u_1) (X : Type u_2) [TopologicalSpace Y] : LocallyConstant Y X ≅ C(Y, ↑(TopCat.discrete.obj X))

Locally constant maps are the same as continuous maps when the target is equipped with the discrete topology

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_inv_apply (Y : Type u_1) (X : Type u_2) [TopologicalSpace Y] (f : C(Y, ↑(TopCat.discrete.obj X))) (a : Y) : ((CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap Y X).inv f) a = f a

@[simp]

theorem CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom (Y : Type u_1) (X : Type u_2) [TopologicalSpace Y] (f : LocallyConstant Y X) : (CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap Y X).hom f = ↑f

def CompHausLike.LocallyConstant.fiber {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) : CompHausLike P

A fiber of a locally constant map as a CompHausLike P.

Equations

• CompHausLike.LocallyConstant.fiber r a = CompHausLike.of P ↑↑a

instance CompHausLike.LocallyConstant.instHasPropαTopologicalSpaceToTopFiber {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) : CompHausLike.HasProp P ↑(CompHausLike.LocallyConstant.fiber r a).toTop

def CompHausLike.LocallyConstant.sigmaIncl {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) : CompHausLike.LocallyConstant.fiber r a ⟶ Q

The inclusion map from a component of the coproduct induced by f into S.

Equations

• CompHausLike.LocallyConstant.sigmaIncl r a = TopologicalSpace.Fiber.sigmaIncl (⇑r) a

noncomputable def CompHausLike.LocallyConstant.sigmaIso {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) [CompHausLike.HasExplicitFiniteCoproducts P] : CompHausLike.finiteCoproduct (CompHausLike.LocallyConstant.fiber r) ≅ Q

The canonical map from the coproduct induced by f to S as an isomorphism in CompHausLike P.

Equations

• CompHausLike.LocallyConstant.sigmaIso r = CompHausLike.isoOfBijective (TopologicalSpace.Fiber.sigmaIsoHom ⇑r) ⋯

theorem CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Q : CompHausLike P} {Z : Type (max u w)} (r : LocallyConstant (↑Q.toTop) Z) (a : Function.Fiber ⇑r) [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) : CategoryTheory.CategoryStruct.comp (X.mapIso (CompHausLike.LocallyConstant.sigmaIso r).op).hom (CategoryTheory.CategoryStruct.comp (CompHausLike.sigmaComparison X fun (a : Function.Fiber ⇑r) => ↑(CompHausLike.LocallyConstant.fiber r a).toTop) fun (g : (a : Function.Fiber ⇑r) → X.obj (Opposite.op (CompHausLike.of P ↑(CompHausLike.LocallyConstant.fiber r a).toTop))) => g a) = X.map (CompHausLike.LocallyConstant.sigmaIncl r a).op

noncomputable def CompHausLike.LocallyConstant.counitAppAppImage {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (a : Function.Fiber ⇑f) : Y.obj (Opposite.op (CompHausLike.LocallyConstant.fiber f a))

The projection of the counit.

Equations

• CompHausLike.LocallyConstant.counitAppAppImage f a = Y.map (CompHausLike.isTerminalPUnit.from (CompHausLike.LocallyConstant.fiber f a)).op (Function.Fiber.image (⇑f) a)

noncomputable def CompHausLike.LocallyConstant.counitAppApp {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] (S : CompHausLike P) (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] [CompHausLike.HasExplicitFiniteCoproducts P] : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y.obj (Opposite.op S)

The counit is defined as follows: given a locally constant map f : S → Y(*), let S = S₁ ⊔ ⋯ ⊔ Sₙ be the corresponding decomposition of S into the fibers. We need to provide an element of Y(S). It suffices to provide an element of Y(Sᵢ) for all i. Let yᵢ ∈ Y(*) denote the value of f on Sᵢ. Our desired element is the image of yᵢ under the canonical map Y(*) → Y(Sᵢ).

Equations

• One or more equations did not get rendered due to their size.

theorem CompHausLike.LocallyConstant.presheaf_ext {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] (x y : X.obj (Opposite.op S)) [CompHausLike.HasExplicitFiniteCoproducts P] (h : ∀ (a : Function.Fiber ⇑f), X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op x = X.map (CompHausLike.LocallyConstant.sigmaIncl f a).op y) : x = y

To check equality of two elements of X(S), it suffices to check equality after composing with each X(S) → X(Sᵢ).

theorem CompHausLike.LocallyConstant.incl_of_counitAppApp {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) [CategoryTheory.Limits.PreservesFiniteProducts Y] [CompHausLike.HasExplicitFiniteCoproducts P] (a : Function.Fiber ⇑f) : Y.map (CompHausLike.LocallyConstant.sigmaIncl f a).op (CompHausLike.LocallyConstant.counitAppApp S Y f) = CompHausLike.LocallyConstant.counitAppAppImage f a

def CompHausLike.LocallyConstant.componentHom {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {S : CompHausLike P} {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) {T : CompHausLike P} (g : T ⟶ S) (a : Function.Fiber ⇑(LocallyConstant.comap g f)) : CompHausLike.LocallyConstant.fiber (LocallyConstant.comap g f) a ⟶ CompHausLike.LocallyConstant.fiber f (Function.Fiber.mk (⇑f) (g (Function.Fiber.preimage (⇑(LocallyConstant.comap g f)) a)))

This is an auxiliary definition, the details do not matter. What's important is that this map exists so that the lemma incl_comap works.

Equations

• CompHausLike.LocallyConstant.componentHom f g a = { toFun := fun (x : ↑(CompHausLike.LocallyConstant.fiber (LocallyConstant.comap g f) a).toTop) => ⟨g ↑x, ⋯⟩, continuous_toFun := ⋯ }

theorem CompHausLike.LocallyConstant.incl_comap {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} [CompHausLike.HasProp P PUnit.{u + 1}] {S T : (CompHausLike P)ᵒᵖ} (f : LocallyConstant (↑(Opposite.unop S).toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) (g : S ⟶ T) (a : Function.Fiber ⇑(LocallyConstant.comap g.unop f)) : CategoryTheory.CategoryStruct.comp g (CompHausLike.LocallyConstant.sigmaIncl (LocallyConstant.comap g.unop f) a).op = CategoryTheory.CategoryStruct.comp (CompHausLike.LocallyConstant.sigmaIncl f (Function.Fiber.mk (⇑f) (g.unop (Function.Fiber.preimage (⇑(LocallyConstant.comap g.unop f)) a)))).op (CompHausLike.LocallyConstant.componentHom f g.unop a).op

noncomputable def CompHausLike.LocallyConstant.counitApp {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] : CompHausLike.LocallyConstant.functorToPresheaves.obj (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y

The counit is natural in S : CompHausLike P

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.counitApp_app {P : TopCat → Prop} [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts Y] (x✝ : (CompHausLike P)ᵒᵖ) (a✝ : (CompHausLike.LocallyConstant.functorToPresheaves.obj (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))).obj x✝) : (CompHausLike.LocallyConstant.counitApp Y).app x✝ a✝ = CompHausLike.LocallyConstant.counitAppApp (Opposite.unop x✝) Y a✝

noncomputable def CompHausLike.LocallyConstant.functorToPresheavesIso (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) (X : Type (max u w)) : CompHausLike.LocallyConstant.functorToPresheaves.obj X ≅ (TopCat.toSheafCompHausLike P (TopCat.discrete.obj X) hs).val

locallyConstantIsoContinuousMap is a natural isomorphism.

Equations

• One or more equations did not get rendered due to their size.

def CompHausLike.LocallyConstant.functor (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CategoryTheory.Functor (Type (max u w)) (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))

CompHausLike.LocallyConstant.functorToPresheaves lands in sheaves.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.functor_obj_val (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) (X : Type (max u w)) : ((CompHausLike.LocallyConstant.functor P hs).obj X).val = CompHausLike.LocallyConstant.functorToPresheaves.obj X

@[simp]

theorem CompHausLike.LocallyConstant.functor_map_val (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) : ((CompHausLike.LocallyConstant.functor P hs).map f).val = CompHausLike.LocallyConstant.functorToPresheaves.map f

noncomputable def CompHausLike.LocallyConstant.functorIso (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CompHausLike.LocallyConstant.functor P hs ≅ TopCat.discrete.comp (topCatToSheafCompHausLike P hs)

CompHausLike.LocallyConstant.functor is naturally isomorphic to the restriction of topCatToSheafCompHausLike to discrete topological spaces.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CompHausLike.LocallyConstant.counit (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] : ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))).comp (CompHausLike.LocallyConstant.functor P hs) ⟶ CategoryTheory.Functor.id (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))

The counit is natural in both S : CompHausLike P and Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.counit_app_val (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))) : ((CompHausLike.LocallyConstant.counit P hs).app X).val = CompHausLike.LocallyConstant.counitApp X.val

def CompHausLike.LocallyConstant.unit (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CategoryTheory.Functor.id (Type (max u u_1)) ⟶ (CompHausLike.LocallyConstant.functor P hs).comp ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u u_1))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))

The unit of the adjunciton is given by mapping each element to the corresponding constant map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.unit_app (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) (x✝ : Type (max u u_1)) (x : (CategoryTheory.Functor.id (Type (max u u_1))).obj x✝) : (CompHausLike.LocallyConstant.unit P hs).app x✝ x = LocallyConstant.const (↑(CompHausLike.of P PUnit.{u + 1}).toTop) x

noncomputable def CompHausLike.LocallyConstant.unitIso (P : TopCat → Prop) [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) : CategoryTheory.Functor.id (Type (max u w)) ≅ (CompHausLike.LocallyConstant.functor P hs).comp ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))

The unit of the adjunction is an iso.

Equations

• One or more equations did not get rendered due to their size.

theorem CompHausLike.LocallyConstant.adjunction_left_triangle (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] (X : Type (max u w)) : CategoryTheory.CategoryStruct.comp (CompHausLike.LocallyConstant.functorToPresheaves.map ((CompHausLike.LocallyConstant.unit P hs).app X)) ((CompHausLike.LocallyConstant.counit P hs).app ((CompHausLike.LocallyConstant.functor P hs).obj X)).val = CategoryTheory.CategoryStruct.id (CompHausLike.LocallyConstant.functorToPresheaves.obj X)

noncomputable def CompHausLike.LocallyConstant.adjunction (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] : CompHausLike.LocallyConstant.functor P hs ⊣ (CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w))).obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))

CompHausLike.LocallyConstant.functor is left adjoint to the forgetful functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompHausLike.LocallyConstant.adjunction_counit (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] : (CompHausLike.LocallyConstant.adjunction P hs).counit = CompHausLike.LocallyConstant.counit P hs

@[simp]

theorem CompHausLike.LocallyConstant.adjunction_unit (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] : (CompHausLike.LocallyConstant.adjunction P hs).unit = CompHausLike.LocallyConstant.unit P hs

instance CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction (P : TopCat → Prop) [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] [CompHausLike.HasProp P PUnit.{u + 1}] [CompHausLike.HasExplicitFiniteCoproducts P] [CompHausLike.HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑f) [CompHausLike.HasExplicitFiniteCoproducts P] : CategoryTheory.IsIso (CompHausLike.LocallyConstant.adjunction P hs).unit

@[reducible, inline]

abbrev CondensedSet.LocallyConstant.functor : CategoryTheory.Functor (Type (u + 1)) CondensedSet

The functor from sets to condensed sets given by locally constant maps into the set.

Equations

• CondensedSet.LocallyConstant.functor = CompHausLike.LocallyConstant.functor (fun (x : TopCat) => True) CondensedSet.LocallyConstant.functor.proof_1

noncomputable def CondensedSet.LocallyConstant.iso : CondensedSet.LocallyConstant.functor ≅ Condensed.discrete (Type (u + 1))

CondensedSet.LocallyConstant.functor is isomorphic to Condensed.discrete (by uniqueness of adjoints).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CondensedSet.LocallyConstant.functorFullyFaithful : CondensedSet.LocallyConstant.functor.FullyFaithful

CondensedSet.LocallyConstant.functor is fully faithful.

Equations

• CondensedSet.LocallyConstant.functorFullyFaithful = (CompHausLike.LocallyConstant.adjunction (fun (x : TopCat) => True) CondensedSet.LocallyConstant.functor.proof_1).fullyFaithfulLOfIsIsoUnit

instance CondensedSet.LocallyConstant.instFaithfulFunctor : CondensedSet.LocallyConstant.functor.Faithful

instance CondensedSet.LocallyConstant.instFullFunctor : CondensedSet.LocallyConstant.functor.Full

instance CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete : (Condensed.discrete (Type (u_1 + 1))).Faithful

instance CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete : (Condensed.discrete (Type (u_1 + 1))).Full

@[reducible, inline]

abbrev LightCondSet.LocallyConstant.functor : CategoryTheory.Functor (Type u) LightCondSet

The functor from sets to light condensed sets given by locally constant maps into the set.

Equations

• One or more equations did not get rendered due to their size.

instance LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceαTopologicalSpaceSecondCountableTopologySubtypeToTop (S : LightProfinite) (p : ↑S.toTop → Prop) : CompHausLike.HasProp (fun (X : TopCat) => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) (Subtype p)

noncomputable def LightCondSet.LocallyConstant.iso : LightCondSet.LocallyConstant.functor ≅ LightCondensed.discrete (Type u)

LightCondSet.LocallyConstant.functor is isomorphic to LightCondensed.discrete (by uniqueness of adjoints).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LightCondSet.LocallyConstant.functorFullyFaithful : LightCondSet.LocallyConstant.functor.FullyFaithful

LightCondSet.LocallyConstant.functor is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance LightCondSet.LocallyConstant.instFaithfulFunctor : LightCondSet.LocallyConstant.functor.Faithful

instance LightCondSet.LocallyConstant.instFullFunctor : LightCondSet.LocallyConstant.functor.Full

instance LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete : (LightCondensed.discrete (Type u)).Faithful

instance LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete : (LightCondensed.discrete (Type u)).Full