Merge remote-tracking branch 'origin/freecondab' into jon/closed_symm…

…_mon

CategoryTheoryExercises/Exercises/Exercise5.lean

@@ -1,12 +1,11 @@
 import Mathlib.CategoryTheory.Preadditive.Basic
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 set_option autoImplicit false
 /-!
-We prove that biproducts (direct sums) are preserved by any preadditive functor.
-
-This result is not in mathlib, so full marks for the exercise are only
-achievable if you contribute to a pull request! :-)
+We prove that binary and finite biproducts (direct sums) are preserved by any 
+additive functor.
 -/
 
 noncomputable section
@@ -17,36 +16,31 @@ open CategoryTheory.Limits
 namespace CategoryTheory
 
 universe u v
--- porting note: was Preadditive but stupid structure below breaks it!
-variable {C : Type u} [Category C] [CategoryTheory.Preadditive C]
-variable {D : Type v} [Category D] [CategoryTheory.Preadditive D]
 
-/-!
-In fact, no one has gotten around to defining preadditive functors,
-so I'll help you out by doing that first.
--/
-
-structure Functor.Preadditive (F : C ⥤ D) : Prop :=
-(map_zero : ∀ X Y, F.map (0 : X ⟶ Y) = 0)
-(map_add : ∀ {X Y} (f g : X ⟶ Y), F.map (f + g) = F.map f + F.map g)
+variable {C : Type u} [Category C] [Preadditive C]
+variable {D : Type v} [Category D] [Preadditive D]
 
 variable [HasBinaryBiproducts C] [HasBinaryBiproducts D]
 
-def Functor.Preadditive.preserves_biproducts (F : C ⥤ D) (P : F.Preadditive) (X Y : C) :
-    F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y :=
-  sorry
+def Functor.Additive.preservesBinaryBiproducts (F : C ⥤ D) [Additive F] (X Y : C) :
+  F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y := sorry
 
-/-!
-There are some further hints in
-`hints/category_theory/exercise5/`
--/
-
--- Challenge problem:
+-- Variant:
 -- In fact one could prove a better result,
 -- not requiring chosen biproducts in D,
 -- asserting that `F.obj (X ⊞ Y)` is a biproduct of `F.obj X` and `F.obj Y`.
 
+-- Note that the version for all finite biproducts is already in mathlib!
+example (F : C ⥤ D) [F.Additive] :
+  PreservesFiniteBiproducts F := inferInstance
+
+-- but the below is missing!
+
+instance (F : C ⥤ D) [F.Additive] :
+  PreservesBinaryBiproducts F := sorry -- `inferInstance` fails!
 
-end CategoryTheory
+example (F : C ⥤ D) [F.Additive] (X Y : C) :
+  F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y := 
+Functor.mapBiprod F X Y -- works given the instance above
 
-end section
+end CategoryTheory

CategoryTheoryExercises/Solutions/Solution5.lean

@@ -1,12 +1,11 @@
 import Mathlib.CategoryTheory.Preadditive.Basic
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 set_option autoImplicit false
 /-!
-We prove that biproducts (direct sums) are preserved by any preadditive functor.
-
-This result is not in mathlib, so full marks for the exercise are only
-achievable if you contribute to a pull request! :-)
+We prove that binary and finite biproducts (direct sums) are preserved by any 
+additive functor.
 -/
 
 noncomputable section
@@ -17,44 +16,55 @@ open CategoryTheory.Limits
 namespace CategoryTheory
 
 universe u v
--- porting note: was Preadditive but stupid structure below breaks it!
-variable {C : Type u} [Category C] [CategoryTheory.Preadditive C]
-variable {D : Type v} [Category D] [CategoryTheory.Preadditive D]
 
-/-!
-In fact, no one has gotten around to defining preadditive functors,
-so I'll help you out by doing that first.
--/
-
-structure Functor.Preadditive (F : C ⥤ D) : Prop :=
-(map_zero : ∀ X Y, F.map (0 : X ⟶ Y) = 0)
-(map_add : ∀ {X Y} (f g : X ⟶ Y), F.map (f + g) = F.map f + F.map g)
+variable {C : Type u} [Category C] [Preadditive C]
+variable {D : Type v} [Category D] [Preadditive D]
 
 variable [HasBinaryBiproducts C] [HasBinaryBiproducts D]
 
-def Functor.Preadditive.preserves_biproducts (F : C ⥤ D) (P : F.Preadditive) (X Y : C) :
+def Functor.Additive.preservesBinaryBiproducts (F : C ⥤ D) [Additive F] (X Y : C) :
   F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y where
     hom := (F.map biprod.fst) ≫ biprod.inl + F.map biprod.snd ≫ biprod.inr
     inv := biprod.fst ≫ F.map biprod.inl + biprod.snd ≫ F.map biprod.inr
     hom_inv_id := by
       simp
-      sorry
+      rw [← F.map_comp, ← F.map_comp]
+      rw [← map_add]
+      simp
       done
     inv_hom_id := by
       simp
