From c78b9a5eac0d06b9e1d8b937e306437f8bbd6bc8 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Mon, 24 Nov 2025 20:53:23 +0100 Subject: [PATCH 1/9] Rewrite yoneda for arbitrary ConcreteCategories with adjoint --- LeanCondensed/LightCondensed/Yoneda.lean | 91 ++++++++++++++---------- 1 file changed, 55 insertions(+), 36 deletions(-) diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index b8fc676..4b61f7f 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -3,74 +3,93 @@ 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 universe u noncomputable section -open CategoryTheory +open CategoryTheory Functor Sheaf + +namespace coherentTopology -namespace LightCondensed +variable {C : Type u} [Category C] [Precoherent C] --- 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 (coherentTopology C)) (Type _)} @[simps! apply] -def yoneda (S : LightProfinite.{u}) (A : LightCondSet) : - (S.toCondensed ⟶ A) ≃ A.val.obj ⟨S⟩ := +def yoneda (A) : + ((coherentTopology C).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⟩) : (coherentTopology C).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 : (coherentTopology C).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 (coherentTopology C) D] + [(coherentTopology C).HasSheafCompose (HasForget.forget (C := D))] + +variable (S S' : C) + +variable (A A' : (Sheaf (coherentTopology C)) D) + +def forget' := sheafCompose (coherentTopology C) (HasForget.forget (C := D)) -abbrev forgetYoneda (S : LightProfinite) (A : LightCondMod R) : - (S.toCondensed ⟶ (forget R).obj A) ≃ A.val.obj ⟨S⟩ := yoneda _ _ +abbrev forgetYoneda : + ((coherentTopology C).yoneda.obj S ⟶ forget'.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 : + (((coherentTopology C).yoneda ⋙ (composeAndSheafify (coherentTopology C) free)).obj S ⟶ A) ≃ ((A.val ⋙ HasForget.forget).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 : (A.val ⋙ HasForget.forget).obj ⟨S⟩) : ((coherentTopology C).yoneda ⋙ composeAndSheafify (coherentTopology C) 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 : ((A.val ⋙ HasForget.forget).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 (coherentTopology C) (HasForget.forget (C := D))).obj A) + (f := (sheafCompose (coherentTopology C) (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 (coherentTopology C) adj) f] rfl -end LightCondensed +end coherentTopology From 807f7def463838a8856eedb19f7018366f360a9f Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Mon, 24 Nov 2025 20:59:13 +0100 Subject: [PATCH 2/9] Remove unnecessary def --- LeanCondensed/LightCondensed/Yoneda.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index 4b61f7f..3f8368f 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -63,7 +63,8 @@ variable (A A' : (Sheaf (coherentTopology C)) D) def forget' := sheafCompose (coherentTopology C) (HasForget.forget (C := D)) abbrev forgetYoneda : - ((coherentTopology C).yoneda.obj S ⟶ forget'.obj A) ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) + ((coherentTopology C).yoneda.obj S ⟶ (sheafCompose (coherentTopology C) (HasForget.forget (C := D))).obj A) + ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) := yoneda _ _ def freeYoneda : From 10d7d851b185272fc1bb2b917a5b67a633f5a65e Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Mon, 24 Nov 2025 21:37:48 +0100 Subject: [PATCH 3/9] Arbitrary subcanonical topology --- LeanCondensed/LightCondensed/Yoneda.lean | 33 ++++++++++++------------ 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index 3f8368f..8298a80 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -6,22 +6,23 @@ Authors: Dagur Asgeirsson import Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves import Mathlib.CategoryTheory.Sites.Adjunction +import Mathlib.CategoryTheory.Sites.Canonical universe u noncomputable section -open CategoryTheory Functor Sheaf +open CategoryTheory Functor Sheaf GrothendieckTopology namespace coherentTopology -variable {C : Type u} [Category C] [Precoherent C] +variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J] -variable (S S' : C) {A A' : (Sheaf (coherentTopology C)) (Type _)} +variable (S S' : C) {A A' : (Sheaf J (Type _))} @[simps! apply] def yoneda (A) : - ((coherentTopology C).yoneda.obj S ⟶ A) ≃ A.val.obj ⟨S⟩ := + (J.yoneda.obj S ⟶ A) ≃ A.val.obj ⟨S⟩ := (fullyFaithfulSheafToPresheaf _ _).homEquiv.trans yonedaEquiv @[simp] @@ -29,7 +30,7 @@ lemma yoneda_symm_apply_val_app (a : A.val.obj ⟨S⟩) (Y : Cᵒᵖ) (f : Y.uno ((yoneda S A).symm a).val.app Y f = A.val.map f.op a := rfl lemma yoneda_symm_naturality {S' : C} (f : S' ⟶ S) - (x : A.val.obj ⟨S⟩) : (coherentTopology C).yoneda.map f ≫ (yoneda S A).symm x = + (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 [Sheaf.comp_val] @@ -47,32 +48,30 @@ lemma yoneda_symm_conaturality (f : A ⟶ A') exact NatTrans.naturality_apply (φ := f.val) (Y := T) _ _ lemma yoneda_conaturality (f : A ⟶ A') - (g : (coherentTopology C).yoneda.obj S ⟶ 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 (coherentTopology C) D] - [(coherentTopology C).HasSheafCompose (HasForget.forget (C := D))] + [HasWeakSheafify J D] + [J.HasSheafCompose (HasForget.forget (C := D))] variable (S S' : C) -variable (A A' : (Sheaf (coherentTopology C)) D) - -def forget' := sheafCompose (coherentTopology C) (HasForget.forget (C := D)) +variable (A A' : (Sheaf J) D) abbrev forgetYoneda : - ((coherentTopology C).yoneda.obj S ⟶ (sheafCompose (coherentTopology C) (HasForget.forget (C := D))).obj A) + (J.yoneda.obj S ⟶ (sheafCompose J (HasForget.forget (C := D))).obj A) ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) := yoneda _ _ def freeYoneda : - (((coherentTopology C).yoneda ⋙ (composeAndSheafify (coherentTopology C) free)).obj S ⟶ A) ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) + ((J.yoneda ⋙ (composeAndSheafify J free)).obj S ⟶ A) ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) := ((adjunction _ adj).homEquiv _ _).trans (yoneda _ _) lemma freeYoneda_symm_naturality {S S'} (f : S' ⟶ S) - (x : (A.val ⋙ HasForget.forget).obj ⟨S⟩) : ((coherentTopology C).yoneda ⋙ composeAndSheafify (coherentTopology C) free).map f ≫ + (x : (A.val ⋙ HasForget.forget).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] @@ -85,12 +84,12 @@ lemma freeYoneda_symm_conaturality (f : A ⟶ A') (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 - (A := (sheafCompose (coherentTopology C) (HasForget.forget (C := D))).obj A) - (f := (sheafCompose (coherentTopology C) (HasForget.forget (C := D))).map f) + (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 (coherentTopology C) adj) f] + erw [Adjunction.counit_naturality (adjunction J adj) f] rfl end coherentTopology From 231b0cd8a09986a22f856796f9ceee6986617d44 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Wed, 26 Nov 2025 15:01:17 +0100 Subject: [PATCH 4/9] Generalize PreservesCoprod --- LeanCondensed/Projects/PreservesCoprod.lean | 71 +++++++++++---------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 9cec2ef..30a9eee 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -5,19 +5,22 @@ Authors: Jonas van der Schaaf -/ import LeanCondensed.LightCondensed.Yoneda import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced +import Mathlib.CategoryTheory.Sites.Canonical import Mathlib.Combinatorics.Quiver.ReflQuiver import Mathlib.Condensed.Light.Explicit -open CategoryTheory Functor Opposite LightProfinite Limits - MonoidalCategory WalkingParallelPair WalkingParallelPairHom - Topology Function +open CategoryTheory Functor Opposite Limits Function GrothendieckTopology universe u +variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J] + [HasFiniteCoproducts C] [∀ X : Sheaf J (Type _), PreservesFiniteProducts X.val] + [HasWeakSheafify J (Type _)] + attribute [local instance] Types.instFunLike Types.instConcreteCategory -instance {n : ℕ} (S : Fin n → LightProfinite.{u}) : - PreservesColimit (Discrete.functor S) lightProfiniteToLightCondSet.{u} := by +instance {n : ℕ} (S : Fin n → C) : + PreservesColimit (Discrete.functor S) J.yoneda := by have : HasColimitsOfSize.{u} (LightCondSet.{u}) := inferInstanceAs (HasColimitsOfSize.{u} (Sheaf _ _)) apply (config := { allowSynthFailures := true}) PreservesCoproduct.of_iso_comparison @@ -26,71 +29,71 @@ instance {n : ℕ} (S : Fin n → LightProfinite.{u}) : 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)) ∘ + let map : (J.yoneda.obj (∐ S) ⟶ X) → ((∐ fun i ↦ J.yoneda.obj (S i)) ⟶ X) := + (inv (piComparison (yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩)) ≫ + (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).inv) ∘ + (Types.productIso (fun i ↦ J.yoneda.obj (S i) ⟶ X)).inv ∘ + (Pi.map (fun i ↦ (Subcanonical.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) + (Types.productIso (fun i ↦ X.val.obj (op (S i)))).hom) ∘ (Subcanonical.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) + · exact Bijective.piMap (fun i ↦ (Subcanonical.yoneda _ _).symm.bijective) · rw [←isIso_iff_bijective]; infer_instance - · exact (LightCondensed.yoneda _ _).bijective + · exact (Subcanonical.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 + (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom ≫ + (piComparison (yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩))) := by apply Bijective.injective rw [←isIso_iff_bijective] infer_instance - suffices ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) = map by + suffices ((coyoneda.map (sigmaComparison J.yoneda 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))] + erw [← coe_comp (f := (inv (piComparison (yoneda.obj X) fun i ↦ ⟨J.yoneda.obj (S i)⟩) ≫ + (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).inv)) + (g := ((yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom ≫ + piComparison (yoneda.obj X) fun i ↦ ⟨J.yoneda.obj (S i)⟩))] 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] + Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, Subcanonical.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) _ + (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩) ≫ + Pi.π (fun i ↦ J.yoneda.obj (S i) ⟶ X) i) + ((opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom.unop ≫ + sigmaComparison J.yoneda S ≫ f) = + ((Types.productIso fun i ↦ J.yoneda.obj (S i) ⟶ X).inv ≫ + Pi.π (fun i ↦ J.yoneda.obj (S i) ⟶ X) i) _ - erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)] + erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩)] 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) ≫ + (Subcanonical.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)) + (Subcanonical.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] + Quiver.Hom.unop_op, ι_comp_sigmaComparison_assoc, ← Subcanonical.yoneda_symm_naturality, + (Subcanonical.yoneda _ _).symm_apply_apply] instance LightProfinite.preservesFiniteCoproductsToLightCondSet : - PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} where + PreservesFiniteCoproducts J.yoneda 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 + exact preservesColimit_of_iso_diagram J.yoneda i.symm } From fcda9d1cc4f2f179fcab7c06e53f3bbf7233b4c7 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Thu, 27 Nov 2025 20:49:05 +0100 Subject: [PATCH 5/9] Fix InternallyProjective.lean --- LeanCondensed/LightCondensed/Yoneda.lean | 13 ++++--- .../Projects/InternallyProjective.lean | 34 +++++++++++++++---- 2 files changed, 34 insertions(+), 13 deletions(-) diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index 8298a80..f28d0d0 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -14,7 +14,7 @@ noncomputable section open CategoryTheory Functor Sheaf GrothendieckTopology -namespace coherentTopology +namespace Subcanonical variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J] @@ -54,8 +54,7 @@ lemma yoneda_conaturality (f : A ⟶ A') 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))] + [HasWeakSheafify J D] [J.HasSheafCompose (HasForget.forget (C := D))] variable (S S' : C) @@ -67,11 +66,11 @@ abbrev forgetYoneda : := yoneda _ _ def freeYoneda : - ((J.yoneda ⋙ (composeAndSheafify J free)).obj S ⟶ A) ≃ ((A.val ⋙ HasForget.forget).obj ⟨S⟩) + ((J.yoneda ⋙ (composeAndSheafify J free)).obj S ⟶ A) ≃ (DD (A.val.obj ⟨S⟩)) := ((adjunction _ adj).homEquiv _ _).trans (yoneda _ _) lemma freeYoneda_symm_naturality {S S'} (f : S' ⟶ S) - (x : (A.val ⋙ HasForget.forget).obj ⟨S⟩) : (J.yoneda ⋙ composeAndSheafify J free).map f ≫ + (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] @@ -80,7 +79,7 @@ lemma freeYoneda_symm_naturality {S S'} (f : S' ⟶ S) rfl lemma freeYoneda_symm_conaturality (f : A ⟶ A') - (x : ((A.val ⋙ HasForget.forget).obj ⟨S⟩)) : + (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 @@ -92,4 +91,4 @@ lemma freeYoneda_symm_conaturality (f : A ⟶ A') erw [Adjunction.counit_naturality (adjunction J adj) f] rfl -end coherentTopology +end Subcanonical diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean index 9486b96..ea165dd 100644 --- a/LeanCondensed/Projects/InternallyProjective.lean +++ b/LeanCondensed/Projects/InternallyProjective.lean @@ -43,7 +43,8 @@ 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 @@ -51,11 +52,12 @@ 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] From b28bbb099d4d465a9eb724e18cc31a284ce9bc8c Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Fri, 28 Nov 2025 11:38:41 +0100 Subject: [PATCH 6/9] Everything works except for size issue --- LeanCondensed/Projects/PreservesCoprod.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 30a9eee..a0362a6 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -4,10 +4,9 @@ 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.CategoryTheory.Sites.Canonical +import Mathlib.CategoryTheory.Sites.Limits import Mathlib.Combinatorics.Quiver.ReflQuiver -import Mathlib.Condensed.Light.Explicit +import Mathlib.Condensed.Light.Functors open CategoryTheory Functor Opposite Limits Function GrothendieckTopology @@ -21,8 +20,6 @@ attribute [local instance] Types.instFunLike Types.instConcreteCategory instance {n : ℕ} (S : Fin n → C) : PreservesColimit (Discrete.functor S) J.yoneda := 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 @@ -90,10 +87,14 @@ instance {n : ℕ} (S : Fin n → C) : Quiver.Hom.unop_op, ι_comp_sigmaComparison_assoc, ← Subcanonical.yoneda_symm_naturality, (Subcanonical.yoneda _ _).symm_apply_apply] -instance LightProfinite.preservesFiniteCoproductsToLightCondSet : +instance Subcanonical.preservesFiniteCoproductsYoneda : PreservesFiniteCoproducts J.yoneda 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 J.yoneda i.symm } + +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet := by + apply (config := { allowSynthFailures := true}) Subcanonical.preservesFiniteCoproductsYoneda + sorry From 1002cd78f4d4a1fee49514d982753ad669f9986b Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Fri, 28 Nov 2025 10:08:13 -0700 Subject: [PATCH 7/9] fix --- LeanCondensed/Projects/PreservesCoprod.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index a0362a6..0fccfdc 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -6,7 +6,9 @@ Authors: Jonas van der Schaaf import LeanCondensed.LightCondensed.Yoneda import Mathlib.CategoryTheory.Sites.Limits import Mathlib.Combinatorics.Quiver.ReflQuiver +import Mathlib.Condensed.Light.Explicit import Mathlib.Condensed.Light.Functors +import Mathlib.Topology.Category.LightProfinite.Limits open CategoryTheory Functor Opposite Limits Function GrothendieckTopology @@ -95,6 +97,8 @@ instance Subcanonical.preservesFiniteCoproductsYoneda : exact preservesColimit_of_iso_diagram J.yoneda i.symm } -instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet := by - apply (config := { allowSynthFailures := true}) Subcanonical.preservesFiniteCoproductsYoneda - sorry +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} := by + have : HasFiniteCoproducts LightProfinite.{u} := + CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts.{u, u} + (P := fun X ↦ TotallyDisconnectedSpace X ∧ SecondCountableTopology X) + apply Subcanonical.preservesFiniteCoproductsYoneda From e016d4118ded56258145fa1e043c9a8ad7ec32c7 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Fri, 5 Dec 2025 14:14:46 -0700 Subject: [PATCH 8/9] golf --- LeanCondensed/Projects/PreservesCoprod.lean | 118 +++++--------------- 1 file changed, 31 insertions(+), 87 deletions(-) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 0fccfdc..4607599 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -3,102 +3,46 @@ 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.Sites.Limits -import Mathlib.Combinatorics.Quiver.ReflQuiver +import Mathlib.CategoryTheory.Sites.Subcanonical import Mathlib.Condensed.Light.Explicit import Mathlib.Condensed.Light.Functors -import Mathlib.Topology.Category.LightProfinite.Limits open CategoryTheory Functor Opposite Limits Function GrothendieckTopology -universe u +universe w v u -variable {C : Type u} [Category C] {J : GrothendieckTopology C} [Subcanonical J] - [HasFiniteCoproducts C] [∀ X : Sheaf J (Type _), PreservesFiniteProducts X.val] - [HasWeakSheafify J (Type _)] - -attribute [local instance] Types.instFunLike Types.instConcreteCategory +variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C} [Subcanonical J] + [∀ X : Sheaf J (Type v), PreservesFiniteProducts X.val] + [HasWeakSheafify J (Type v)] instance {n : ℕ} (S : Fin n → C) : - PreservesColimit (Discrete.functor S) J.yoneda := by - 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 : (J.yoneda.obj (∐ S) ⟶ X) → ((∐ fun i ↦ J.yoneda.obj (S i)) ⟶ X) := - (inv (piComparison (yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩)) ≫ - (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).inv) ∘ - (Types.productIso (fun i ↦ J.yoneda.obj (S i) ⟶ X)).inv ∘ - (Pi.map (fun i ↦ (Subcanonical.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) ∘ (Subcanonical.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 ↦ (Subcanonical.yoneda _ _).symm.bijective) - · rw [←isIso_iff_bijective]; infer_instance - · exact (Subcanonical.yoneda _ _).bijective - - have : Injective ((CategoryTheory.yoneda.obj X).map - (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom ≫ - (piComparison (yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩))) := by - apply Bijective.injective - rw [←isIso_iff_bijective] - infer_instance - - suffices ((coyoneda.map (sigmaComparison J.yoneda 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 ↦ ⟨J.yoneda.obj (S i)⟩) ≫ - (yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).inv)) - (g := ((yoneda.obj X).map (opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom ≫ - piComparison (yoneda.obj X) fun i ↦ ⟨J.yoneda.obj (S i)⟩))] - 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, Subcanonical.yoneda_apply, CategoryTheory.id_apply] - - change - (piComparison - (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩) ≫ - Pi.π (fun i ↦ J.yoneda.obj (S i) ⟶ X) i) - ((opCoproductIsoProduct fun i ↦ J.yoneda.obj (S i)).hom.unop ≫ - sigmaComparison J.yoneda S ≫ f) = - ((Types.productIso fun i ↦ J.yoneda.obj (S i) ⟶ X).inv ≫ - Pi.π (fun i ↦ J.yoneda.obj (S i) ⟶ X) i) _ - - erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨J.yoneda.obj (S i)⟩)] - rw [Types.productIso_inv_comp_π] - simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply] - - change _ = - (Subcanonical.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) - (Subcanonical.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, ← Subcanonical.yoneda_symm_naturality, - (Subcanonical.yoneda _ _).symm_apply_apply] + 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 n := - { preservesColimit {S} := by - let i : S ≅ Discrete.functor (fun i ↦ S.obj ⟨i⟩) := Discrete.natIso (fun _ ↦ Iso.refl _) - exact preservesColimit_of_iso_diagram J.yoneda i.symm - } + 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 : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} := by - have : HasFiniteCoproducts LightProfinite.{u} := - CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts.{u, u} - (P := fun X ↦ TotallyDisconnectedSpace X ∧ SecondCountableTopology X) - apply Subcanonical.preservesFiniteCoproductsYoneda +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} := + Subcanonical.preservesFiniteCoproductsYoneda From 3d57372c2cec1c803936617029b6d5d05a5d5642 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Fri, 5 Dec 2025 14:24:13 -0700 Subject: [PATCH 9/9] . --- LeanCondensed/Projects/PreservesCoprod.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 4607599..657bc8e 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -9,12 +9,13 @@ import Mathlib.Condensed.Light.Functors open CategoryTheory Functor Opposite Limits Function GrothendieckTopology -universe w v u +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