Regression in `Functor.preimageIso`

Stream: mathlib4

[Dagur Asgeirsson]

Before #12449 was merged, the last sorry in

import Mathlib.Condensed.TopComparison

universe u

open CategoryTheory

namespace Condensed.LocallyConstant

/--
The functor from the category of sets to presheaves on `CompHaus` given by locally constant maps.
-/
@[simps]
def functorToPresheaves : Type* ⥤ (CompHaus.{u}ᵒᵖ ⥤ Type _) where
  obj X := {
    obj := fun ⟨S⟩ ↦ LocallyConstant S X
    map := fun f g ↦ g.comap f.unop }
  map f := { app := fun S t ↦ t.map f }

/--
Locally constant maps are the same as continuous maps when the target is equipped with the discrete
topology
-/
@[simps]
def locallyConstantIsoContinuousMap (Y X : Type*) [TopologicalSpace Y] :
    LocallyConstant Y X ≅ C(Y, TopCat.discrete.obj X) :=
  letI : TopologicalSpace X := ⊥
  haveI : DiscreteTopology X := ⟨rfl⟩
  { hom := fun f ↦ (f : C(Y, X))
    inv := fun f ↦ ⟨f, (IsLocallyConstant.iff_continuous f).mpr f.2⟩ }

/-- `locallyConstantIsoContinuousMap` is a natural isomorphism. -/
noncomputable def functorToPresheavesIsoTopCatToCondensed (X : Type (u+1)) :
    functorToPresheaves.obj X ≅ (topCatToCondensed.obj (TopCat.discrete.obj X)).val :=
  NatIso.ofComponents (fun S ↦ locallyConstantIsoContinuousMap _ _)

/-- `Condensed.LocallyConstant.functorToPresheaves` lands in condensed sets. -/
@[simps]
def functor : Type (u+1) ⥤ CondensedSet.{u} where
  obj X := {
    val := functorToPresheaves.obj X
    cond := by
      rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIsoTopCatToCondensed X)]
      exact (topCatToCondensed.obj _).cond
  }
  map f := ⟨functorToPresheaves.map f⟩

/--
`Condensed.LocallyConstant.functor` is naturally isomorphic to the restriction of
`topCatToCondensed` to discrete topological spaces.
-/
noncomputable def functorIsoTopCatToCondensed : functor ≅ TopCat.discrete ⋙ topCatToCondensed := by
  refine NatIso.ofComponents (fun X ↦ (sheafToPresheaf _ _).preimageIso
    (functorToPresheavesIsoTopCatToCondensed X)) sorry

was completed by automation, but not anymore, now that Functor.preimage is defined by Exists.choose. How are we supposed to work with full functors where there is a "preferred" preimage? There is an easy workaround that I could use here, just define something like Sheaf.isoEquiv analogous to Sheaf.homEquiv that I think Joël added in this PR. But shouldn't we have more general API to work with this type of "canonically fully faithful" functors / actual inclusion functors?

[Dagur Asgeirsson]

Maybe this is just lean having problems unifying f.val with (sheafToPresheaf _ _).map f, but I wonder what caused automation to break...

[Andrew Yang]

Maybe we can add a type-valued FullyFaithful structure that is not a class? Are there any full functors that are not faithful but have a "preferred preimage"?
cc @Joël Riou

[Joël Riou]

I think the most reasonable fix is to define Sheaf.isoEquiv.

[Andrew Yang]

Yeah but you needed to add plenty of such definitions throughout the refactor for yoneda and SheafedSpace.toPresheafedSpace etc, and defining a separate isoEquiv for each fully faithful embedding we have isn't scalable IMHO.

[Joël Riou]

I do not mind if someone makes the effort of developing this FullyFaithful API! Then, presumably, given data : F.FullyFaithful, we would define data.homEquiv, data.isoEquiv, and once these data are defined for (yoneda/sheaves/SheafedSpace), Sheaf.homEquiv should be defined as an abbreviation for data.homEquiv, etc.

The API should also contain, FullyFaithful.whisker: if F is fully faithful, the postcomposition with F is also fully faithful. Then, we could get coyoneda.preimageNatTrans and coyoneda.preimageNatIso.