-      sorry
+      rw [← Category.assoc (F.map biprod.inl), ← F.map_comp]
+      simp
+      rw [← Category.assoc (F.map biprod.inr), ← F.map_comp]
+      simp
+      rw [← Category.assoc (F.map biprod.inl), ← F.map_comp]
+      simp
+      rw [← Category.assoc (F.map biprod.inr), ← F.map_comp]
+      simp
       done
 
-/-!
-There are some further hints in
-`hints/category_theory/exercise5/`
--/
-
 -- Challenge problem:
 -- In fact one could prove a better result,
 -- not requiring chosen biproducts in D,
 -- asserting that `F.obj (X ⊞ Y)` is a biproduct of `F.obj X` and `F.obj Y`.
 
+def Functor.Additive.preservesFiniteBiproducts (F : C ⥤ D) [Additive F] :
+  PreservesFiniteBiproducts F := inferInstance
+
+example (F : C ⥤ D) [F.Additive] :
+  PreservesFiniteBiproducts F := inferInstance
+
+variable (F : C ⥤ D) [F.Additive] in
+#synth PreservesFiniteBiproducts F 
+
+variable (F : C ⥤ D) [F.Additive] in
+#synth PreservesBinaryBiproducts F -- oops!
+
+def Functor.Additive.preservesBinaryBiproducts' (F : C ⥤ D) [Additive F] (X Y : C) :
+  F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y := 
+  mapBiprod F X Y
+
 
 end CategoryTheory
 

Condensed/AB5.lean

