Clean up PreservesCoprod and make it independent on Condensed.yoneda

LeanCondensed/LightCondensed/Yoneda.lean

@@ -3,74 +3,92 @@ Copyright (c) 2025 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.Condensed.Light.Functors
-import Mathlib.Condensed.Light.Module
+
+import Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
+import Mathlib.CategoryTheory.Sites.Adjunction
+import Mathlib.CategoryTheory.Sites.Canonical
 
 universe u
 
 noncomputable section
 
-open CategoryTheory
+open CategoryTheory Functor Sheaf GrothendieckTopology
+
+namespace Subcanonical
 
-namespace LightCondensed
+variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J]
 
--- This should be done for all concrete categories with a left adjoint to types.
-variable (R : Type _) [Ring R]
+variable (S S' : C) {A A' : (Sheaf J (Type _))}
 
 @[simps! apply]
-def yoneda (S : LightProfinite.{u}) (A : LightCondSet) :
-    (S.toCondensed ⟶ A) ≃ A.val.obj ⟨S⟩ :=
+def yoneda (A) :
+    (J.yoneda.obj S ⟶ A) ≃ A.val.obj ⟨S⟩ :=
   (fullyFaithfulSheafToPresheaf _ _).homEquiv.trans yonedaEquiv
 
 @[simp]
-lemma yoneda_symm_apply_val_app (S : LightProfinite) (A : LightCondSet)
-    (a : A.val.obj ⟨S⟩) (Y : LightProfiniteᵒᵖ) (f : Y.unop ⟶ S) :
+lemma yoneda_symm_apply_val_app (a : A.val.obj ⟨S⟩) (Y : Cᵒᵖ) (f : Y.unop ⟶ S) :
       ((yoneda S A).symm a).val.app Y f = A.val.map f.op a := rfl
 
