add some examples

dagurtomas · Jun 15, 2024 · dc05203 · dc05203
1 parent f172018
commit dc05203
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/LeanCondensed/LightCondensed/Small.lean b/LeanCondensed/LightCondensed/Small.lean
@@ -1,5 +1,5 @@
 import Mathlib.CategoryTheory.Sites.Coherent.Equivalence
-import Mathlib.Condensed.Light.Basic
+import Mathlib.Condensed.Light.Module
 
 universe v u w
 
@@ -13,6 +13,12 @@ instance : LocallySmall.{max v w} (LightCondensed.{w} C) := by
   erw [locallySmall_congr ((equivSmallModel LightProfinite.{w}).sheafCongrPrecoherent C)]
   infer_instance
 
-example (A B : LightCondensed.{w} C) : Small.{max v w} (A ⟶ B) := LocallySmall.hom_small A B
+example (A B : LightCondensed.{w} C) : Small.{max v w} (A ⟶ B) := inferInstance
+
+example : LocallySmall.{u} LightCondSet.{u} := inferInstance
+
+example (R : Type) [Ring R] : LocallySmall.{0} (LightCondMod R) := inferInstance
+
+example : LocallySmall.{0} LightCondAb := inferInstance
 
 end LightCondensed