@@ -0,0 +1,187 @@
+import Condensed.Equivalence
+import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
+import Mathlib.CategoryTheory.Abelian.Basic
+import Mathlib.Algebra.Category.GroupCat.Abelian
+import Mathlib.Algebra.Category.GroupCat.FilteredColimits
+import Mathlib.Algebra.Category.GroupCat.Limits
+import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.Condensed.Abelian
+import Mathlib.CategoryTheory.Limits.Filtered
+
+/-!
+
+# `Condensed Ab` has AB5
+
+- Recall AB3, AB4, AB5:
+[https://stacks.math.columbia.edu/tag/079A](Stacks 079A)
+
+- How should we formulate this in lean?
+
+- Review proof that `Condensed Ab` has AB5 (on the board) 
+
+- Start the skeleton for this assertion in Lean.
+
+-/
+
+universe v u
+
+open CategoryTheory Limits
+
+#check CondensedAb.{u}
+
+variable (A B : Type u) 
+  [Category.{v} A] [Abelian A]
+  [Category.{v} B] [Abelian B]
+  (F : A ⥤ B) [F.Additive]
+
+-- AB3
+
+example [HasColimits A] : HasCoproducts A := inferInstance
+
+example [HasCoproducts A] : HasColimits A := 
+  by exact has_colimits_of_hasCoequalizers_and_coproducts
+
+noncomputable
+example [PreservesFiniteLimits F] (X Y : A) 
+    (f : X ⟶ Y) : PreservesLimit (parallelPair f 0) F := 
+  inferInstance
+
+noncomputable
+example [∀ {X Y : A} (f : X ⟶ Y), 
+    PreservesLimit (parallelPair f 0) F] : PreservesFiniteLimits F :=
+  by exact Functor.preservesFiniteLimitsOfPreservesKernels F
+
+noncomputable
+example [∀ {X Y : A} (f : X ⟶ Y), 
+    PreservesColimit (parallelPair f 0) F] : PreservesFiniteColimits F :=
+  by exact Functor.preservesFiniteColimitsOfPreservesCokernels F
+
+abbrev AB4 (A : Type u) [Category.{v} A] 
+    [HasCoproducts A] := 
+    ∀ (α : Type v), PreservesFiniteLimits 
+      (colim : (Discrete α ⥤ A) ⥤ A)
+
+example [HasCoproducts A] 
+  [∀ α : Type v, PreservesFiniteLimits 
+    (colim (J := Discrete α) (C := A))] : AB4 A := inferInstance
+
+abbrev AB5 (A : Type u) [Category.{v} A] 
+    [HasFilteredColimitsOfSize.{v} A] :=
+    ∀ (J : Type v) [SmallCategory J] [IsFiltered J],
+      PreservesFiniteLimits (colim (J := J) (C := A))
+
+noncomputable
+example (A : Type u) [Category.{v} A] 
+    (J : Type v) [SmallCategory J] [HasColimitsOfShape J A] :
+    PreservesColimits (colim (J := J) (C := A)) := 
+  colimConstAdj.leftAdjointPreservesColimits
+
+
+
+-- Condensed Mathematics
+
+#check CondensedAb
+
+noncomputable section
+
+example : Abelian CondensedAb := inferInstance
+
+example : Sheaf (coherentTopology ExtrDisc.{u}) AddCommGroupCat.{u+1} ≌ CondensedAb := 
+  Condensed.ExtrDiscCompHaus.equivalence _
+
+set_option pp.universes true
+example : Abelian (Sheaf (coherentTopology ExtrDisc.{u}) AddCommGroupCat.{u+1}) := 
+  letI : PreservesLimits (forget AddCommGroupCat.{u+1}) :=
+    AddCommGroupCat.forgetPreservesLimits.{u+1, u+1}
+  CategoryTheory.sheafIsAbelian
+
+example : 
+  Functor.Additive 
+    (Condensed.ExtrDiscCompHaus.equivalence AddCommGroupCat).inverse := by
+  constructor
+  aesop_cat
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+/-
+
+
+open CategoryTheory Limits
+
+universe v u
+
+example : HasColimits (CondensedAb.{u}) := 
+  letI : PreservesLimits (forget AddCommGroupCat.{u+1}) :=
+    AddCommGroupCat.forgetPreservesLimits.{u+1, u+1}
+  show HasColimits (Sheaf _ _) from inferInstance
+  --CategoryTheory.Sheaf.instHasColimitsSheafInstCategorySheaf 
+
+example : HasLimits (CondensedAb.{u}) := 
+  --letI : PreservesLimits (forget AddCommGroupCat.{u+1}) :=
+  --  AddCommGroupCat.forgetPreservesLimits.{u+1, u+1}
+  show HasLimits (Sheaf _ _) from inferInstance
+
+noncomputable
+example : Sheaf (coherentTopology ExtrDisc.{u}) AddCommGroupCat.{u+1} ≌ CondensedAb.{u} := 
+  Condensed.ExtrDiscCompHaus.equivalence AddCommGroupCat.{u+1}
+
+example (A : Type u) [Category.{v} A] [Abelian A] 
+    [HasCoproducts A] : HasColimits A := 
+  has_colimits_of_hasCoequalizers_and_coproducts
+
+noncomputable
+example (J : Type v) [SmallCategory J] (C D : Type u) 
+    [Category.{v} C] [Category.{v} D] (e : C ≌ D)
+    [HasColimits C] [HasColimits D]
+    [PreservesLimits (colim : (J ⥤ C) ⥤ C)] :
+    PreservesLimits (colim : (J ⥤ D) ⥤ D) := 
+  let e₁ : (J ⥤ D) ≌ (J ⥤ C) := sorry 
+  let e₂ : e₁.functor ⋙ colim ⋙ e.functor ≅ colim := sorry
+  preservesLimitsOfNatIso e₂
+
+noncomputable
+example (J : Type v) [SmallCategory J] 
+    (C : Type u) [Category.{v} C]
+    [HasColimitsOfShape J C] :
+    PreservesColimits (colim : (J ⥤ C) ⥤ C) := 
+  Adjunction.leftAdjointPreservesColimits colimConstAdj   
+
+noncomputable
+example {A B : Type u} [Category.{v} A] [Category.{v} B] 
+    (F : A ⥤ B) [Abelian A] [Abelian B] [F.Additive] 
+    [∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] : 
+    PreservesFiniteLimits F := 
+  Functor.preservesFiniteLimitsOfPreservesKernels F
+
+noncomputable
+example {A B : Type u} [Category.{v} A] [Category.{v} B] 
+    (F : A ⥤ B) [Abelian A] [Abelian B] [F.Additive] 
+    [∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] : 
+    PreservesFiniteColimits F := 
+  Functor.preservesFiniteColimitsOfPreservesCokernels F
+
+-/

Condensed/Equivalence.lean

@@ -10,6 +10,8 @@ import Mathlib.CategoryTheory.Sites.DenseSubsite
 import Mathlib.CategoryTheory.Sites.InducedTopology
 import Mathlib.CategoryTheory.Sites.Closed
 import FindWithGpt
+import Mathlib.Topology.Category.CompHaus.Basic
+import Mathlib.CategoryTheory.Preadditive.Projective
 /-!
 # Sheaves on CompHaus are equivalent to sheaves on ExtrDisc
 
@@ -92,10 +94,33 @@ lemma coverDense :
       intro b
       refine ⟨(), ?_⟩ 
       have hπ : 
-        Function.Surjective B.presentationπ := sorry
+        Function.Surjective B.presentationπ := by
+          rw [← CompHaus.epi_iff_surjective B.presentationπ]
+          exact CompHaus.epiPresentπ B
       exact hπ b
   convert hS
-  sorry
+  ext Y f
+  constructor
+  · rintro ⟨⟨obj, lift, map, fact⟩⟩ 
+    obtain ⟨obj_factors⟩ : Projective obj.compHaus := by 
+      infer_instance
+    obtain ⟨p, p_factors⟩ := obj_factors map B.presentationπ 
+    refine ⟨(CompHaus.presentation B).compHaus ,?_⟩  
+    refine ⟨lift ≫ p, ⟨ B.presentationπ
+        , {
+        left := Presieve.singleton.mk
+        right := by
+          rw [Category.assoc, p_factors, fact]
+      } ⟩  
+      ⟩
+  · rintro ⟨Z, h, g, hypo1, ⟨_⟩⟩  
+    cases hypo1
+    constructor 
+    refine
+    { obj := CompHaus.presentation B
+      lift := h
+      map := CompHaus.presentationπ B
+      fac := rfl } 
 
 lemma coherentTopology_is_induced : 
     coherentTopology ExtrDisc.{u} = coverDense.inducedTopology := by