-lemma yoneda_symm_naturality {S S' : LightProfinite} (f : S' ⟶ S) (A : LightCondSet)
-    (x : A.val.obj ⟨S⟩) : lightProfiniteToLightCondSet.map f ≫ (yoneda S A).symm x =
+lemma yoneda_symm_naturality {S' : C} (f : S' ⟶ S)
+    (x : A.val.obj ⟨S⟩) : J.yoneda.map f ≫ (yoneda S A).symm x =
       (yoneda S' A).symm ((A.val.map f.op) x) := by
   apply Sheaf.hom_ext
-  simp only [comp_val]
+  simp only [Sheaf.comp_val]
   ext T y
   simp only [FunctorToTypes.comp, yoneda_symm_apply_val_app, Opposite.op_unop]
   rw [← FunctorToTypes.map_comp_apply (F := A.val)]
   rfl
 
 attribute [local instance] Types.instConcreteCategory Types.instFunLike
-lemma yoneda_symm_conaturality (S : LightProfinite) {A A' : LightCondSet} (f : A ⟶ A')
+lemma yoneda_symm_conaturality (f : A ⟶ A')
     (x : A.val.obj ⟨S⟩) : (yoneda S A).symm x ≫ f = (yoneda S A').symm (f.val.app ⟨S⟩ x) := by
   apply Sheaf.hom_ext
-  simp only [comp_val]
+  simp only [Sheaf.comp_val]
   ext T y
   exact NatTrans.naturality_apply (φ := f.val) (Y := T) _ _
 
-lemma yoneda_conaturality (S : LightProfinite) {A A' : LightCondSet} (f : A ⟶ A')
-    (g : S.toCondensed ⟶ A) : f.val.app ⟨S⟩ (yoneda S A g) = yoneda S A' (g ≫ f) := rfl
+lemma yoneda_conaturality (f : A ⟶ A')
+    (g : J.yoneda.obj S ⟶ A)
+  : f.val.app ⟨S⟩ (yoneda S A g) = yoneda S A' (g ≫ f) := rfl
+
+variable {D : Type*} [Category D] {FD : D → D → Type*} {DD : D → Type*}
+  [∀ X Y, FunLike (FD X Y) (DD X) (DD Y)] [ConcreteCategory D FD]
+  {free : Type _ ⥤ D} (adj : free ⊣ HasForget.forget)
+  [HasWeakSheafify J D] [J.HasSheafCompose (HasForget.forget (C := D))]
+
+variable (S S' : C)
+
+variable (A A' : (Sheaf J) D)
 
-abbrev forgetYoneda (S : LightProfinite) (A : LightCondMod R) :
-    (S.toCondensed ⟶ (forget R).obj A) ≃ A.val.obj ⟨S⟩ := yoneda _ _
+abbrev forgetYoneda :
+    (J.yoneda.obj S ⟶ (sheafCompose J (HasForget.forget (C := D))).obj A)
+      ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩)
+  := yoneda _ _
 
-def freeYoneda (S : LightProfinite) (A : LightCondMod R) :
-    ((free R).obj S.toCondensed ⟶ A) ≃ A.val.obj ⟨S⟩ :=
-  ((freeForgetAdjunction R).homEquiv _ _).trans (yoneda _ _)
+def freeYoneda :
+    ((J.yoneda ⋙ (composeAndSheafify J free)).obj S ⟶ A) ≃ (DD (A.val.obj ⟨S⟩))
+  := ((adjunction _ adj).homEquiv _ _).trans (yoneda _ _)
 
-lemma freeYoneda_symm_naturality {S S' : LightProfinite} (f : S' ⟶ S) (A : LightCondMod R)
-    (x : A.val.obj ⟨S⟩) : (lightProfiniteToLightCondSet ⋙ free R).map f ≫
-      (freeYoneda R S A).symm x = (freeYoneda R S' A).symm ((A.val.map f.op) x) := by
-  simp only [Functor.comp_obj, Functor.comp_map, freeYoneda, Equiv.symm_trans_apply,
-    Adjunction.homEquiv_counit]
-  simp only [← Category.assoc, ← Functor.map_comp]
-  erw [yoneda_symm_naturality]
+lemma freeYoneda_symm_naturality {S S'} (f : S' ⟶ S)
+    (x : DD (A.val.obj ⟨S⟩)) : (J.yoneda ⋙ composeAndSheafify J free).map f ≫
+      (freeYoneda adj S A).symm x = (freeYoneda adj S' A).symm ((A.val.map f.op) x) := by
+  simp only [Functor.comp_obj, freeYoneda, Equiv.symm_trans_apply]
+  erw [Adjunction.homEquiv_counit, Adjunction.homEquiv_counit]
+  simp only [← Category.assoc]
+  erw [←Functor.map_comp (composeAndSheafify _ _), yoneda_symm_naturality]
   rfl
 
-lemma freeYoneda_symm_conaturality (S : LightProfinite) {A A' : LightCondMod R} (f : A ⟶ A')
-    (x : A.val.obj ⟨S⟩) :
-    (freeYoneda R S A).symm x ≫ f = (freeYoneda R S A').symm (f.val.app ⟨S⟩ x) := by
+lemma freeYoneda_symm_conaturality (f : A ⟶ A')
+    (x : DD (A.val.obj ⟨S⟩)) :
+    (freeYoneda adj S A).symm x ≫ f = (freeYoneda adj S A').symm (f.val.app ⟨S⟩ x) := by
   simp only [freeYoneda, Equiv.symm_trans_apply]
-  erw [← yoneda_symm_conaturality (S := S) (A' := (forget R).obj A') (f := (forget R).map f)]
-  simp only [Adjunction.homEquiv_counit, Functor.id_obj, Category.assoc, Functor.map_comp,
-    Adjunction.counit_naturality, Functor.comp_obj]
+  erw [←yoneda_symm_conaturality S
+    (A := (sheafCompose J (HasForget.forget (C := D))).obj A)
+    (f := (sheafCompose J (HasForget.forget (C := D))).map f)
+  ]
+  erw [Adjunction.homEquiv_counit, Adjunction.homEquiv_counit]
+  simp only [Category.assoc, Functor.comp_obj, Functor.map_comp]
+  erw [Adjunction.counit_naturality (adjunction J adj) f]
   rfl
 
-end LightCondensed
+end Subcanonical

LeanCondensed/Projects/InternallyProjective.lean

@@ -43,19 +43,21 @@ theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X) :
 
 end InternallyProjective
 
-open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed
+open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory
+  MonoidalClosed Subcanonical Functor
 
 section Condensed
 
 attribute [local instance] Types.instConcreteCategory Types.instFunLike
 
 variable (R : Type u) [CommRing R]
 
-variable (A : LightCondMod R) (S : LightProfinite)
+instance : (coherentTopology LightProfinite).HasSheafCompose (forget (ModuleCat.{u} R)) :=
+  hasSheafCompose_of_preservesLimitsOfSize _
 
 def ihomPoints (A B : LightCondMod.{u} R) (S : LightProfinite) :
     ((ihom A).obj B).val.obj ⟨S⟩ ≃ ((A ⊗ ((free R).obj S.toCondensed)) ⟶ B) :=
-  (LightCondensed.freeYoneda _ _ _).symm.trans ((ihom.adjunction A).homEquiv _ _).symm
+  (freeYoneda (ModuleCat.adj.{u} R) _ _).symm.trans ((ihom.adjunction A).homEquiv _ _).symm
 -- We have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`,
 -- and this could be made an `≅`. But it's not needed in this proof.
 
@@ -67,12 +69,29 @@ lemma ihom_map_val_app (A B P : LightCondMod.{u} R) (S : LightProfinite) (e : A
         (ihomPoints R P B S).symm (ihomPoints R P A S x ≫ e) := by
   intro x
   apply (ihomPoints R P B S).injective
-  simp only [ihomPoints, freeYoneda, curriedTensor_obj_obj, Equiv.trans_apply,
+  simp only [ihomPoints, freeYoneda]
+  change ((((freeForgetAdjunction R).homEquiv S.toCondensed _).trans
+            (Subcanonical.yoneda S ((LightCondensed.forget R).obj _))).symm.trans
+      ((ihom.adjunction P).homEquiv _ _).symm)
+    ((ConcreteCategory.hom (((ihom P).map e).val.app (Opposite.op S))) x) =
+  ((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj B)).trans
+            (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj B)))).symm.trans
+      ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) B).symm)
+    (((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj B)).trans
+                (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj B)))).symm.trans
+          ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) B).symm).symm
+      (((((freeForgetAdjunction R).homEquiv S.toCondensed ((ihom P).obj A)).trans
+                  (Subcanonical.yoneda S ((LightCondensed.forget R).obj ((ihom P).obj A)))).symm.trans
+            ((ihom.adjunction P).homEquiv ((free R).obj S.toCondensed) A).symm)
+          x ≫
+        e))
+  simp only [curriedTensor_obj_obj, Equiv.trans_apply,
     Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.symm_apply_apply]
   erw [← Adjunction.homEquiv_naturality_right_symm]
   erw [← Adjunction.homEquiv_naturality_right_symm]
-  simp only [LightCondensed.yoneda, sheafToPresheaf_obj, Equiv.symm_trans_apply,
+  simp only [Subcanonical.yoneda, sheafToPresheaf_obj, Equiv.symm_trans_apply,
     curriedTensor_obj_obj, EmbeddingLike.apply_eq_iff_eq]
+  change (fullyFaithfulSheafToPresheaf _ _).homEquiv.symm _ = _ ≫ _
   apply (fullyFaithfulSheafToPresheaf _ _).map_injective
   erw [Functor.FullyFaithful.homEquiv_symm_apply, Functor.FullyFaithful.homEquiv_symm_apply]
   ext
@@ -84,7 +103,10 @@ lemma ihomPoints_symm_comp (B P : LightCondMod.{u} R) (S S' : LightProfinite) (
     (ihomPoints R P B S).symm (P ◁ (free R).map (lightProfiniteToLightCondSet.map π) ≫ f) =
       ConcreteCategory.hom (((ihom P).obj B).val.map π.op) ((ihomPoints R P B S').symm f) := by
   simp only [ihomPoints, Equiv.symm_trans_apply, Equiv.symm_symm]
-  simp only [freeYoneda, LightCondensed.yoneda, sheafToPresheaf_obj, Equiv.trans_apply]
+  simp only [freeYoneda, Subcanonical.yoneda, sheafToPresheaf_obj, Equiv.trans_apply]
+  change ((fullyFaithfulSheafToPresheaf _ _).homEquiv.trans _)
+    (((freeForgetAdjunction R).homEquiv _ _)
+      (((ihom.adjunction P).homEquiv _ _) _)) = _
   erw [Adjunction.homEquiv_apply, Adjunction.homEquiv_apply, Adjunction.homEquiv_apply,
     Adjunction.homEquiv_apply]
   simp only [Functor.comp_obj, ihom.ihom_adjunction_unit, Functor.map_comp]

LeanCondensed/Projects/PreservesCoprod.lean

@@ -3,94 +3,47 @@ Copyright (c) 2025 Jonas van der Schaaf. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jonas van der Schaaf
 -/
-import LeanCondensed.LightCondensed.Yoneda
-import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
-import Mathlib.Combinatorics.Quiver.ReflQuiver
+import Mathlib.CategoryTheory.Sites.Subcanonical
 import Mathlib.Condensed.Light.Explicit
-
-open CategoryTheory Functor Opposite LightProfinite Limits
-  MonoidalCategory WalkingParallelPair WalkingParallelPairHom
-  Topology Function
-
-universe u
+import Mathlib.Condensed.Light.Functors
+
+open CategoryTheory Functor Opposite Limits Function GrothendieckTopology
+
+universe v u
+
+variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C} [Subcanonical J]
+  [∀ X : Sheaf J (Type v), PreservesFiniteProducts X.val]
+  [HasWeakSheafify J (Type v)]
+
+-- TODO: more general version for `yonedaULift`
+instance {n : ℕ} (S : Fin n → C) :
+    PreservesColimit (Discrete.functor S) J.yoneda where
+  preserves {c} hc := ⟨by
+    suffices IsLimit (coyoneda.mapCone (J.yoneda.mapCocone c).op) from
+      isColimitOfOp (isLimitOfReflects _ this)
+    apply evaluationJointlyReflectsLimits
+    intro X
+    let i : (J.yoneda.op ⋙ coyoneda ⋙
+        ((evaluation (Sheaf J (Type v)) (Type (max u v))).obj X)) ≅ X.val ⋙ uliftFunctor := by
+      refine NatIso.ofComponents (fun Y ↦ equivEquivIso (J.yonedaEquiv.trans Equiv.ulift.symm)) ?_
+      intro Y Z f
+      dsimp
+      ext a
+      change _ = (a.val.app Y ≫ X.val.map f) _
+      rw [← a.val.naturality]
+      dsimp [-sheafToPresheaf_obj, GrothendieckTopology.yonedaEquiv, CategoryTheory.yonedaEquiv]
+      simp
+    suffices IsLimit ((X.val ⋙ uliftFunctor).mapCone c.op) from IsLimit.mapConeEquiv i.symm this
+    have := preservesLimitsOfShape_of_equiv (Discrete.opposite (Fin n)).symm X.val
+    exact isLimitOfPreserves _ hc.op⟩
+
+instance Subcanonical.preservesFiniteCoproductsYoneda :
+    PreservesFiniteCoproducts J.yoneda where
+  preserves _ := { preservesColimit {S} :=
+    let i : S ≅ Discrete.functor (fun i ↦ S.obj ⟨i⟩) := Discrete.natIso (fun _ ↦ Iso.refl _)
+    preservesColimit_of_iso_diagram J.yoneda i.symm }
 
 attribute [local instance] Types.instFunLike Types.instConcreteCategory
 
-instance {n : ℕ} (S : Fin n → LightProfinite.{u}) :
-    PreservesColimit (Discrete.functor S) lightProfiniteToLightCondSet.{u} := by
-  have : HasColimitsOfSize.{u} (LightCondSet.{u}) :=
-    inferInstanceAs (HasColimitsOfSize.{u} (Sheaf _ _))
-  apply (config := { allowSynthFailures := true}) PreservesCoproduct.of_iso_comparison
-  rw [isIso_iff_isIso_coyoneda_map]
-  intro X
-  rw [isIso_iff_bijective]
-  have := instIsIsoPiComparison X.val (fun i ↦ ⟨S i⟩)
-
-  let map : ((∐ S).toCondensed ⟶ X) → ((∐ fun i ↦ (S i).toCondensed) ⟶ X) :=
-    (inv (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)) ≫
-      (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv) ∘
-      (Types.productIso (fun i ↦ (S i).toCondensed ⟶ X)).inv ∘
-      (Pi.map (fun i ↦ (LightCondensed.yoneda (S i) X).symm)) ∘
-      ((X.val.mapIso (opCoproductIsoProduct S)).hom ≫ (piComparison X.val (fun i ↦ ⟨S i⟩)) ≫
-        (Types.productIso (fun i ↦ X.val.obj (op (S i)))).hom) ∘ (LightCondensed.yoneda (∐ S) X)
-
-  have map_bij : Bijective map := by
-    refine Bijective.comp ?_ (Bijective.comp ?_ (Bijective.comp ?_ (Bijective.comp ?_ ?_)))
-    repeat {rw [←isIso_iff_bijective]; infer_instance}
-    · exact Bijective.piMap (fun i ↦ (LightCondensed.yoneda _ _).symm.bijective)
-    · rw [←isIso_iff_bijective]; infer_instance
-    · exact (LightCondensed.yoneda _ _).bijective
-
-  have : Injective ((CategoryTheory.yoneda.obj X).map
-    (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom ≫
-      (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩))) := by
-    apply Bijective.injective
-    rw [←isIso_iff_bijective]
-    infer_instance
-
-  suffices ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) = map by
-    rw [this]
-    exact map_bij
-
-  apply this.comp_left
-  simp only [mapIso_hom, map]
-  rw [← Function.comp_assoc]
-  erw [← coe_comp (f := (inv (piComparison (yoneda.obj X) fun i ↦ op (S i).toCondensed) ≫
-    (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv))
-    (g := ((yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom ≫
-      piComparison (yoneda.obj X) fun i ↦ op (S i).toCondensed))]
-  ext1 f
-  ext1 ⟨i⟩
-  simp only [yoneda_obj_obj, Discrete.functor_obj_eq_as, coyoneda_obj_obj, Function.comp_apply,
-    coyoneda_map_app, Quiver.Hom.unop_op, types_comp_apply, yoneda_obj_map, Category.assoc,
-    Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, LightCondensed.yoneda_apply, CategoryTheory.id_apply]
-
-  change
-    (piComparison
-      (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩) ≫
-        Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i)
-      ((opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom.unop ≫
-        sigmaComparison lightProfiniteToLightCondSet S ≫ f) =
-    ((Types.productIso fun i ↦ (S i).toCondensed ⟶ X).inv ≫
-      Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i) _
-
-  erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)]
-  rw [Types.productIso_inv_comp_π]
-  simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply]
-
-  change _ =
-    (LightCondensed.yoneda (S i) X).symm (((X.val.map (opCoproductIsoProduct S).hom) ≫
-      piComparison X.val (fun i ↦ ⟨S i⟩) ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i)
-      (LightCondensed.yoneda (∐ S) X f))
-  rw [piComparison_comp_π, ← X.val.map_comp, opCoproductIsoProduct_hom_comp_π,
-    yoneda_obj_map, ← unop_comp_assoc, opCoproductIsoProduct_hom_comp_π,
-    Quiver.Hom.unop_op, ι_comp_sigmaComparison_assoc, ← LightCondensed.yoneda_symm_naturality,
-    (LightCondensed.yoneda _ _).symm_apply_apply]
-
-instance LightProfinite.preservesFiniteCoproductsToLightCondSet :
-    PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} where
-  preserves n :=
-    { preservesColimit {S} := by
-        let i : S ≅ Discrete.functor (fun i ↦ S.obj ⟨i⟩) := Discrete.natIso (fun _ ↦ Iso.refl _)
-        exact preservesColimit_of_iso_diagram lightProfiniteToLightCondSet i.symm
-    }
+instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} :=
+  Subcanonical.preservesFiniteCoproductsYoneda