diff --git a/CategoryTheoryExercises/Exercises/Exercise5.lean b/CategoryTheoryExercises/Exercises/Exercise5.lean index 68dc78f..65c4522 100644 --- a/CategoryTheoryExercises/Exercises/Exercise5.lean +++ b/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 \ No newline at end of file +end CategoryTheory \ No newline at end of file diff --git a/CategoryTheoryExercises/Solutions/Solution5.lean b/CategoryTheoryExercises/Solutions/Solution5.lean index 9c8ac04..438f088 100644 --- a/CategoryTheoryExercises/Solutions/Solution5.lean +++ b/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 diff --git a/Condensed/AB5.lean b/Condensed/AB5.lean new file mode 100644 index 0000000..63b34db --- /dev/null +++ b/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 + +-/ \ No newline at end of file diff --git a/Condensed/Equivalence.lean b/Condensed/Equivalence.lean index 3a16cb2..2d42ff9 100644 --- a/Condensed/Equivalence.lean +++ b/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 diff --git a/Condensed/Projectives.lean b/Condensed/Projectives.lean new file mode 100644 index 0000000..b3131b7 --- /dev/null +++ b/Condensed/Projectives.lean @@ -0,0 +1,226 @@ +import Condensed.SheafCondition +import Mathlib.Condensed.Abelian +import Mathlib.CategoryTheory.Sites.Adjunction +import Mathlib.Algebra.Category.GroupCat.Adjunctions +import Mathlib.Topology.Category.CompHaus.Projective +import ExtrDisc.Epi +import TopCat.toCondensed +import Condensed.Equivalence + +universe u + +namespace Condensed + +-- Free stuff + +open CategoryTheory Limits Opposite + +noncomputable +instance : PreservesLimits (forget AddCommGroupCat.{u+1}) := + AddCommGroupCat.forgetPreservesLimits.{u+1, u+1} + +def forgetAb : CondensedAb.{u} ⥤ Condensed.{u} (Type (u+1)) := + sheafCompose _ (forget _) + +noncomputable +def freeAb : Condensed.{u} (Type (u+1)) ⥤ CondensedAb.{u} := + Sheaf.composeAndSheafify _ <| AddCommGroupCat.free + +noncomputable +def adjunction : freeAb ⊣ forgetAb := + CategoryTheory.Sheaf.adjunction _ AddCommGroupCat.adj + +notation "ℤ[" S "]" => freeAb.obj S +notation "ℤ[" S "]" => freeAb.obj (CompHaus.toCondensed.obj S) +notation "ℤ[" S "]" => freeAb.obj + (CompHaus.toCondensed.obj (ExtrDisc.toCompHaus.obj S)) + +noncomputable +example (S : Condensed.{u} (Type (u+1))) : CondensedAb.{u} := + ℤ[S] + +noncomputable +example (S : CompHaus) : CondensedAb.{u} := + ℤ[S] + +noncomputable +example (S : ExtrDisc) : CondensedAb.{u} := + ℤ[S] + +theorem epi_iff_forall_epi + (E X : CondensedAb.{u}) (f : E ⟶ X) : + Epi f ↔ ∀ (S : ExtrDisc.{u}), Epi (f.val.app (op S.compHaus)) := by + let e : CondensedAb.{u} ≌ + Sheaf (coherentTopology ExtrDisc.{u}) AddCommGroupCat.{u+1} := + ExtrDiscCompHaus.equivalence _ |>.symm + let f' := e.functor.map f + suffices Epi f' ↔ ∀ (S : ExtrDisc.{u}), Epi (f.val.app (op S.compHaus)) + by sorry + let f'' := sheafToPresheaf _ _ |>.map f' + suffices Epi f' ↔ Epi f'' by sorry + sorry -- this depends on the characterization of sheaves + -- on ExtrDisc. + +theorem projective_of_projective + (S : CompHaus.{u}) [Projective S] : + Projective ℤ[S] := by + constructor + intro E X f e he + rw [epi_iff_forall_epi] at he + have : ExtremallyDisconnected S := sorry -- Gleason (the easy direction) + let T : ExtrDisc := ⟨S⟩ + specialize he T + let E' := forgetAb.obj E + let X' := forgetAb.obj X + let T' := CompHaus.toCondensed.obj S + let gg : (T' ⟶ E') → (T' ⟶ X') := + fun q => q ≫ forgetAb.map e + have hg : Function.Surjective gg := sorry + -- from he + let f' : T' ⟶ X' := adjunction.homEquiv _ _ f + --cases' hg f' with g' hg' + obtain ⟨g',hg'⟩ := hg f' + let g : ℤ[S] ⟶ E := + (adjunction.homEquiv _ _).symm g' + refine ⟨g, ?_⟩ + sorry + +def projIndex (A : CondensedAb.{u}) := + Σ (E : ExtrDisc.{u}), + CompHaus.toCondensed.obj E.compHaus ⟶ forgetAb.obj A + +#check projIndex + +instance : HasColimits CondensedAb.{u} := sorry + +noncomputable +def projPres (A : CondensedAb.{u}) : + CondensedAb.{u} := + ∐ fun (E : projIndex A) => ℤ[E.1] + +noncomputable +def projPresπ (A : CondensedAb.{u}) : + projPres A ⟶ A := + Sigma.desc fun ⟨_,f⟩ => + adjunction.homEquiv _ _|>.symm f + +-- GOAL +instance : EnoughProjectives CondensedAb.{u} where + presentation A := Nonempty.intro <| + { p := projPres A + projective := sorry + f := projPresπ A + epi := sorry } + +end Condensed + + + +/- +#exit + +namespace Condensed + +open CategoryTheory Limits Opposite + +def forgetAb : CondensedAb.{u} ⥤ Condensed.{u} (Type (u+1)) := + letI : PreservesLimits (forget AddCommGroupCat.{u+1}) := + AddCommGroupCat.forgetPreservesLimits.{u+1, u+1} + sheafCompose _ (forget _) + +noncomputable +def freeAb : Condensed.{u} (Type (u+1)) ⥤ CondensedAb.{u} := + letI : PreservesLimits (forget AddCommGroupCat.{u+1}) := + AddCommGroupCat.forgetPreservesLimits.{u+1, u+1} + Sheaf.composeAndSheafify _ (AddCommGroupCat.free) + +noncomputable +def adjunctionAb : freeAb.{u} ⊣ forgetAb := + letI : PreservesLimits (forget AddCommGroupCat.{u+1}) := + AddCommGroupCat.forgetPreservesLimits.{u+1, u+1} + CategoryTheory.Sheaf.adjunction _ AddCommGroupCat.adj + +notation "ℤ[" S "]" => freeAb.obj S +notation "ℤ[" S "]" => freeAb.obj (CompHaus.toCondensed.obj S) + +def _root_.String.tails (S : String) : Array String := Id.run <| do + let mut out := #[] + for i in [:S.length] do + out := out.push <| S.extract ⟨i⟩ ⟨S.length⟩ + return out + +def _root_.String.containsStr (S T : String) : Bool := Id.run <| do + for tail in S.tails do + if T.isPrefixOf tail then return true + return false + +open Lean Elab Command in +#eval show CommandElabM Unit from do + let env ← getEnv + for (c,tp) in env.constants.toList do + if c.isInternal then continue + if c.toString.containsStr "preservesEpi" then + IO.println "---" + IO.println c + let e ← ppExprWithInfos { env := env } tp.type + IO.println <| e.fmt + +lemma epi_iff_extrDisc {A B : CondensedAb.{u}} + (f : A ⟶ B) : + Epi f ↔ (∀ S : ExtrDisc.{u}, Epi (f.val.app (op S.compHaus))) := by + let e := Condensed.ExtrDiscCompHaus.equivalence AddCommGroupCat.{u+1} + let f' := e.inverse.map f + suffices Epi f' ↔ ∀ (S : ExtrDisc), Epi (f'.val.app (op S)) by sorry + suffices Epi f' ↔ Epi ((sheafToPresheaf _ _).map f') by sorry + constructor + · intro + have : (sheafToPresheaf (coherentTopology ExtrDisc) AddCommGroupCat).PreservesEpimorphisms := by + constructor + intros + suffices PreservesColimits (sheafToPresheaf (coherentTopology ExtrDisc) AddCommGroupCat) by + apply + preserves_epi_of_preservesColimit (sheafToPresheaf (coherentTopology ExtrDisc) AddCommGroupCat) + sorry + apply Functor.map_epi + · intro he + apply (sheafToPresheaf (coherentTopology ExtrDisc) AddCommGroupCat).epi_of_epi_map + assumption + +lemma projective_of_free_of_projective + (S : CompHaus.{u}) [Projective S] : Projective (ℤ[S]) := by + constructor + intro E X f e he + rw [epi_iff_extrDisc] at he + have : ExtremallyDisconnected S := sorry -- Gleason + let T : ExtrDisc := ⟨S⟩ + let g : CompHaus.toCondensed.obj S ⟶ forgetAb.obj X := + adjunctionAb.homEquiv _ _ f + specialize he T + let thing : (CompHaus.toCondensed.obj T.compHaus ⟶ forgetAb.obj E) → + (CompHaus.toCondensed.obj T.compHaus ⟶ forgetAb.obj X) := + fun q => q ≫ forgetAb.map e -- essentially e.val.app (op T.compHaus) + have hthing : Function.Surjective thing := sorry -- from he + obtain ⟨g', hg'⟩ := hthing g + let f' : ℤ[S] ⟶ E := + (adjunctionAb.homEquiv _ _).symm g' + refine ⟨f', ?_⟩ + sorry + +instance : HasColimits CondensedAb.{u} := sorry + +def projectiveIndex (B : CondensedAb.{u}) := + Σ (S : ExtrDisc.{u}), CompHaus.toCondensed.obj S.compHaus ⟶ forgetAb.obj B + +noncomputable +def projectivePresentation (B : CondensedAb.{u}) : + ProjectivePresentation B where + p := ∐ fun (⟨S,i⟩ : projectiveIndex B) => ℤ[S.compHaus] + projective := sorry + f := sorry + epi := sorry + +instance : EnoughProjectives CondensedAb.{u} := EnoughProjectives.mk <| + fun _ => ⟨projectivePresentation _⟩ + +end Condensed +-/ \ No newline at end of file diff --git a/Condensed/SheafCondition.lean b/Condensed/SheafCondition.lean new file mode 100644 index 0000000..41be861 --- /dev/null +++ b/Condensed/SheafCondition.lean @@ -0,0 +1,76 @@ +import Mathlib.Condensed.Basic +import FindWithGpt + +namespace Condensed + +open CategoryTheory Limits Opposite + + +universe u v w + +-- TODO: Move +lemma isSheafFor_ofArrows + {α : Type} {C : Type _} [Category C] (P : Cᵒᵖ ⥤ Type w) + (B : C) (X : α → C) (π : (a : α) → (X a ⟶ B)) : + Presieve.IsSheafFor P (Presieve.ofArrows X π) ↔ + (∀ (x : (a : α) → P.obj (op (X a))) + (hx : ∀ (R : C) (i j : α) (ri : R ⟶ X i) (rj : R ⟶ X j), + P.map ri.op (x i) = P.map rj.op (x j)), + ∃! b : P.obj (op B), ∀ i, P.map (π i).op b = x i) := sorry + +variable {C : Type w} [Category.{v} C] + +noncomputable +def productFan (P : CompHaus.{u}ᵒᵖ ⥤ C) + {α : Type} [Fintype α] + (X : α → CompHaus.{u}) : + Fan fun a => P.obj (X a |> op) := + Fan.mk (P.obj (∐ X |> op)) fun a => P.map (Sigma.ι _ a).op + +def ProductCondition (P : CompHaus.{u}ᵒᵖ ⥤ C) : Prop := + ∀ {α : Type} [Fintype α] (X : α → CompHaus.{u}), + Nonempty (IsLimit <| productFan P X) + +noncomputable +def equalizerFork (P : CompHaus.{u}ᵒᵖ ⥤ C) + {X B : CompHaus.{u}} (f : X ⟶ B) : + Fork + (P.map <| pullback.fst (f := f) (g := f) |>.op) + (P.map <| pullback.snd (f := f) (g := f) |>.op) := + Fork.ofι (P.map f.op) <| by + simp only [← P.map_comp, ← op_comp, pullback.condition] + +def EqualizerCondition (P : CompHaus.{u}ᵒᵖ ⥤ C) : Prop := + ∀ {X Y : CompHaus.{u}} (f : X ⟶ Y) [Epi f], + Nonempty (IsLimit <| equalizerFork P f) + +theorem isSheaf_iff_conditions (P : CompHaus.{u}ᵒᵖ ⥤ C) : + Presheaf.IsSheaf (coherentTopology CompHaus) P ↔ + ProductCondition P ∧ EqualizerCondition P := by + constructor + · intro H + constructor + · intro α _ X + let B := ∐ X + let π : (a : α) → (X a ⟶ B) := + Sigma.ι X + have : EffectiveEpiFamily X π := sorry + specialize H (P.obj <| op B) + erw [Presieve.isSheaf_coverage] at H + specialize H (Presieve.ofArrows X π) ?_ + · sorry + sorry + · sorry + · intro ⟨H1,H2⟩ + intro T + erw [Presieve.isSheaf_coverage] + rintro B R ⟨α, _, X, π, rfl, H⟩ + specialize H2 (Sigma.desc π) + rw [isSheafFor_ofArrows] + intro x hx + dsimp at x + sorry + +end Condensed + + diff --git a/ExtrDisc/Basic.lean b/ExtrDisc/Basic.lean index 5379e0f..88fddf3 100644 --- a/ExtrDisc/Basic.lean +++ b/ExtrDisc/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2023 Adam Topaz. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam Topaz -/ +import ExtrDisc.Gleason import Mathlib.CategoryTheory.Sites.Coherent import Mathlib.Topology.Category.CompHaus.Projective import Mathlib.Topology.Category.Profinite.Basic @@ -15,14 +16,14 @@ This file develops some of the basic theory of extremally disconnected sets. ## Overview -This file defines the type `ExtrDisc` of all extremally (note: not "extremely"!) +This file defines the type `ExtrDisc` of all extremally (note: not "extremely"!) disconnected spaces, and gives it the structure of a large category. -The Lean implementation: a term of type `ExtrDisc` is a pair, considering of +The Lean implementation: a term of type `ExtrDisc` is a pair, considering of a term of type `CompHaus` (i.e. a compact Hausdorff topological space) plus a proof that the space is extremally disconnected. -This is equivalent to the assertion that the term is projective in `CompHaus`, -in the sense of category theory (i.e., such that morphisms out of the object +This is equivalent to the assertion that the term is projective in `CompHaus`, +in the sense of category theory (i.e., such that morphisms out of the object can be lifted along epimorphisms). This file defines the type of all extremally disconnected spaces, gives it the @@ -38,10 +39,8 @@ category and various functors from it. ## TODO -The following proofs need to be filled in: +The following proofs need to be filled in: -* Gleason's theorem: a compact Hausdorff space is extrDisc if and - only if it is projective (one direction is in `mathlib4`). * If `X` is extremally disconnected then it is totally disconnected. * The forgetful functor `toCompHaus : ExtrDisc ⥤ CompHaus` is full and faithful. * The functor `toProfinite : ExtrDisc ⥤ Profinite` is full and faithful. @@ -63,7 +62,7 @@ attribute [nolint docBlame] ExtrDisc.compHaus ExtrDisc.extrDisc namespace ExtrDisc /-- Extremally disconnected spaces form a large category. -/ -instance : LargeCategory ExtrDisc.{u} := +instance : LargeCategory ExtrDisc.{u} := show Category (InducedCategory CompHaus (·.compHaus)) from inferInstance /-- The (forgetful) functor from extremally disconnected spaces to compact Hausdorff spaces. -/ @@ -71,6 +70,13 @@ instance : LargeCategory ExtrDisc.{u} := def toCompHaus : ExtrDisc.{u} ⥤ CompHaus.{u} := inducedFunctor _ +/-- Construct a term of `ExtrDistr` from a type endowed with the structure of a +compact, Hausdorff and totally disconnected topological space. +-/ +def of (X : Type _) [TopologicalSpace X] [CompactSpace X] [T2Space X] + [ExtremallyDisconnected X] : ExtrDisc := + ⟨⟨⟨X, inferInstance⟩⟩⟩ + /-- The forgetful functor `ExtrDisc ⥤ CompHaus` is full. -/ instance : Full toCompHaus where preimage := fun f => f @@ -92,18 +98,18 @@ instance : CoeSort ExtrDisc.{u} (Type u) := ConcreteCategory.hasCoeToSort _ instance {X Y : ExtrDisc.{u}} : FunLike (X ⟶ Y) X (fun _ => Y) := ConcreteCategory.funLike /-- Extremally disconnected spaces are topological spaces. -/ -instance (X : ExtrDisc.{u}) : TopologicalSpace X := +instance instTopologicalSpace (X : ExtrDisc.{u}) : TopologicalSpace X := show TopologicalSpace X.compHaus from inferInstance /-- Extremally disconnected spaces are compact. -/ -instance (X : ExtrDisc.{u}) : CompactSpace X := +instance (X : ExtrDisc.{u}) : CompactSpace X := show CompactSpace X.compHaus from inferInstance /-- Extremally disconnected spaces are Hausdorff. -/ -instance (X : ExtrDisc.{u}) : T2Space X := +instance (X : ExtrDisc.{u}) : T2Space X := show T2Space X.compHaus from inferInstance -instance (X : ExtrDisc.{u}) : ExtremallyDisconnected X := +instance (X : ExtrDisc.{u}) : ExtremallyDisconnected X := X.2 open ExtremallyDisconnected @@ -111,11 +117,11 @@ instance [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnect constructor -- have := open_closure (Set.univ : Set X) (by apply?) -- TODO fail replace intro t _ hpt - + by_contra ht - rw [Set.not_subsingleton_iff] at ht + rw [Set.not_subsingleton_iff] at ht -- rcases? ht -- TODO - rcases ht with ⟨x, hx, y, hy, hxy⟩ + rcases ht with ⟨x, hx, y, hy, hxy⟩ rcases T2Space.t2 x y hxy with ⟨U, V, hU, hV, hxU, hyV, hUV⟩ have := open_closure U hU -- specialize hpt U (Uᶜ) hU -- TODO why bracket @@ -136,19 +142,19 @@ instance [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnect /-- Extremally disconnected spaces are totally disconnected. -/ -instance (X : ExtrDisc.{u}) : TotallySeparatedSpace X := -{ isTotallySeparated_univ := by - intro x _ y _ hxy +instance (X : ExtrDisc.{u}) : TotallySeparatedSpace X := +{ isTotallySeparated_univ := by + intro x _ y _ hxy obtain ⟨U, V, hUV⟩ := T2Space.t2 x y hxy - use closure U - use (closure U)ᶜ + use closure U + use (closure U)ᶜ refine ⟨ExtremallyDisconnected.open_closure U hUV.1, - by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_, - by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩ + by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_, + by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩ simp only [Set.mem_compl_iff] - rw [mem_closure_iff] - push_neg - use V + rw [mem_closure_iff] + push_neg + use V refine' ⟨hUV.2.1,hUV.2.2.2.1,_⟩ rw [Set.nonempty_iff_ne_empty] simp only [not_not] @@ -160,8 +166,8 @@ instance (X : ExtrDisc.{u}) : TotallyDisconnectedSpace X := inferInstance /-- The functor from extremally disconnected spaces to profinite spaces. -/ @[simps] def toProfinite : ExtrDisc.{u} ⥤ Profinite.{u} where - obj X := { - toCompHaus := X.compHaus, + obj X := { + toCompHaus := X.compHaus, IsTotallyDisconnected := show TotallyDisconnectedSpace X from inferInstance } map f := f @@ -169,11 +175,19 @@ def toProfinite : ExtrDisc.{u} ⥤ Profinite.{u} where instance : Full toProfinite := sorry instance : Faithful toProfinite := sorry -example : toProfinite ⋙ profiniteToCompHaus = toCompHaus := +example : toProfinite ⋙ profiniteToCompHaus = toCompHaus := rfl -- TODO: Gleason's theorem. -instance (X : ExtrDisc) : Projective X.compHaus := sorry +instance (X : ExtrDisc) : Projective X.compHaus where + factors := by + intro B C φ f _ + haveI : ExtremallyDisconnected X.compHaus.toTop := X.extrDisc + have hf : f.1.Surjective + · rwa [CompHaus.epi_iff_surjective] at * + use ⟨_, (gleason_diagram_commutes φ.continuous f.continuous hf).left⟩ + ext + exact congr_fun (gleason_diagram_commutes φ.continuous f.continuous hf).right _ end ExtrDisc @@ -185,19 +199,19 @@ namespace CompHaus noncomputable def presentation (X : CompHaus) : ExtrDisc where compHaus := (projectivePresentation X).p - extrDisc := sorry + extrDisc := sorry /-- The morphism from `presentation X` to `X`. -/ noncomputable -def presentationπ (X : CompHaus) : X.presentation.compHaus ⟶ X := +def presentationπ (X : CompHaus) : X.presentation.compHaus ⟶ X := (projectivePresentation X).f /-- The morphism from `presentation X` to `X` is an epimorphism. -/ noncomputable -instance epiPresentπ (X : CompHaus) : Epi X.presentationπ := +instance epiPresentπ (X : CompHaus) : Epi X.presentationπ := (projectivePresentation X).epi -/-- +/-- X | @@ -205,14 +219,14 @@ instance epiPresentπ (X : CompHaus) : Epi X.presentationπ := | \/ Z ---(e)---> Y - + If `Z` is extremally disconnected, X, Y are compact Hausdorff, if `f : X ⟶ Y` is an epi and `e : Z ⟶ Y` is arbitrary, then `lift e f` is a fixed (but arbitrary) lift of `e` to a morphism `Z ⟶ X`. It exists because -`Z` is a projective object in `CompHaus`. +`Z` is a projective object in `CompHaus`. -/ noncomputable def lift {X Y : CompHaus} {Z : ExtrDisc} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [Epi f] : Z.compHaus ⟶ X := - Projective.factorThru e f + Projective.factorThru e f @[simp, reassoc] lemma lift_lifts {X Y : CompHaus} {Z : ExtrDisc} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [Epi f] : @@ -222,7 +236,7 @@ lemma lift_lifts {X Y : CompHaus} {Z : ExtrDisc} (e : Z.compHaus ⟶ Y) (f : X instance : Limits.HasCoproducts ExtrDisc.{u} := sorry /-- The category of extremally disconnected spaces has finite coproducts. -/ -instance : Limits.HasFiniteCoproducts ExtrDisc.{u} := +instance : Limits.HasFiniteCoproducts ExtrDisc.{u} := Limits.hasFiniteCoproducts_of_hasCoproducts.{u} ExtrDisc.{u} end CompHaus diff --git a/ExtrDisc/Coherent.lean b/ExtrDisc/Coherent.lean index f7c87a2..bce42f3 100644 --- a/ExtrDisc/Coherent.lean +++ b/ExtrDisc/Coherent.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam Topaz -/ import ExtrDisc.Basic +import ExtrDisc.Epi /-! # The category of extremally disconnected spaces is precoherent @@ -13,17 +14,37 @@ spaces is precoherent. Precoherence is the claim that "effective epis pull back" and is the condition we'll use to define a *coverage* on `ExtrDisc`, which is a collection of covering presieves satisfying a pullback condition. -## TODO - -Supply the proof! - -/ universe u -open CategoryTheory +open CategoryTheory CompHaus Functor namespace ExtrDisc -instance : Precoherent ExtrDisc.{u} := sorry +theorem _root_.CategoryTheory.EffectiveEpiFamily.toCompHaus {α : Type} [Fintype α] {B : ExtrDisc.{u}} + {X : α → ExtrDisc.{u}} {π : (a : α) → (X a ⟶ B)} (H : EffectiveEpiFamily X π) : + EffectiveEpiFamily (fun a => toCompHaus.obj (X a) ) (fun a => toCompHaus.map (π a)) := by + refine' ((CompHaus.effectiveEpiFamily_tfae _ _).out 0 2).2 (fun b => _) + exact (((effectiveEpiFamily_tfae _ _).out 0 2).1 H : ∀ _, ∃ _, _) _ + +instance : Precoherent ExtrDisc.{u} := by + constructor + intro B₁ B₂ f α _ X₁ π₁ h₁ + refine' ⟨α, inferInstance, fun a => (pullback f (π₁ a)).presentation, fun a => + toCompHaus.preimage (presentationπ _ ≫ (pullback.fst _ _)), _, id, fun a => + toCompHaus.preimage (presentationπ _ ≫ (pullback.snd _ _ )), fun a => _⟩ + · refine' ((effectiveEpiFamily_tfae _ _).out 0 2).2 (fun b => _) + have h₁' := ((CompHaus.effectiveEpiFamily_tfae _ _).out 0 2).1 h₁.toCompHaus + obtain ⟨a, x, h⟩ := h₁' (f b) + obtain ⟨c, hc⟩ := (CompHaus.epi_iff_surjective _).1 (epiPresentπ (pullback f (π₁ a))) ⟨⟨b, x⟩, h.symm⟩ + refine' ⟨a, c, _⟩ + change toCompHaus.map (toCompHaus.preimage _) _ = _ + simp only [image_preimage, toCompHaus_obj, comp_apply, hc] + rfl + · apply map_injective toCompHaus + simp only [map_comp, image_preimage, Category.assoc] + congr 1 + ext ⟨⟨_, _⟩, h⟩ + exact h.symm end ExtrDisc \ No newline at end of file diff --git a/ExtrDisc/Epi.lean b/ExtrDisc/Epi.lean index 69896d0..c56c619 100644 --- a/ExtrDisc/Epi.lean +++ b/ExtrDisc/Epi.lean @@ -1,31 +1,309 @@ import ExtrDisc.Basic import Mathlib.Topology.Category.CompHaus.EffectiveEpi -open CategoryTheory +open CategoryTheory Limits + +universe u + +/-! +This section contains helper lemmas about the sigma-type `Σ i, π i`, +they probably belong into a different place. +-/ +section Sigma + +@[simp] +theorem mem_sigma_iff {π : ι → Type _} [∀ i, TopologicalSpace (π i)] + {i : ι} {x : π i} {s : Set (Σ i, π i)} + : x ∈ Sigma.mk i ⁻¹' s ↔ ⟨i, x⟩ ∈ s := + Iff.rfl + +lemma sigma_mk_preimage_image' (h : i ≠ j) : Sigma.mk j ⁻¹' (Sigma.mk i '' U) = ∅ := by + change Sigma.mk j ⁻¹' {⟨i, u⟩ | u ∈ U} = ∅ + -- change { x | (Sigma.mk j) x ∈ {⟨i, u⟩ | u ∈ U}} = ∅ + simp [h] + +lemma sigma_mk_preimage_image_eq_self : Sigma.mk i ⁻¹' (Sigma.mk i '' U) = U := by + change Sigma.mk i ⁻¹' {⟨i, u⟩ | u ∈ U} = U + simp + +-- Note: It might be possible to use Gleason for this instead +/-- The sigma-type of extremally disconneted spaces is extremally disconnected -/ +instance instExtremallyDisconnected + {π : ι → Type _} [∀ i, TopologicalSpace (π i)] [h₀ : ∀ i, ExtremallyDisconnected (π i)] : + ExtremallyDisconnected (Σi, π i) := by + constructor + intro s hs + rw [isOpen_sigma_iff] at hs ⊢ + intro i + rcases h₀ i with ⟨h₀⟩ + have h₁ : IsOpen (closure (Sigma.mk i ⁻¹' s)) + · apply h₀ + exact hs i + suffices h₂ : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s) + · rwa [h₂] + apply IsOpenMap.preimage_closure_eq_closure_preimage + intro U _ + · rw [isOpen_sigma_iff] + intro j + by_cases ij : i = j + · rw [← ij] + rw [sigma_mk_preimage_image_eq_self] + assumption + · rw [sigma_mk_preimage_image' ij] + apply isOpen_empty + · continuity + +end Sigma namespace ExtrDisc -universe u +-- Assume we have `X a → B` which are jointly surjective. +variable {α : Type} [Fintype α] {B : ExtrDisc.{u}} + {X : α → ExtrDisc.{u}} (π : (a : α) → (X a ⟶ B)) + (surj : ∀ b : B, ∃ (a : α) (x : X a), π a x = b) + +/-! +This section defines the finite Coproduct of a finite family +of profinite spaces `X : α → ExtrDisc.{u}` + +Notes: The content is mainly copied from +`Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean` +-/ +section FiniteCoproducts + +variable (X) + +/-- +The coproduct of a finite family of objects in `ExtrDisc`, constructed as the disjoint +union with its usual topology. +-/ +def finiteCoproduct : ExtrDisc := ExtrDisc.of <| Σ (a : α), X a + +/-- The inclusion of one of the factors into the explicit finite coproduct. -/ +def finiteCoproduct.ι (a : α) : X a ⟶ finiteCoproduct X where + toFun := fun x => ⟨a,x⟩ + continuous_toFun := continuous_sigmaMk (σ := fun a => X a) + +/-- +To construct a morphism from the explicit finite coproduct, it suffices to +specify a morphism from each of its factors. +This is essentially the universal property of the coproduct. +-/ +def finiteCoproduct.desc {B : ExtrDisc.{u}} (e : (a : α) → (X a ⟶ B)) : + finiteCoproduct X ⟶ B where + toFun := fun ⟨a,x⟩ => e a x + continuous_toFun := by + apply continuous_sigma + intro a ; exact (e a).continuous + +@[reassoc (attr := simp)] +lemma finiteCoproduct.ι_desc {B : ExtrDisc.{u}} (e : (a : α) → (X a ⟶ B)) (a : α) : + finiteCoproduct.ι X a ≫ finiteCoproduct.desc X e = e a := rfl + +lemma finiteCoproduct.hom_ext {B : ExtrDisc.{u}} (f g : finiteCoproduct X ⟶ B) + (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g := by + ext ⟨a,x⟩ + specialize h a + apply_fun (fun q => q x) at h + exact h + +/-- The coproduct cocone associated to the explicit finite coproduct. -/ +@[simps] +def finiteCoproduct.cocone : Limits.Cocone (Discrete.functor X) where + pt := finiteCoproduct X + ι := Discrete.natTrans fun ⟨a⟩ => finiteCoproduct.ι X a + +/-- The explicit finite coproduct cocone is a colimit cocone. -/ +@[simps] +def finiteCoproduct.isColimit : Limits.IsColimit (finiteCoproduct.cocone X) where + desc := fun s => finiteCoproduct.desc _ fun a => s.ι.app ⟨a⟩ + fac := fun s ⟨a⟩ => finiteCoproduct.ι_desc _ _ _ + uniq := fun s m hm => finiteCoproduct.hom_ext _ _ _ fun a => by + specialize hm ⟨a⟩ + ext t + apply_fun (fun q => q t) at hm + exact hm + +end FiniteCoproducts + +/-- +`Fin 2` as an extremally disconnected space. +Implementation: This is only used in the proof below. +-/ +protected +def two : ExtrDisc.{u} where + compHaus := CompHaus.of <| ULift <| Fin 2 + extrDisc := by + dsimp + constructor + intro U _ + apply isOpen_discrete (closure U) lemma epi_iff_surjective {X Y : ExtrDisc.{u}} (f : X ⟶ Y) : - Epi f ↔ Function.Surjective f := - sorry + Epi f ↔ Function.Surjective f := by + constructor + · dsimp [Function.Surjective] + contrapose! + rintro ⟨y,hy⟩ h + let C := Set.range f + have hC : IsClosed C := (isCompact_range f.continuous).isClosed + let U := Cᶜ + have hyU : y ∈ U := by + refine' Set.mem_compl _ + rintro ⟨y', hy'⟩ + exact hy y' hy' + have hUy : U ∈ nhds y := hC.compl_mem_nhds hyU + haveI : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y)) := + show TotallyDisconnectedSpace Y from inferInstance + obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy + classical + let g : Y ⟶ ExtrDisc.two := + ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩ + let h : Y ⟶ ExtrDisc.two := ⟨fun _ => ⟨1⟩, continuous_const⟩ + have H : h = g := by + rw [← cancel_epi f] + apply ContinuousMap.ext ; intro x + apply ULift.ext + change 1 = _ + dsimp [LocallyConstant.ofClopen] + -- BUG: Should not have to provide instance `(ExtrDisc.instTopologicalSpace Y)` explicitely + rw [comp_apply, @ContinuousMap.coe_mk _ _ (ExtrDisc.instTopologicalSpace Y), + Function.comp_apply, if_neg] + refine' mt (fun α => hVU α) _ + simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not] + exact ⟨x, rfl⟩ + apply_fun fun e => (e y).down at H + dsimp [LocallyConstant.ofClopen] at H + change 1 = ite _ _ _ at H + rw [if_pos hyV] at H + exact top_ne_bot H + · intro (h : Function.Surjective (toCompHaus.map f)) + rw [← CompHaus.epi_iff_surjective] at h + constructor + intro W a b h + apply Functor.map_injective toCompHaus + apply_fun toCompHaus.map at h + simp only [Functor.map_comp] at h + rwa [← cancel_epi (toCompHaus.map f)] + +/-! +Everything in this section is only used for the proof of +`effectiveEpiFamily_of_jointly_surjective` +-/ +namespace EffectiveEpiFamily + +/-- +Abbreviation for the fully faithful functor `ExtrDisc ⥤ CompHaus` called `ExtrDisc.toCompHaus` +-/ +abbrev F := ExtrDisc.toCompHaus + +/-- A helper lemma lifting the condition +``` +∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), + g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) +``` +from `Z : ExtrDisc` to `Z : CompHaus`. This condition is used in +the definition of `EffectiveEpiFamily.dec`, etc. +-/ +lemma helper {W : ExtrDisc} {e : (a : α) → X a ⟶ W} + (h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), + g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) + : ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ F.obj (X a₁)) (g₂ : Z ⟶ F.obj (X a₂)), + g₁ ≫ (π a₁) = g₂ ≫ (π a₂) → g₁ ≫ e a₁ = g₂ ≫ e a₂ := by + intro Z a₁ a₂ g₁ g₂ hg + -- The Stone-Czech-compactification `βZ` of `Z : CompHaus` is in `ExtrDisc` + let βZ := Z.presentation + let g₁' := F.preimage (Z.presentationπ ≫ g₁ : F.obj βZ ⟶ F.obj (X a₁)) + let g₂' := F.preimage (Z.presentationπ ≫ g₂ : F.obj βZ ⟶ F.obj (X a₂)) + -- Use that `βZ → Z` is an epi + apply Epi.left_cancellation (f := Z.presentationπ) + -- By definition `g₁' = presentationπ ≫ g₁` and `g₂' = presentationπ ≫ g₂` + change g₁' ≫ e a₁ = g₂' ≫ e a₂ + -- use assumption in `ExtrDisc` + apply h + change CompHaus.presentationπ Z ≫ g₁ ≫ π a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ π a₂ + simp [hg] + +/-- Implementation: The structure for the `EffectiveEpiFamily X π` -/ +noncomputable +def struct : EffectiveEpiFamilyStruct X π where + desc := fun {W} e h => ExtrDisc.toCompHaus.preimage <| + -- Use the `EffectiveEpiFamily F(X) F(π)` on `CompHaus` + (CompHaus.effectiveEpiFamily_of_jointly_surjective (fun (a : α) => F.obj (X a)) π surj).desc + (fun (a : α) => F.map (e a)) (helper π h) + fac := by + intro W e he a + -- The `EffectiveEpiFamily F(X) F(π)` on `CompHaus` + have : EffectiveEpiFamily (fun a => F.obj (X a)) π := + CompHaus.effectiveEpiFamily_of_jointly_surjective (fun a => F.obj (X a)) π surj + -- The `fac` on `CompHaus` + have fac₁ := EffectiveEpiFamily.fac (fun (a : α) => F.obj (X a)) π e (helper π he) a + change F.map (π a ≫ _) = F.map (e a) at fac₁ + replace fac₁ := Faithful.map_injective fac₁ + exact fac₁ + uniq := by + intro W e he m hm + have Fhm : ∀ (a : α), π a ≫ F.map m = e a + · aesop_cat + have : EffectiveEpiFamily (fun a => F.obj (X a)) π := + CompHaus.effectiveEpiFamily_of_jointly_surjective (fun a => F.obj (X a)) π surj + have uniq₁ := + EffectiveEpiFamily.uniq (fun (a : α) => F.obj (X a)) π e (helper π he) (F.map m) Fhm + change F.map m = F.map _ at uniq₁ + replace uniq₁ := Faithful.map_injective uniq₁ + exact uniq₁ + +end EffectiveEpiFamily + +/-- On direction of `effectiveEpiFamily_tfae` -/ +theorem effectiveEpiFamily_of_jointly_surjective + {α : Type} [Fintype α] {B : ExtrDisc.{u}} + (X : α → ExtrDisc.{u}) (π : (a : α) → (X a ⟶ B)) + (surj : ∀ b : B, ∃ (a : α) (x : X a), π a x = b) : + EffectiveEpiFamily X π := + ⟨⟨ExtrDisc.EffectiveEpiFamily.struct π surj⟩⟩ open List in -theorem effectiveEpiFamily_tfae {α : Type} [Fintype α] {B : ExtrDisc.{u}} +/-- +For a finite family of extremally disconnected spaces `πₐ : Xₐ → B` the following are equivalent: +* they are an effective epi family +* the map `∐ πₐ ⟶ B` is an epimorphism +* they are jointly surjective +-/ +theorem effectiveEpiFamily_tfae {α : Type} [Fintype α] {B : ExtrDisc.{u}} (X : α → ExtrDisc.{u}) (π : (a : α) → (X a ⟶ B)) : TFAE [ EffectiveEpiFamily X π, Epi (Limits.Sigma.desc π), - ∀ (b : B), ∃ (a : α) (x : X a), π a x = b + ∀ (b : B), ∃ (a : α) (x : X a), π a x = b ] := by - tfae_have 1 → 2 - · intro ; infer_instance + tfae_have 1 → 2 + · intro ; infer_instance + tfae_have 1 → 2 + · intro ; infer_instance tfae_have 2 → 3 - · sorry + · intro e + rw [epi_iff_surjective] at e + let i : ∐ X ≅ finiteCoproduct X := + (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _) + intro b + obtain ⟨t,rfl⟩ := e b + let q := i.hom t + refine ⟨q.1,q.2,?_⟩ + have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id] ; rfl + rw [this] + show _ = (i.inv ≫ Sigma.desc π) (i.hom t) + suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by + rw [this] ; rfl + rw [Iso.inv_comp_eq] + apply colimit.hom_ext + rintro ⟨a⟩ + simp only [Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, + colimit.comp_coconePointUniqueUpToIso_hom_assoc] + ext ; rfl tfae_have 3 → 1 - · sorry + · apply effectiveEpiFamily_of_jointly_surjective tfae_finish -end ExtrDisc \ No newline at end of file +end ExtrDisc diff --git a/ExtrDisc/Gleason.lean b/ExtrDisc/Gleason.lean new file mode 100644 index 0000000..b5ebd5b --- /dev/null +++ b/ExtrDisc/Gleason.lean @@ -0,0 +1,257 @@ +import Mathlib.Topology.ExtremallyDisconnected +import Mathlib.Topology.Homeomorph + +variable {A B C D : Type _} {E : Set D} [TopologicalSpace A] [TopologicalSpace B] + [TopologicalSpace C] [TopologicalSpace D] + {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : ρ.Surjective) + {π : D → A} (π_cont : Continuous π) (π_surj : π.Surjective) + (image_ne_top : ∀ E₀ : Set E, E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤) + +open Set + +/-- Lemma 2.1 -/ +lemma image_subset_closure_compl_image_compl {G : Set E} (hG : IsOpen G) : + ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ) := by + by_cases G_empty : G = ∅ + · simpa only [G_empty, image_empty] using empty_subset _ + · intro a ha + rw [mem_closure_iff] + intro N hN ha' + rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩ + have non_empty : (G ∩ ρ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr ha'⟩ + have is_open : IsOpen <| G ∩ ρ⁻¹' N := hG.inter <| hN.preimage ρ_cont + have ne_top : ρ '' (G ∩ ρ⁻¹' N)ᶜ ≠ ⊤ := image_ne_top _ (compl_ne_univ.mpr non_empty) + is_open.isClosed_compl + rcases nonempty_compl.mpr ne_top with ⟨x, hx⟩ + have hx' : x ∈ (ρ '' Gᶜ)ᶜ := (compl_subset_compl.mpr <| image_subset ρ <| + compl_subset_compl.mpr <| G.inter_subset_left _) hx + rcases ρ_surj x with ⟨y, rfl⟩ + have hy : y ∈ G ∩ ρ⁻¹' N := not_mem_compl_iff.mp <| (not_imp_not.mpr <| mem_image_of_mem ρ) <| + (mem_compl_iff _ _).mp hx + exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩ + +/-- Lemma 2.2 -/ +lemma disjoint_of_extremally_disconnected [ExtremallyDisconnected A] {U₁ U₂ : Set A} + (h : Disjoint U₁ U₂) (hU₁ : IsOpen U₁) (hU₂ : IsOpen U₂) : Disjoint (closure U₁) (closure U₂) := + Disjoint.closure_left (h.closure_right hU₁) <| ExtremallyDisconnected.open_closure U₂ hU₂ + +lemma compact_to_T2_injective [T2Space A] [ExtremallyDisconnected A] [T2Space E] [CompactSpace E] : + ρ.Injective := by + intro x y h_eq_im + by_contra h + rcases t2_separation h with ⟨G₁, G₂, hG₁, hG₂, hxG₁, hyG₂, hG⟩ + have open1 : IsOpen ((ρ '' (G₁ᶜ))ᶜ) + · simp only [isOpen_compl_iff] + apply IsCompact.isClosed + refine' IsCompact.image (IsClosed.isCompact _) ρ_cont + simpa only [isClosed_compl_iff] + have open2 : IsOpen ((ρ '' (G₂ᶜ))ᶜ) + · simp only [isOpen_compl_iff] + apply IsCompact.isClosed + refine' IsCompact.image (IsClosed.isCompact _) ρ_cont + simpa only [isClosed_compl_iff] + have disj : Disjoint ((ρ '' (G₁ᶜ))ᶜ) ((ρ '' (G₂ᶜ))ᶜ) + · rw [disjoint_compl_left_iff_subset] + refine' subset_trans (subset_image_compl ρ_surj) _ + simp only [compl_compl, image_subset_iff] + refine' subset_trans _ (subset_preimage_image _ _) + rw [← disjoint_compl_left_iff_subset] + simpa only [compl_compl] + replace disj := disjoint_of_extremally_disconnected disj open1 open2 + have oups₁ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₁ + have oups₂ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₂ + have mem₁ : ρ x ∈ ρ '' G₁ + · exact mem_image_of_mem _ hxG₁ + have mem₂ : ρ x ∈ ρ '' G₂ + · rw [h_eq_im] + exact mem_image_of_mem _ hyG₂ + have mem : ρ x ∈ (closure ((ρ '' G₁ᶜ)ᶜ)) ∩ (closure ((ρ '' G₂ᶜ)ᶜ)) := ⟨oups₁ mem₁, oups₂ mem₂⟩ + exact (disj.ne_of_mem mem.1 mem.2) rfl + +/-- Lemma 2.3 -/ +noncomputable def compact_to_T2_homeomorph [T2Space A] [ExtremallyDisconnected A] [T2Space E] + [CompactSpace E] : E ≃ₜ A := + Continuous.homeoOfEquivCompactToT2 + (f := Equiv.ofBijective ρ ⟨compact_to_T2_injective ρ_cont ρ_surj image_ne_top, ρ_surj⟩) ρ_cont + +variable [T2Space A] [CompactSpace A] [T2Space B] [CompactSpace B] [T2Space C] (φ : A → C) (f : B → C) + +def D' : Set (A × B) := {x | φ x.fst = f x.snd} + +def π₁ : D' φ f → A := fun x ↦ x.val.fst + +def π₂ : D' φ f → B := fun x ↦ x.val.snd + +variable {φ f} (hφ : Continuous φ) (hf : Continuous f) (hf' : f.Surjective) + +/-- Lemma 2.4 -/ +lemma exists_image_ne_top : ∃ E : Set <| D' φ f, CompactSpace E ∧ π₁ φ f '' E = univ ∧ + ∀ E₀ : Set <| D' φ f, E₀ ⊂ E → CompactSpace E₀ → π₁ φ f '' E₀ ≠ univ := by + haveI : CompactSpace <| D' φ f := isCompact_iff_compactSpace.mp (IsClosed.isCompact + (isClosed_eq (Continuous.comp hφ continuous_fst) (Continuous.comp hf continuous_snd))) + -- Define the set of closed subsets of D for which the map onto A is surjective + let S := { E : Set (D' φ f) | CompactSpace E ∧ (π₁ φ f) '' E = univ} + -- Checking the Chain condition + have chain_cond : (∀ (c : Set (Set ↑(D' φ f))), + c ⊆ S → + IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s) := by + intro Ch h hCh + let M := sInter Ch + use M + constructor + · constructor + · rw [←isCompact_iff_compactSpace] + apply IsClosed.isCompact + apply isClosed_sInter + intro N hN + have N_comp := (h hN).1 + dsimp at N_comp + rw [←isCompact_iff_compactSpace] at N_comp + exact IsCompact.isClosed N_comp + --Next, we need to show that the image of M is all of A + · by_cases h₂ : Nonempty Ch + rotate_left 1 + -- Case that `Ch` is empty + · simp at h₂ + rw [←eq_empty_iff_forall_not_mem] at h₂ + revert M + rw [h₂, sInter_empty] + simp + exact range_iff_surjective.mpr <| fun a => ⟨⟨⟨_, _⟩, (hf' <| φ a).choose_spec.symm⟩, rfl⟩ + -- Now we assume that `Ch` is nonempty + · ext x + refine' ⟨ fun _ => trivial , fun _ => _ ⟩ + rw [mem_image] + change Set.Nonempty {x_1 : D' φ f | x_1 ∈ M ∧ π₁ φ f x_1 = x} + let Z : Ch → Set (D' φ f) := fun X => X ∩ (π₁ _ _)⁻¹' {x} + suffices Set.Nonempty <| ⋂ (X : Ch), (X: Set (D' φ f)) ∩ (π₁ _ _)⁻¹' {x} by + convert this + rw [← iInter_inter, ← sInter_eq_iInter] + rw [←setOf_inter_eq_sep, inter_comm] + congr + -- Using this result `nonempty_iInter_of_...` introduces a lot of unnecessary checks + have assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i) := by + intro X + -- `Z X` nonempty + simp + have h₃ := (h (Subtype.mem X)).2 + rw [←image_inter_nonempty_iff, h₃] + simp + -- `Z X` is Closed + have := (h (Subtype.mem X)).1 + rw [←isCompact_iff_compactSpace] at this + have h_cl := IsClosed.inter (IsCompact.isClosed this) + (IsClosed.preimage (Continuous.comp continuous_fst continuous_subtype_val) <| T1Space.t1 x) + exact And.intro (IsClosed.isCompact h_cl) h_cl + + apply IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed Z _ + (fun X => (assumps X).1) (fun X => (assumps X).2.1) (fun X => (assumps X).2.2) + -- Need to show the `Directed` assumption for the inclusion, which is annoying... + change Directed _ ((fun X => X ∩ _) ∘ (fun X => X: ↑Ch → Set (D' φ f))) + refine' Directed.mono_comp _ _ _ + · exact fun x y => x ⊇ y + · exact fun ⦃x y⦄ a => inter_subset_inter_left _ a + refine Iff.mp directedOn_iff_directed ?_ + refine IsChain.directedOn ?H + dsimp [IsChain, Pairwise] at hCh ⊢ + exact fun ⦃x⦄ a ⦃y⦄ a_1 a_2 => Or.comm.mp (hCh a a_1 a_2) + · intro X hX + exact sInter_subset_of_mem hX + have := zorn_superset S chain_cond + rcases this with ⟨E, ⟨⟨hE₁,hE₂⟩, hE₃⟩⟩ + use E + constructor + · exact hE₁ + constructor + · exact hE₂ + --Now, it's just rephrasing the conclusion of Zorn's Lemma + · intro E₀ h₁ h₂ + replace hE₃ := hE₃ E₀ + by_contra h₃ + replace hE₃ := hE₃ (And.intro h₂ h₃) (subset_of_ssubset h₁) + exact (ne_of_ssubset h₁) hE₃ + +def E' [T2Space A] [CompactSpace A] : Set <| D' φ f := (exists_image_ne_top hφ hf hf').choose + +noncomputable def ρ' [ExtremallyDisconnected A] : (E' hφ hf hf') ≃ₜ A := by + haveI : CompactSpace <| E' hφ hf hf' := (exists_image_ne_top hφ hf hf').choose_spec.1 + have π₁_surj : ((E' hφ hf hf').restrict (π₁ φ f)).Surjective := by + intro a + have := (exists_image_ne_top hφ hf hf').choose_spec.2.1 + have ha : a ∈ univ := by tauto + rw [← this] at ha + obtain ⟨c,hc⟩ := ha + use ⟨c,hc.1⟩ + exact hc.2 + have π₁_cont : Continuous ((E' hφ hf hf').restrict (π₁ φ f)) := + ContinuousOn.restrict (Continuous.continuousOn (Continuous.comp continuous_fst continuous_subtype_val)) + refine' compact_to_T2_homeomorph π₁_cont π₁_surj _ + have := (exists_image_ne_top hφ hf hf').choose_spec.2.2 + simp_rw [top_eq_univ, ← ne_eq, ← ssubset_univ_iff] + intro E₀ hE₀ hE₀c + let E₀' : Set (D' φ f) := Subtype.val '' E₀ + have hE₀' : E₀' ⊂ E' hφ hf hf' + · rw [ssubset_iff_subset_ne] + constructor + · intro x hx + dsimp at hx + obtain ⟨y,hy⟩ := hx + rw [← hy.2] + exact y.prop + · rw [ssubset_iff_subset_ne] at hE₀ + dsimp + intro h + apply hE₀.2 + ext x + refine' ⟨by tauto, _⟩ + intro _ + have hx := x.prop + simp_rw [← h] at hx + obtain ⟨y,hy⟩ := hx + have hxy : y = x + · ext1 + exact hy.2 + rw [← hxy] + exact hy.1 + specialize this E₀' hE₀' + rw [ssubset_univ_iff] + have hE₀c' : CompactSpace E₀' + · rw [← isCompact_iff_compactSpace] + haveI : CompactSpace <| D' φ f := isCompact_iff_compactSpace.mp (IsClosed.isCompact + (isClosed_eq (Continuous.comp hφ continuous_fst) (Continuous.comp hf continuous_snd))) + apply IsClosed.isCompact + dsimp + refine Iff.mp (ClosedEmbedding.closed_iff_image_closed ?hE₀c'.h.hf) hE₀c + apply closedEmbedding_subtype_val + apply IsCompact.isClosed + rw [isCompact_iff_compactSpace] + exact (exists_image_ne_top hφ hf hf').choose_spec.1 + have hπ : (E' hφ hf hf').restrict (π₁ φ f) '' E₀ = π₁ φ f '' E₀' + · simp only [restrict_apply] + ext a + simp only [mem_image, Subtype.exists, exists_and_right, Prod.exists, exists_eq_right] + specialize this hE₀c' + rwa [hπ] + +lemma gleason_diagram_commutes [ExtremallyDisconnected A] : + Continuous ((E' hφ hf hf').restrict (π₂ φ f) ∘ (ρ' hφ hf hf').invFun) ∧ + f ∘ ((E' hφ hf hf').restrict (π₂ φ f) ∘ (ρ' hφ hf hf').invFun) = φ := by + constructor + · refine' Continuous.comp _ _ + · refine' ContinuousOn.restrict _ + apply Continuous.continuousOn + exact Continuous.comp continuous_snd continuous_subtype_val + · exact (Homeomorph.continuous (Homeomorph.symm (ρ' hφ hf hf'))) + · suffices : f ∘ (E' hφ hf hf').restrict (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toFun + · simp only [← Function.comp.assoc] + rw [this] + simp only [Function.comp.assoc, Equiv.toFun_as_coe, Homeomorph.coe_toEquiv, + Equiv.invFun_as_coe, Homeomorph.coe_symm_toEquiv, + Homeomorph.self_comp_symm, Function.comp.right_id] + ext x + simp only [Function.comp_apply, restrict_apply, Equiv.toFun_as_coe, Homeomorph.coe_toEquiv] + dsimp [π₂, ρ', compact_to_T2_homeomorph, Continuous.homeoOfEquivCompactToT2_toEquiv, + Continuous.homeoOfEquivCompactToT2, π₁] + have := x.val.prop + dsimp [D'] at this + exact this.symm diff --git a/KevinLectures/abelian_categories.lean b/KevinLectures/abelian_categories.lean new file mode 100644 index 0000000..85b3d23 --- /dev/null +++ b/KevinLectures/abelian_categories.lean @@ -0,0 +1,130 @@ +import Mathlib.CategoryTheory.Abelian.Basic -- definition and basic properties of abelian categories + +import Mathlib.CategoryTheory.Limits.Preserves.Filtered -- definition and basic properties of +-- filtered colimits and cofiltered limits + +/- + +## An abelian category tutorial + +-/ + +open CategoryTheory + +-- let `𝒞` be an abelian category + +variable {𝒞 : Type u} [Category.{v} 𝒞] [Abelian 𝒞] +/- + +Note: `Abelian 𝒞` is *data*, because e.g. it contains the group structure +on `A ⟶ B` for all `A`, `B`. + +-/ + +-- Let A, B be objects of 𝒞 + +variable (A B : 𝒞) + +example : AddCommGroup (A ⟶ B) := inferInstance + +#synth AddCommGroup (A ⟶ B) + +variable (f g : A ⟶ B) in +#check f + g + +variable (f g : A ⟶ B) (C : 𝒞) (h : B ⟶ C) in +example : (f + g) ≫ h = f ≫ h + g ≫ h := by exact Preadditive.add_comp A B C f g h + +variable (C : 𝒞) (h : B ⟶ C) in +example : (A ⟶ B) →+ (A ⟶ C) := by exact Preadditive.rightComp A h + +-- exercise +example : Ring (A ⟶ A) := +{ Preadditive.homGroup A A with + mul := sorry + left_distrib := sorry + right_distrib := sorry + zero_mul := sorry + mul_zero := sorry + mul_assoc := sorry + one := 𝟙 A + one_mul := sorry + mul_one := sorry + add_left_neg := sorry +} + +open Limits + +noncomputable section + +variable (f : A ⟶ B) + + +#check kernel f +example : kernel f ⟶ A := by exact kernel.ι f +#check cokernel f +example : B ⟶ cokernel f := by exact cokernel.π f -- it's epi, and composition is zero + +#synth Mono (kernel.ι f) + +example : kernel.ι f ≫ f = 0 := by exact kernel.condition f + +example (g : C ⟶ A) (hg : g ≫ f = 0) : C ⟶ kernel f := by exact kernel.lift f g hg + +example (g : C ⟶ A) (hg : g ≫ f = 0) : kernel.lift f g hg ≫ kernel.ι f = g := by exact kernel.lift_ι f g hg + +example (g : B ⟶ C) (hg : f ≫ g = 0) : cokernel.π f ≫ cokernel.desc f g hg = g := sorry + +example [Mono f] [Epi f] : IsIso f := by exact isIso_of_mono_of_epi f + +#synth Balanced 𝒞 + +open Abelian +#check image f -- WARNING! +#check Abelian.image f -- WARNING! +#check Abelian.coimage f + +noncomputable example : Abelian.image f ⟶ B := by exact Abelian.image.ι f +noncomputable example : A ⟶ Abelian.image f := by exact Abelian.factorThruImage f + +example : Abelian.factorThruImage f ≫ Abelian.image.ι f = f := sorry + +-- coimage is cokernel of kernel +noncomputable example : A ⟶ Abelian.coimage f := sorry +noncomputable example : Abelian.coimage f ⟶ B := sorry + +example : coimage.π f ≫ Abelian.factorThruCoimage f = f := sorry + +noncomputable example : Abelian.coimage f ⟶ Abelian.image f := by exact coimageImageComparison f + +#synth IsIso (coimageImageComparison f) + +/- + +# Preserving Filtered Colimits (AB5) + +-/ +open Limits + +-- Let J be a (small) filtered category + +variable {J : Type v} [SmallCategory J] (K : J ⥤ 𝒞) + +variable (𝒟 : Type _) [Category 𝒟] (F : 𝒞 ⥤ 𝒟) + +example (h : ∀ {c : Cocone K}, IsColimit c → IsColimit (F.mapCocone c)) : PreservesColimit K F := +⟨h⟩ + + +example (h : ∀ K : J ⥤ 𝒞, PreservesColimit K F) : PreservesColimitsOfShape J F := ⟨@h⟩ + +example (h : ∀ (J : Type v) [SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F) : + PreservesFilteredColimits F := ⟨h⟩ + + + + + + + +#check PreservesFilteredColimits \ No newline at end of file diff --git a/Profinite/Coherent.lean b/Profinite/Coherent.lean index 4f6d05d..32588a3 100644 --- a/Profinite/Coherent.lean +++ b/Profinite/Coherent.lean @@ -5,15 +5,11 @@ Authors: Adam Topaz -/ import Mathlib.CategoryTheory.Sites.Coherent import Mathlib.Topology.Category.Profinite.Basic +import Profinite.Epi /-! # The category of profinite spaces is precoherent -# TODO - -Prove the theorem that the category of profinite spaces -is precoherent. - -/ namespace Profinite @@ -21,6 +17,20 @@ open CategoryTheory universe u -instance : Precoherent Profinite.{u} := sorry - -end Profinite \ No newline at end of file +instance : Precoherent Profinite.{u} := by + constructor + intro B₁ B₂ f α _ X₁ π₁ h₁ + refine ⟨α, inferInstance, fun a => pullback f (π₁ a), fun a => pullback.fst _ _, ?_, + id, fun a => pullback.snd _ _, ?_⟩ + · have := (effectiveEpiFamily_tfae _ π₁).out 0 2 ; rw [this] at h₁ ; clear this + have := (effectiveEpiFamily_tfae _ (fun a => pullback.fst f (π₁ a))).out 0 2 + rw [this] ; clear this + intro b₂ + obtain ⟨a,x,h⟩ := h₁ (f b₂) + refine ⟨a, ⟨⟨b₂, x⟩, h.symm⟩, rfl⟩ + · intro a + dsimp + ext ⟨⟨_,_⟩,h⟩ + exact h.symm + +end Profinite diff --git a/Profinite/Epi.lean b/Profinite/Epi.lean new file mode 100644 index 0000000..268eeef --- /dev/null +++ b/Profinite/Epi.lean @@ -0,0 +1,396 @@ +import Mathlib.Topology.Category.Profinite.Basic +import Mathlib.CategoryTheory.Sites.Coherent + +open CategoryTheory Limits + +universe u + +/-! +This section contains results that should probably go in a different file as they +do not work with `Profinite` at all. + +TODO: They also need proper naming +-/ +section Preliminaries + +/-- +The image of an open set under an isomorphism is open. +-/ +lemma TopCat.isOpen_iso {X Y : TopCat} {U : Set X} (f : X ≅ Y) (h : IsOpen U) : + IsOpen (f.hom '' U) := by + let ff := TopCat.homeoOfIso f + rw [← Homeomorph.isOpen_image ff] at h + assumption + +/-- +Isomorphisms preserve totally-disconnectedness. +-/ +lemma TotallyDisconnectedSpace.ofIso + {X Y : TopCat} [k : TotallyDisconnectedSpace X] (f : X ≅ Y) : + TotallyDisconnectedSpace Y := by + + have surj' : Function.Surjective f.hom + · apply (TopCat.homeoOfIso f).surjective + + have inj' : Function.Injective f.hom + · apply (TopCat.homeoOfIso f).injective + + constructor + unfold _root_.IsTotallyDisconnected + intro t _ ht₂ + + apply Set.subsingleton_of_preimage surj' + + replace k := k.isTotallyDisconnected_univ + unfold _root_.IsTotallyDisconnected at k + + apply k + + tauto + + apply IsPreconnected.preimage_of_open_map + assumption + assumption + · unfold IsOpenMap + intro U hU + apply TopCat.isOpen_iso _ hU + tauto + +end Preliminaries + +namespace Profinite + +/-! +This section defines the finite Coproduct of a finite family +of profinite spaces `X : α → Profinite.{u}` + +Notes: The content is mainly copied from +`Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean` +-/ +section FiniteCoproducts + +variable {α : Type} [Fintype α] (X : α → Profinite.{u}) + +/-- +The coproduct of a finite family of objects in `Profinite`, constructed as the disjoint +union with its usual topology. +-/ +def finiteCoproduct : Profinite := Profinite.of <| Σ (a : α), X a + +/-- +The inclusion of one of the factors into the explicit finite coproduct. +-/ +def finiteCoproduct.ι (a : α) : X a ⟶ finiteCoproduct X where + toFun := fun x => ⟨a,x⟩ + continuous_toFun := continuous_sigmaMk (σ := fun a => X a) + +/-- +To construct a morphism from the explicit finite coproduct, it suffices to +specify a morphism from each of its factors. +This is essentially the universal property of the coproduct. +-/ +def finiteCoproduct.desc {B : Profinite.{u}} (e : (a : α) → (X a ⟶ B)) : + finiteCoproduct X ⟶ B where + toFun := fun ⟨a,x⟩ => e a x + continuous_toFun := by + apply continuous_sigma + intro a ; exact (e a).continuous + +@[reassoc (attr := simp)] +lemma finiteCoproduct.ι_desc {B : Profinite.{u}} (e : (a : α) → (X a ⟶ B)) (a : α) : + finiteCoproduct.ι X a ≫ finiteCoproduct.desc X e = e a := rfl + +lemma finiteCoproduct.hom_ext {B : Profinite.{u}} (f g : finiteCoproduct X ⟶ B) + (h : ∀ a : α, finiteCoproduct.ι X a ≫ f = finiteCoproduct.ι X a ≫ g) : f = g := by + ext ⟨a,x⟩ + specialize h a + apply_fun (fun q => q x) at h + exact h + +/-- +The coproduct cocone associated to the explicit finite coproduct. +-/ +@[simps] +def finiteCoproduct.cocone : Limits.Cocone (Discrete.functor X) where + pt := finiteCoproduct X + ι := Discrete.natTrans fun ⟨a⟩ => finiteCoproduct.ι X a + +/-- +The explicit finite coproduct cocone is a colimit cocone. +-/ +@[simps] +def finiteCoproduct.isColimit : Limits.IsColimit (finiteCoproduct.cocone X) where + desc := fun s => finiteCoproduct.desc _ fun a => s.ι.app ⟨a⟩ + fac := fun s ⟨a⟩ => finiteCoproduct.ι_desc _ _ _ + uniq := fun s m hm => finiteCoproduct.hom_ext _ _ _ fun a => by + specialize hm ⟨a⟩ + ext t + apply_fun (fun q => q t) at hm + exact hm + +end FiniteCoproducts + +variable {X Y B : Profinite.{u}} (f : X ⟶ B) (g : Y ⟶ B) + +/-- +The pullback of two morphisms `f, g` in `Profinite`, constructed explicitly as the set of +pairs `(x, y)` such that `f x = g y`, with the topology induced by the product. +-/ +def pullback : Profinite.{u} := + let set := { xy : X × Y | f xy.fst = g xy.snd } + have : CompactSpace set := by + rw [← isCompact_iff_compactSpace] + apply IsClosed.isCompact + exact isClosed_eq (f.continuous.comp continuous_fst) (g.continuous.comp continuous_snd) + Profinite.of set + +/-- +The projection from the pullback to the first component. +-/ +def pullback.fst : pullback f g ⟶ X where + toFun := fun ⟨⟨x,_⟩,_⟩ => x + continuous_toFun := Continuous.comp continuous_fst continuous_subtype_val + +/-- +The projection from the pullback to the second component. +-/ +def pullback.snd : pullback f g ⟶ Y where + toFun := fun ⟨⟨_,y⟩,_⟩ => y + continuous_toFun := Continuous.comp continuous_snd continuous_subtype_val + +/-! +This section contains exclusively technical definitions and results that are used +in the proof of `Profinite.effectiveEpiFamily_of_jointly_surjective`. + +The construction of `QB` as a quotient of the maps `X a → B` is analoguous to the +construction in `CompHaus`, but one has to start with an equivalence relation +on `Profinite` instead. +-/ +namespace EffectiveEpiFamily + +-- Assume we have `X a → B` which are jointly surjective. +variable {α : Type} [Fintype α] {B : Profinite.{u}} + {X : α → Profinite.{u}} (π : (a : α) → (X a ⟶ B)) + (surj : ∀ b : B, ∃ (a : α) (x : X a), π a x = b) + +/-- +Implementation: This is a setoid on the explicit finite coproduct of `X` whose quotient +will be isomorphic to `B` provided that `X a → B` is an effective epi family. +-/ +def relation : Setoid (finiteCoproduct X) where + r a b := ∃ (Z : Profinite.{u}) (z : Z) + (fst : Z ⟶ X a.fst) (snd : Z ⟶ X b.fst), + fst ≫ π _ = snd ≫ π _ ∧ fst z = a.snd ∧ snd z = b.snd + iseqv := by + constructor + · rintro ⟨a,x⟩ + refine ⟨X a, x, 𝟙 _, 𝟙 _, by simp, rfl, rfl⟩ + · rintro ⟨a,x⟩ ⟨b,y⟩ ⟨Z,z,fst,snd,w,h1,h2⟩ + exact ⟨Z,z,snd,fst,w.symm,h2,h1⟩ + · rintro ⟨a,x⟩ ⟨b,y⟩ ⟨z,c⟩ ⟨Z, z,fstZ,sndZ,hZ,hZ1,hZ2⟩ + rintro ⟨W,w,fstW,sndW,hW,hW1,hW2⟩ + refine ⟨pullback sndZ fstW, ⟨⟨z,w⟩, by dsimp; rw [hZ2, hW1]⟩, + pullback.fst _ _ ≫ fstZ, pullback.snd _ _ ≫ sndW, ?_, hZ1, hW2⟩ + dsimp at * + simp only [Category.assoc, hZ, ← hW] + apply ContinuousMap.ext + rintro ⟨⟨u,v⟩,h⟩ + change π b (sndZ u) = π b (fstW v) + rw [h] + +/-- +Implementation: the map from the quotient of `relation π` to `B`, which will eventually +become the function underlying an isomorphism, provided that `X a → B` is an effective epi family. +-/ +def ιFun : Quotient (relation π) → B := + Quotient.lift (fun ⟨a,x⟩ => π a x) <| by + rintro ⟨a,x⟩ ⟨b,y⟩ ⟨Z,z,fst,snd,h,hx,hy⟩ + dsimp at * + rw [← hx, ← hy] + apply_fun (fun t => t z) at h + exact h + +lemma ιFun_continuous : Continuous (ιFun π) := by + apply Continuous.quotient_lift + apply continuous_sigma + intro a + exact (π a).continuous + +lemma ιFun_injective : (ιFun π).Injective := by + rintro ⟨⟨a,x⟩⟩ ⟨⟨b,y⟩⟩ (h : π _ _ = π _ _) + apply Quotient.sound' + refine ⟨pullback (π a) (π b), ⟨⟨x,y⟩,h⟩, pullback.fst _ _, pullback.snd _ _, ?_, rfl, rfl⟩ + ext ⟨_, h⟩ ; exact h + +lemma ιFun_surjective : (ιFun π).Surjective := by + intro b + obtain ⟨a,x,h⟩ := surj b + refine ⟨Quotient.mk _ ⟨a,x⟩, h⟩ + +lemma ιFun_bijective : (ιFun π).Bijective := ⟨ιFun_injective π, ιFun_surjective π surj⟩ + +/-- Implementation: The quotient of `relation π`, considered as an object of `CompHaus`. -/ +def QB₁ : CompHaus.{u} := + haveI : T2Space (Quotient <| relation π) := + ⟨fun _ _ h => separated_by_continuous (ιFun_continuous π) <| (ιFun_injective π).ne h ⟩ + CompHaus.of (Quotient <| relation π) + +/-- Implementation: The function `ιFun`, considered as a morphism in `CompHaus`. -/ +def ι₁Hom : (QB₁ π) ⟶ B.toCompHaus := ⟨ιFun π, ιFun_continuous π⟩ + +/-- Implementation: `ιFun` as isomorphism in `CompHaus`. -/ +noncomputable +def ι₁Iso : (QB₁ π) ≅ B.toCompHaus := + have : IsIso (ι₁Hom π) := by + apply CompHaus.isIso_of_bijective + refine ⟨ιFun_injective _, ?_⟩ + intro b + obtain ⟨a,x,h⟩ := surj b + refine ⟨Quotient.mk _ ⟨a,x⟩, h⟩ + asIso (ι₁Hom π) + +lemma CompHaus.TotallyDisconnectedSpace_ofIsIso + {X Y : CompHaus} [k : TotallyDisconnectedSpace X] (f : X ≅ Y) : + TotallyDisconnectedSpace Y := by + have f : X.toTop ≅ Y.toTop + · exact compHausToTop.mapIso f + apply TotallyDisconnectedSpace.ofIso f + +/-- Implementation: The quotient of `relation π`, considered as an object of `Profinite`. -/ +def QB₂ : Profinite.{u} where + toCompHaus := QB₁ π + IsTotallyDisconnected := CompHaus.TotallyDisconnectedSpace_ofIsIso (ι₁Iso π surj).symm + +/-- Implementation: The function `ιFun`, considered as a morphism in `Profinite`. -/ +def ι₂Hom : (QB₂ π surj) ⟶ B := ⟨ιFun π, ιFun_continuous π⟩ + +/-- Implementation: `ιFun` as isomorphism in `CompHaus`. -/ +noncomputable +def ι₂Iso : (QB₂ π surj) ≅ B := + have : IsIso (ι₂Hom π surj) := by + apply Profinite.isIso_of_bijective + refine ⟨ιFun_injective _, ?_⟩ + intro b + obtain ⟨a,x,h⟩ := surj b + refine ⟨Quotient.mk _ ⟨a,x⟩, h⟩ + asIso (ι₂Hom π surj) + +/-- Implementation: The family of morphisms `X a ⟶ QB` which will be shown to be effective epi. -/ +def π' : (a : α) → (X a ⟶ QB₂ π surj) := fun a => + { toFun := fun x => Quotient.mk _ ⟨a, x⟩ + continuous_toFun := by + apply Continuous.comp + apply continuous_quot_mk + apply continuous_sigmaMk (σ := fun a => X a) } + +/-- Implementation: The family of morphisms `X a ⟶ QB` is an effective epi. -/ +def structAux : EffectiveEpiFamilyStruct X (π' π surj) where + desc := fun {W} e h => { + toFun := Quotient.lift (fun ⟨a,x⟩ => e a x) <| by + rintro ⟨a,x⟩ ⟨b,y⟩ ⟨Z,z,fst,snd,hh,hx,hy⟩ + dsimp at * + rw [← hx, ← hy] + specialize h _ _ fst snd ?_ + · ext z + apply ιFun_injective + apply_fun (fun q => q z) at hh + exact hh + apply_fun (fun q => q z) at h + exact h + continuous_toFun := by + apply Continuous.quotient_lift + apply continuous_sigma + intro a + exact (e a).continuous } + fac := by intro Z e h a ; ext ; rfl + uniq := by + intro Z e h m hm + ext ⟨⟨a,x⟩⟩ + specialize hm a + apply_fun (fun q => q x) at hm + exact hm + +@[reassoc] +lemma π'_comp_ι_hom (a : α) : π' π surj a ≫ (ι₂Iso π surj).hom = π a := by + ext + rfl + +@[reassoc] +lemma π_comp_ι_inv (a : α) : π a ≫ (ι₂Iso π surj).inv = π' π surj a := by + rw [Iso.comp_inv_eq] + exact π'_comp_ι_hom _ surj _ + +/-- +Implementation: The family `X` is an effective epi, provided that `π` are jointly surjective. +The theorem `Profinite.effectiveEpiFamily_tfae` should be used instead. +-/ +noncomputable +def struct : EffectiveEpiFamilyStruct X π where + desc := fun {W} e h => (ι₂Iso π surj).inv ≫ (structAux π surj).desc e (fun {Z} a₁ a₂ g₁ g₂ hh => by + apply h + rw [← cancel_mono (ι₂Iso _ surj).inv] + simpa only [Category.assoc, π_comp_ι_inv]) + fac := by + intro W e h a + simp only [Eq.ndrec, id_eq, eq_mpr_eq_cast, π_comp_ι_inv_assoc, (structAux π surj).fac] + uniq := by + intro W e h m hm + dsimp + rw [Iso.eq_inv_comp] + apply (structAux π surj).uniq + intro a + simpa using hm a + +end EffectiveEpiFamily + +/-- One direction of `Profinite.effectiveEpiFamily_tfae` -/ +theorem effectiveEpiFamily_of_jointly_surjective + {α : Type} [Fintype α] {B : Profinite.{u}} + (X : α → Profinite.{u}) (π : (a : α) → (X a ⟶ B)) + (surj : ∀ b : B, ∃ (a : α) (x : X a), π a x = b) : + EffectiveEpiFamily X π := + ⟨⟨Profinite.EffectiveEpiFamily.struct π surj⟩⟩ + +open List in +/-- +For a finite family of profinite spaces `πₐ : Xₐ → B` the following are equivalent: +* they are an effective epi family +* the map `∐ πₐ ⟶ B` is an epimorphism +* they are jointly surjective +-/ +theorem effectiveEpiFamily_tfae {α : Type} [Fintype α] {B : Profinite.{u}} + (X : α → Profinite.{u}) + (π : (a : α) → (X a ⟶ B)) : + TFAE [ + EffectiveEpiFamily X π, + Epi (Limits.Sigma.desc π), + ∀ (b : B), ∃ (a : α) (x : X a), π a x = b + ] := by + tfae_have 1 → 2 + · intro + infer_instance + tfae_have 2 → 3 + · intro e + rw [epi_iff_surjective] at e + let i : ∐ X ≅ finiteCoproduct X := + (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _) + intro b + obtain ⟨t,rfl⟩ := e b + let q := i.hom t + refine ⟨q.1,q.2,?_⟩ + have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id] ; rfl + rw [this] + show _ = (i.inv ≫ Sigma.desc π) (i.hom t) + suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by + rw [this] ; rfl + rw [Iso.inv_comp_eq] + apply colimit.hom_ext + rintro ⟨a⟩ + simp only [Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, + colimit.comp_coconePointUniqueUpToIso_hom_assoc] + ext ; rfl + tfae_have 3 → 1 + · apply effectiveEpiFamily_of_jointly_surjective + tfae_finish + +end Profinite diff --git a/TopCat.lean b/TopCat.lean new file mode 100644 index 0000000..e69de29 diff --git a/TopCat/toCondensed.lean b/TopCat/toCondensed.lean new file mode 100644 index 0000000..fbe3aef --- /dev/null +++ b/TopCat/toCondensed.lean @@ -0,0 +1,40 @@ +import Mathlib.Condensed.Abelian + +#check Condensed + +open CategoryTheory + +universe u + +def TopCat.ulift' : TopCat.{u} ⥤ TopCat.{u+1} where + obj X := of (ULift.{u+1} X) + map f := sorry + map_id := sorry + map_comp := sorry + + + +def TopCat.toCondensed : TopCat.{u+1} ⥤ Condensed.{u} (Type (u+1)) where + obj X := { + val := (compHausToTop : CompHaus ⥤ TopCat.{u}).op ⋙ + (sorry : TopCat.{u} ⥤ TopCat.{u+1}).op ⋙ + (yoneda.obj X : TopCat.{u+1}ᵒᵖ ⥤ Type (u+1)) + cond := sorry -- sheaf condition + } + map := sorry -- data + map_id := sorry -- proof + map_comp := sorry -- proof + +#check whiskerRight + +theorem CompHausCondIsSheaf : + Presheaf.IsSheaf (coherentTopology CompHaus) (yoneda.obj X ⋙ uliftFunctor) := by + -- now Adam takes over + sorry + +def CompHaus.toCondensed : CompHaus.{u} ⥤ Condensed.{u} (Type (u+1)) where + obj X := { + val := yoneda.obj X ⋙ (uliftFunctor.{u+1} : Type u ⥤ Type (u+1)) + cond := CompHausCondIsSheaf -- sheaf condition + } + map f := ⟨whiskerRight (yoneda.map f) _⟩ \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index dbc1516..ced0fb3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -28,7 +28,7 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "b5ebe913f3c6cbfc67d97b5b1b78ff4bacaa9116", + "rev": "b2f1e713f2fd8be8074ff6d062a5a4ab3d5aa593", "name": "mathlib", "inputRev?": null}}, {"git": diff --git a/lakefile.lean b/lakefile.lean index e602254..1850084 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,6 +14,7 @@ require find_with_gpt from git @[default_target] lean_lib «CopenhagenMasterclass2023» { globs := #[ + .andSubmodules `TopCat, .andSubmodules `Condensed, .andSubmodules `Profinite, .andSubmodules `ExtrDisc,