From 302a39725716fbdfffb1b7eb4d09f7e45732c84e Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Fri, 20 Jun 2025 17:58:31 +0200 Subject: [PATCH 01/13] All except finite coproducts --- .../Mathlib/CategoryTheory/Countable.lean | 13 + LeanCondensed/Projects/Epi.lean | 157 +++++ LeanCondensed/Projects/Initial.lean | 29 + LeanCondensed/Projects/OverN.lean | 46 ++ LeanCondensed/Projects/PreservesCoprod.lean | 20 + LeanCondensed/Projects/PreservesEpi.lean | 108 ++++ LeanCondensed/Projects/Proj.lean | 538 ++++++++++++++++++ LeanCondensed/Projects/Pullbacks.lean | 274 +++++++++ LeanCondensed/Projects/test.lean | 18 + 9 files changed, 1203 insertions(+) create mode 100644 LeanCondensed/Mathlib/CategoryTheory/Countable.lean create mode 100644 LeanCondensed/Projects/Epi.lean create mode 100644 LeanCondensed/Projects/Initial.lean create mode 100644 LeanCondensed/Projects/OverN.lean create mode 100644 LeanCondensed/Projects/PreservesCoprod.lean create mode 100644 LeanCondensed/Projects/PreservesEpi.lean create mode 100644 LeanCondensed/Projects/Proj.lean create mode 100644 LeanCondensed/Projects/Pullbacks.lean create mode 100644 LeanCondensed/Projects/test.lean diff --git a/LeanCondensed/Mathlib/CategoryTheory/Countable.lean b/LeanCondensed/Mathlib/CategoryTheory/Countable.lean new file mode 100644 index 0000000..0fe12f6 --- /dev/null +++ b/LeanCondensed/Mathlib/CategoryTheory/Countable.lean @@ -0,0 +1,13 @@ +import Mathlib.CategoryTheory.Countable + +universe u + +noncomputable section + +open CategoryTheory Quiver Countable + +instance {J : Type u} [ctble : Countable J] [Category J] [thin : Quiver.IsThin J]: CountableCategory J := + CountableCategory.mk ctble (fun _ _ ↦ ⟨fun _ ↦ 0, fun _ _ _ ↦ (thin _ _).elim _ _⟩) + +noncomputable instance {J : Type u} [fin : Finite J] [Category J] [thin : Quiver.IsThin J] : FinCategory J := by + apply FinCategory.mk (Fintype.ofFinite J) (fun j j' ↦ Fintype.ofFinite (j ⟶ j')) diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean new file mode 100644 index 0000000..604b100 --- /dev/null +++ b/LeanCondensed/Projects/Epi.lean @@ -0,0 +1,157 @@ +import Mathlib + +import LeanCondensed.Mathlib.CategoryTheory.Countable +import LeanCondensed.Projects.Pullbacks + +open Function CategoryTheory Limits Opposite + +universe u + +lemma surj_pullback' {X Y Z : LightProfinite.{u}} (f : X ⟶ Z) {g : Y ⟶ Z} + (hf : Function.Surjective f) : Function.Surjective ↑(pullback.snd f g) := by + intro y + + let point : LightProfinite.{u} := LightProfinite.of PUnit + let point_map : point ⟶ Y := TopCat.ofHom ⟨fun _ ↦ y, continuous_const⟩ + + rcases hf (g y) with ⟨z, hz⟩ + + let point_map' : point ⟶ X := TopCat.ofHom ⟨fun _ ↦ z, continuous_const⟩ + + use pullback.lift point_map' point_map (by ext; erw [hz]; rfl) PUnit.unit + + rw [←ConcreteCategory.comp_apply, pullback.lift_snd] + rfl + +instance surj_widePullback {J : Type*} (B : LightProfinite.{u}) (objs : J → LightProfinite) + (arrows: (j : J) → (objs j ⟶ B)) (hepi : ∀ j, Epi (arrows j)) [HasWidePullback B objs arrows] + : ∀ j, Epi (WidePullback.π arrows j) := by + classical + intro i + simp [LightProfinite.epi_iff_surjective] at ⊢ hepi + intro xi + let point : LightProfinite.{u} := LightProfinite.of PUnit + let base_pt : B := arrows i xi + have choice : ∀ j, ∃ xj, arrows j xj = base_pt := fun j ↦ hepi j base_pt + let point_maps : (j : J) → (point ⟶ objs j) := (fun j ↦ + if h : i = j then + CompHausLike.ofHom _ (ContinuousMap.const point (h ▸ xi)) + else + (CompHausLike.ofHom _ (ContinuousMap.const point (choice j).choose)) + ) + let lift : point ⟶ widePullback B objs arrows := + WidePullback.lift (CompHausLike.ofHom _ (ContinuousMap.const point base_pt)) point_maps + ( + by + intro j + unfold point_maps + by_cases h : i = j + · simp only [↓reduceDIte] + rw [dif_pos h] + subst h + rfl + · rw [dif_neg h] + ext x + simp only [ConcreteCategory.comp_apply, CompHausLike.hom_ofHom, ContinuousMap.const_apply] + exact (choice j).choose_spec + ) + use lift PUnit.unit + rw [←ConcreteCategory.comp_apply, WidePullback.lift_π] + simp [point_maps] + + + + +instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := { + preserves f hf := (LightCondSet.epi_iff_locallySurjective_on_lightProfinite _).mpr + fun _ g ↦ + ⟨ + pullback f g, + pullback.snd _ _, + surj_pullback' f ((LightProfinite.epi_iff_surjective f).mp hf), + pullback.fst _ _, + pullback.condition + ⟩ +} + +lemma abc {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y + := congr_arg (fun (a : s) ↦ (↑a : A)) h + +noncomputable def regular {X Y : LightProfinite} (π : X ⟶ Y) + : Cofork (lightProfiniteToLightCondSet.map <| pullback.fst π π) (lightProfiniteToLightCondSet.map <| pullback.snd π π) := Cofork.ofπ (lightProfiniteToLightCondSet.map <| π) (by + rw [ + ←lightProfiniteToLightCondSet.map_comp, + ←lightProfiniteToLightCondSet.map_comp, + pullback.condition + ]) + +def cfork {X Y : LightProfinite} (π : X ⟶ Y) + := Cofork (lightProfiniteToLightCondSet.map (pullback.fst π π)) (lightProfiniteToLightCondSet.map (pullback.snd π π)) + +noncomputable def regularLiftElem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] + (cone : cfork π) : cone.pt.val.obj (op Y) + := + let fX := yonedaEquiv cone.π.val + have : cone.pt.val.map (pullback.fst π π).op fX = cone.pt.val.map (pullback.snd π π).op fX := by + have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl + have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl + + erw [ + yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π), + yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π), + ←this, ←this', + cone.condition, + ] + (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨fX, this⟩).choose + +private lemma cone_elem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) + : cone.pt.val.map (pullback.fst π π).op (yonedaEquiv cone.π.val) = cone.pt.val.map (pullback.snd π π).op (yonedaEquiv cone.π.val) := by + have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl + have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl + erw [ + yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π), + yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π), + ←this, ←this', + cone.condition, + ] + +noncomputable def regularLift {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) : lightProfiniteToLightCondSet.obj Y ⟶ cone.pt + := ⟨ yonedaEquiv.symm (regularLiftElem π cone) ⟩ + +private lemma regularLift_prop {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) + : regularTopology.MapToEqualizer cone.pt.val π (pullback.fst π π) (pullback.snd π π) pullback.condition (regularLiftElem π cone) = ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩ + := (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩).choose_spec + +lemma regularLift_comp {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) + : (regular π).π ≫ regularLift π cone = cone.π := by + refine Sheaf.Hom.ext (yonedaEquiv.injective ?_) + erw [←yonedaEquiv_naturality (F := cone.pt.val), Equiv.apply_symm_apply] + exact abc (s := {x : cone.pt.val.obj (Opposite.op X) | cone.pt.val.map (pullback.fst π π).op x = cone.pt.val.map (pullback.snd π π).op x}) (regularLift_prop π cone) + +lemma regularLift_unique {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) + (m : (lightProfiniteToLightCondSet.obj Y) ⟶ cone.pt) (hm : (regular π).π ≫ m = cone.π) + : m = regularLift π cone := by + erw [Cofork.π_ofπ, ←regularLift_comp π cone] at hm + exact Epi.left_cancellation _ _ hm + +noncomputable abbrev regular_IsColimit {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] + : IsColimit (regular π) + := Cofork.IsColimit.mk _ (regularLift π) (regularLift_comp π) (regularLift_unique π) + +noncomputable abbrev regular_RegularEpi {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] + : RegularEpi (lightProfiniteToLightCondSet.map π) where + W := lightProfiniteToLightCondSet.obj (pullback π π) + left := lightProfiniteToLightCondSet.map (pullback.fst π π) + right := lightProfiniteToLightCondSet.map (pullback.snd π π) + w := by + rw [ + ←lightProfiniteToLightCondSet.map_comp, + ←lightProfiniteToLightCondSet.map_comp, + pullback.condition + ] + isColimit := regular_IsColimit π + +instance : lightProfiniteToLightCondSet.PreservesEffectiveEpis where + preserves π _ := + have : RegularEpi (lightProfiniteToLightCondSet.map π) := regular_RegularEpi π + inferInstance diff --git a/LeanCondensed/Projects/Initial.lean b/LeanCondensed/Projects/Initial.lean new file mode 100644 index 0000000..948e936 --- /dev/null +++ b/LeanCondensed/Projects/Initial.lean @@ -0,0 +1,29 @@ +import Mathlib + +open CategoryTheory Limits Condensed + +universe u + +def empty_elim {p : Sort u} {X : LightProfinite} (hX : ¬Nonempty X) (x : X) : p := (hX ⟨x⟩).elim + +def empty_subset {X : LightProfinite} (hX : ¬Nonempty X) (s : Set X) : s = ⊤ := by + ext x + exact empty_elim hX x + +def empty_map {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : ¬Nonempty X + := fun h ↦ h.elim (fun x ↦ hY ⟨f x⟩) + +def empty_iso {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : IsIso f := by + let finv : Y ⟶ X := CompHausLike.ofHom _ { + toFun y := empty_elim hY y + continuous_toFun := by + apply Continuous.mk + intro s empty_elim + rw [empty_subset hY ((fun y ↦ _root_.empty_elim hY y) ⁻¹' s)] + exact TopologicalSpace.isOpen_univ + } + apply IsIso.mk + use finv + constructor <;> ext x + exact empty_elim hY (f x) + exact empty_elim hY x diff --git a/LeanCondensed/Projects/OverN.lean b/LeanCondensed/Projects/OverN.lean new file mode 100644 index 0000000..3d8ccaa --- /dev/null +++ b/LeanCondensed/Projects/OverN.lean @@ -0,0 +1,46 @@ +import Mathlib +import LeanCondensed.Projects.Pullbacks + +open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed + MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom + ChosenFiniteProducts + + +lemma IsClosedThingy {T : LightProfinite} (f : T ⟶ ℕ∪{∞}) (s : ℕ → Set T) + (hs : ∀ n (x : s n), f x = n) (hs' : ∀ n, IsClosed (s n)) : IsClosed ({t | f t = ∞} ∪ ⋃ n, s n) := by + apply IsClosed.mk + let fibre : ℕ → Set T := fun n ↦ f ⁻¹' {OnePoint.some n} + have clopen : ∀ n, IsClopen (fibre n) := by + intro n + refine IsClopen.preimage ⟨isClosed_singleton, ?_⟩ f.1.continuous + rw [isOpen_def] + refine ⟨fun h ↦ by simp at h, trivial⟩ + have : ({t | f t = ∞} ∪ ⋃ n, s n)ᶜ = ⋃ n, (s n)ᶜ ∩ fibre n := by + ext x + simp only [Set.compl_union, Set.compl_iUnion, Set.mem_inter_iff, Set.mem_compl_iff, + Set.mem_setOf_eq, Set.mem_iInter, Set.mem_iUnion] + constructor + · intro ⟨h, h'⟩ + obtain ⟨n', hn⟩ := Option.ne_none_iff_exists'.mp h + exact ⟨n', h' n', hn⟩ + · intro ⟨n, hn, hn'⟩ + refine ⟨?_, ?_⟩ + rw [hn'] + simp + intro i + by_cases h : i = n + rw [h] + exact hn + intro h' + have := hs i ⟨x, h'⟩ + apply h + simp [fibre] at hn' + rw [hn'] at this + rw [OnePoint.coe_eq_coe] at this + symm + exact this + rw [this] + refine isOpen_iUnion (fun i ↦ ?_) + apply IsOpen.inter + exact (hs' i).1 + exact (clopen i).2 diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean new file mode 100644 index 0000000..aa55e64 --- /dev/null +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -0,0 +1,20 @@ +import Mathlib + +open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed + MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom + ChosenFiniteProducts Topology + +def coprod_desc {n : ℕ} {K : Discrete (Fin n) ⥤ LightProfinite} {c : Cocone K} + (hc : IsColimit c) (s : Cocone (K ⋙ lightProfiniteToLightCondSet)) + : c.pt.toCondensed ⟶ s.pt := sorry + +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where + preserves n := { + preservesColimit {K} := { + preserves {c} hc := ⟨{ + desc s := coprod_desc hc s + fac := sorry + uniq := sorry + }⟩ + } + } diff --git a/LeanCondensed/Projects/PreservesEpi.lean b/LeanCondensed/Projects/PreservesEpi.lean new file mode 100644 index 0000000..fe30c20 --- /dev/null +++ b/LeanCondensed/Projects/PreservesEpi.lean @@ -0,0 +1,108 @@ +import Mathlib + +import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono +import LeanCondensed.Projects.LightProfiniteInjective + + +universe u v + +open CategoryTheory Category Preadditive LightProfinite OnePoint Limits LightCondensed + +variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C] + +class InternallyProjective (P : C) : Prop where + preserves_epi : (ihom P).PreservesEpimorphisms + +namespace InternallyProjective + +theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X) + : InternallyProjective Y := + haveI : Retract (ihom Y) (ihom X) := { + i := MonoidalClosed.pre r.r + r := MonoidalClosed.pre r.i + retract := by + rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id] + } + InternallyProjective.mk <| preservesEpi_ofRetract this proj.preserves_epi + +end InternallyProjective + +open LightCondensed + +variable (R : Type _) [CommRing R] + +instance : TotallyDisconnectedSpace PUnit := by + have := TotallySeparatedSpace.of_discrete + apply TotallySeparatedSpace.totallyDisconnectedSpace + +def pt := LightProfinite.of PUnit.{1} + +def ι : pt ⟶ ℕ∪{∞} := (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) + +instance : Mono ι := (CompHausLike.mono_iff_injective ι).mpr fun _ _ ↦ congrFun rfl + +instance : Nonempty pt := by + unfold pt + infer_instance + +noncomputable def ι_SplitMono : SplitMono ι where + retraction := ((injective_of_light (LightProfinite.of PUnit.{1})).factors (𝟙 pt) ι).choose + id := ((injective_of_light pt).factors _ _).choose_spec + +noncomputable def P_map : + (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed := + (lightProfiniteToLightCondSet ⋙ free R).map (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) + +noncomputable def ιSplit : SplitMono (P_map R) := SplitMono.map ι_SplitMono (lightProfiniteToLightCondSet ⋙ (free R)) + +noncomputable def P : LightCondMod R := cokernel (P_map R) + +noncomputable def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _ + +noncomputable def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A) + (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf + +noncomputable def xyz := (Preadditive.homGroup _ _).sub (𝟙 (free R).obj (ℕ∪{∞}).toCondensed) ((ιSplit R).retraction ≫ ((lightProfiniteToLightCondSet ⋙ free R).map ι)) + +lemma comp_zero : P_map R ≫ xyz R = 0 := by + erw [ + Preadditive.comp_sub, + comp_id, + Functor.comp_map, + SplitMono.id_assoc, + sub_eq_zero + ] + rfl + +instance P_proj_Epi : Epi (P_proj R) := by + unfold P_proj + rw [←coequalizer_as_cokernel] + exact coequalizer.π_epi + +noncomputable def πSplit : SplitEpi (P_proj R) where + section_ := P_homMk R ((free R).obj (ℕ∪{∞}).toCondensed) (xyz R) (comp_zero _) + id := by + apply (P_proj_Epi R).left_cancellation + erw [ + ←assoc _ (cokernel.desc (P_map R) (xyz R) (comp_zero _)) _, + cokernel.π_desc, + sub_comp, + id_comp, + assoc, + cokernel.condition, + HasZeroMorphisms.comp_zero, + sub_zero + ] + +noncomputable def r : Retract (P R) ((free R).obj ℕ∪{∞}.toCondensed) where + i := (πSplit R).section_ + r := P_proj R + retract := (πSplit R).id + +instance : MonoidalCategory (LightCondMod.{u} R) := sorry + +instance : MonoidalClosed (LightCondMod.{u} R) := sorry + +instance qwerty : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry + +theorem qwerty' : InternallyProjective (P R) := (qwerty _).ofRetract (r _) diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean new file mode 100644 index 0000000..a4b1053 --- /dev/null +++ b/LeanCondensed/Projects/Proj.lean @@ -0,0 +1,538 @@ +import LeanCondensed.Projects.Epi +import LeanCondensed.Projects.LightProfiniteInjective +import LeanCondensed.Projects.Initial +import LeanCondensed.Projects.OverN +import LeanCondensed.Projects.InternallyProjective +import LeanCondensed.Mathlib.CategoryTheory.Countable +import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts +import LeanCondensed.Projects.Pullbacks +import Mathlib + +open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed + MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom + ChosenFiniteProducts Topology + +universe u + +variable (R : Type) [CommRing R] + +instance : TotallyDisconnectedSpace PUnit := by + have := TotallySeparatedSpace.of_discrete + apply TotallySeparatedSpace.totallyDisconnectedSpace + +@[simps!] +def CategoryTheory.Limits.parallelPair.hom {C : Type*} [Category C] + {F G : WalkingParallelPair ⥤ C} (zero : F.obj zero ⟶ G.obj zero) + (one : F.obj one ⟶ G.obj one) (left : F.map left ≫ one = zero ≫ G.map left) + (right : F.map right ≫ one = zero ≫ G.map right) : F ⟶ G := { + app := (by + rintro ⟨j⟩ + exacts [zero, one]) + naturality := (by rintro _ _ ⟨_⟩ <;> simp [left, right]) + } + +set_option maxHeartbeats 500000 +noncomputable def smart_cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : coprod T (explicitPullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)) ⟶ explicitPullback π π := + coprod.desc + (explicitPullback.diagonal π : T ⟶ explicitPullback π π) + ( + explicitPullback.map + (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) + π π + (fibre_incl ∞ (π ≫ snd S ℕ∪{∞})) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞})) (𝟙 _) + (by rw [Category.comp_id]) (by rw [Category.comp_id]) + : explicitPullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ⟶ explicitPullback π π + ) + +lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hepi : Epi π] + {σ' : ℕ∪{∞} → (S ⟶ T)} (hσ : ∀ n, σ' n ≫ π ≫ fst _ _ = 𝟙 _) + (hσ' : ∀ n s, (σ' n ≫ π ≫ snd S ℕ∪{∞}) s = ↑n) + : ∃ (T' : LightProfinite) (i : T' ⟶ T), + Epi (i ≫ π) ∧ Epi (smart_cover (i ≫ π)) + ∧ IsSplitEpi + (fibre_incl ∞ ((i ≫ π) ≫ snd _ _) ≫ i ≫ π ≫ fst S ℕ∪{∞}) := by + + let space : Set T := + Set.iUnion (fun (n : ℕ) ↦ Set.range (σ' (OnePoint.some n))) ∪ {t : T | (π ≫ snd _ _) t = ∞} + have : IsClosed space := by + unfold space + rw [Set.union_comm] + apply IsClosedThingy + intro n ⟨x, ⟨s, hs⟩⟩ + simp only [←hs, ←ConcreteCategory.comp_apply, Category.assoc] + exact hσ' n s + exact fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous) + + let T' : LightProfinite := ⟨TopCat.of space, inferInstance, inferInstance⟩ + + let i : T' ⟶ T := + CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩ + + have : Mono i := by + rw [CompHausLike.mono_iff_injective] + exact Subtype.val_injective + + let σ : ℕ∪{∞} → (S ⟶ T') := fun n ↦ (CompHausLike.ofHom _ + ⟨ + fun s ↦ ⟨σ' n s, + by + rcases n with (n | n) + · apply Or.inr + simp only [Set.mem_setOf_eq, ←ConcreteCategory.comp_apply]; + exact hσ' ∞ s + · apply Or.inl + rw [Set.mem_iUnion] + exact ⟨n, s, rfl⟩ + ⟩, + by + have : IsInducing i := by exact { eq_induced := rfl } + rw [IsInducing.continuous_iff this] + exact (σ' n).1.continuous + ⟩) + + have hσ'' : ∀ (n : ℕ∪{∞}) (t : T'), t ∈ Set.range (σ n) → (i ≫ π ≫ fst _ _ ≫ σ n) t = t := by + intro n t ht + obtain ⟨s, hs⟩ := ht + rw (config := { occs := .pos [1]}) [←hs] + rw [ + ←ConcreteCategory.comp_apply, + ←Category.assoc π, + ←Category.assoc i, + ←Category.assoc (σ n), + ] + erw [hσ] + rw [Category.id_comp, hs] + + have coe_i : ∀ (t : T'), ↑t = i t := fun _ ↦ rfl + + have σ_i : ∀ n, σ' n = σ n ≫ i := fun n ↦ rfl + + have hT' : ∀ (n : ℕ) t, t ∈ Set.range (σ n) ↔ (i ≫ π ≫ snd _ _) t = n := by + intro n t' + constructor <;> intro h + · obtain ⟨_, ht⟩ := h + rw [←ht, ←ConcreteCategory.comp_apply] + erw [hσ'] + · rcases t'.2 with (fin | inf) + · rw [Set.mem_iUnion] at fin + obtain ⟨j, ⟨s, hs⟩⟩ := fin + suffices h' : j = n by + rw [h'] at hs + use s + exact Subtype.ext hs + rw [coe_i] at hs + rw [ConcreteCategory.comp_apply, ←hs, ←ConcreteCategory.comp_apply, hσ'] at h + rw [←OnePoint.coe_eq_coe] + exact h + · simp only [Set.mem_setOf_eq] at inf + erw [inf] at h + exact (Option.some_ne_none n (Eq.symm h)).elim + + refine ⟨T', i, ?_, ?_, ?_⟩ + · rw [LightProfinite.epi_iff_surjective] + rintro ⟨s, (n | n)⟩ + obtain ⟨t, ht⟩ := (LightProfinite.epi_iff_surjective π).mp hepi ⟨s, none⟩ + have : t ∈ space := by apply Or.inr; rw [Set.mem_setOf_eq, ConcreteCategory.comp_apply, ht]; rfl + use ⟨t, this⟩ + rw [←ht] + rfl + · use σ n s + apply Prod.ext + change ConcreteCategory.hom (σ' n ≫ π ≫ fst _ _) s = s + rw [hσ]; rfl + change ConcreteCategory.hom (σ' n ≫ π ≫ snd _ _) s = (OnePoint.some n) + rw [hσ'] + · rw [LightProfinite.epi_iff_surjective] + intro ⟨⟨t,t'⟩, ht⟩ + by_cases h : (i ≫ π ≫ snd _ _) t = ∞ + · unfold smart_cover + have : (i ≫ π ≫ snd _ _) t' = ∞ := by + rw [←Category.assoc, ConcreteCategory.comp_apply, ←ht, + ←ConcreteCategory.comp_apply, Category.assoc, h + ] + let x : explicitPullback (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) + (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) := + ⟨⟨⟨t, h⟩, ⟨t', this⟩⟩, + by + simp only [Set.mem_setOf_eq] + rw [ConcreteCategory.comp_apply (fibre_incl _ _), ConcreteCategory.comp_apply (fibre_incl _ _)] + unfold fibre_incl + simp only [CompHausLike.hom_ofHom, ContinuousMap.coe_mk] + exact ht + ⟩ + let p := coprod.inr (X := T') (Y := (explicitPullback _ _)) x + use coprod.inr (X := T') (Y := (explicitPullback _ _)) x + rw [←ConcreteCategory.comp_apply] + simp only [←Category.assoc, coprod.inr_desc] + rfl + · rw [←ne_eq, OnePoint.ne_infty_iff_exists] at h + obtain ⟨n, hn⟩ := h + symm at hn + use coprod.inl (X := T') (Y := (explicitPullback _ _)) ((i ≫ π ≫ fst _ _ ≫ σ n) t) + unfold smart_cover + simp only [←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc] + rw [ + ←Category.assoc (fst _ _), ←Category.assoc π, ←Category.assoc i, + ConcreteCategory.comp_apply + ] + rw [hσ''] + · apply Subtype.ext + apply Prod.ext (by rfl) + change t = t' + have hn' : (ConcreteCategory.hom (i ≫ π ≫ snd S ℕ∪{∞})) t' = n := by + rw [←hn] + rw [ + ←Category.assoc, + ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (i ≫ π), + ht + ] + rw [←hT'] at hn hn' + obtain ⟨s, hs⟩ := hn + obtain ⟨s', hs'⟩ := hn' + rw [←hs, ←hs'] + apply congr_arg + rw [←ConcreteCategory.id_apply s, ←ConcreteCategory.id_apply s'] + erw [←hσ n, σ_i] + simp only [Category.assoc] + erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (σ n), + hs, hs' + ] + erw [←Category.assoc, ConcreteCategory.comp_apply,ConcreteCategory.comp_apply (i ≫ π), ht] + rfl + · rw [hT'] + exact hn + · have : σ ∞ ≫ i = σ' ∞ := rfl + + let σσ : S ⟶ fibre ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) := + fibreLift ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞) + + exact ⟨⟨ + σσ, + by + simp only [←Category.assoc] + rw [ + fibreLift_comp ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞), + ] + erw [hσ] + ⟩⟩ + +lemma xyz { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] + : ∃ (S' T' : LightProfinite) (y' : S' ⟶ S) (π' : T' ⟶ S' ⊗ ℕ∪{∞}) (g' : T' ⟶ T), + Epi π' + ∧ Epi y' + ∧ π' ≫ MonoidalCategoryStruct.tensorHom y' (𝟙 _) = g' ≫ π + ∧ IsSplitEpi (fibre_incl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) + ∧ Epi ( + smart_cover π' + ) + := by + have : Countable (WidePullbackShape ↑ℕ∪{∞}.toTop) := by + have : Countable ℕ∪{∞} := Option.instCountable + apply Option.instCountable + let S' := widePullback S (fun (n : ℕ∪{∞}) ↦ fibre n (π ≫ snd _ _)) + (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _) + let y' : S' ⟶ S := WidePullback.base (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _) + + + let Ttilde := explicitPullback π (MonoidalCategoryStruct.tensorHom y' (𝟙 ℕ∪{∞})) + let π_tilde : Ttilde ⟶ S' ⊗ ℕ∪{∞} := explicitPullback.snd _ _ + + let σ' : ℕ∪{∞} → (S' ⟶ Ttilde) := fun n ↦ + PullbackCone.IsLimit.lift explicitPullback.IsLimit + ((WidePullback.π _ n) ≫ fibre_incl n (π ≫ snd _ _)) + (lift (𝟙 S') (CompHausLike.ofHom _ <| ContinuousMap.const S' n)) + ( + by + simp only [Category.assoc, limit.cone_x, prod.lift_map, Category.id_comp, + Category.comp_id] + apply ChosenFiniteProducts.hom_ext + · simp [y'] + · ext + simp [←ConcreteCategory.comp_apply, fibre_condition] + rfl + ) + have hσ : ∀ n, σ' n ≫ π_tilde ≫ fst _ _ = 𝟙 _ := by + intro n + simp only [←Category.assoc, σ'] + erw [PullbackCone.IsLimit.lift_snd] + exact lift_fst _ _ + have hσ' : ∀ n s, (σ' n ≫ π_tilde ≫ snd S' ℕ∪{∞}) s = n := by + intro n s + simp only [←Category.assoc, σ'] + erw [PullbackCone.IsLimit.lift_snd] + simp + + obtain ⟨T', i, _, _, split⟩ := subspaceCover π_tilde hσ hσ' + + refine ⟨ + S', T', y', + i ≫ π_tilde, + i ≫ explicitPullback.fst _ _, + inferInstance, + ?_, + ?_, + split, + inferInstance + ⟩ + unfold y' + · rw [←WidePullback.π_arrow _ (OnePoint.some 0)] + have : ∀ j, Epi (fibre_incl j (π ≫ snd S ℕ∪{∞}) ≫ π ≫ fst S ℕ∪{∞}) := by + simp_rw [LightProfinite.epi_iff_surjective] + intro j s + have epi : Epi π := inferInstance + rw [LightProfinite.epi_iff_surjective] at epi + obtain ⟨t, ht⟩ := epi ⟨s, j⟩ + use ⟨ + t, + by + simp only [Set.mem_preimage, ConcreteCategory.comp_apply, ht, + Set.mem_singleton_iff, S', y', Ttilde, σ'] + rfl + ⟩ + rw [ConcreteCategory.comp_apply] + change (ConcreteCategory.hom (π ≫ fst S ℕ∪{∞})) t = s + rw [ConcreteCategory.comp_apply, ht] + rfl + have := surj_widePullback S (fun (n : ℕ∪{∞}) ↦ fibre n (π ≫ snd _ _)) + (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _) this + apply epi_comp + simp only [π_tilde, Category.assoc,explicitPullback.condition] + +section + +variable {X Y : LightProfinite} (y : Y) (f : X ⟶ Y) + +instance (S : Set Y) [IsClosed S] : IsClosed (f ⁻¹' S) := by + exact IsClosed.preimage f.1.continuous inferInstance + +instance : IsClosed (f ⁻¹' {y}) := + inferInstance + +instance (S : Set X) [IsClosed S] : CompactSpace S := by + exact isCompact_iff_compactSpace.mp (IsClosed.isCompact inferInstance) + +instance : CompactSpace (f ⁻¹' {y}) := inferInstance +end + + +lemma prod_epi (X Y : LightProfinite.{u}) [hempty : Nonempty X] : Epi (snd X Y) := by + rw [LightProfinite.epi_iff_surjective] + exact fun y ↦ ⟨⟨Classical.choice hempty, y⟩, rfl⟩ + +lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} + (f : (free R).obj (S).toCondensed ⟶ Y) + : ∃ (T : LightProfinite) (π : T ⟶ S) (g : ((free R).obj T.toCondensed) ⟶ X), Epi π + ∧ g ≫ p = (lightProfiniteToLightCondSet ⋙ (free R)).map π ≫ f := by + have : Epi ((LightCondensed.forget _).map p) := inferInstance + rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite] at this + + let y : Y.val.obj (op S) := (coherentTopology LightProfinite).yonedaEquiv <| + (Adjunction.homEquiv (freeForgetAdjunction R) (S).toCondensed Y f) + + obtain ⟨T, π, hπ, x, hx⟩ := this S y + + let g : (free R).obj T.toCondensed ⟶ X := + ((freeForgetAdjunction R).homEquiv T.toCondensed X).symm ((coherentTopology LightProfinite).yonedaEquiv.symm x) + + have comm : g ≫ p = (lightProfiniteToLightCondSet ⋙ (LightCondensed.free R)).map π ≫ f := by + symm + rw [ + Functor.comp_map, + ←Adjunction.homEquiv_naturality_left_square_iff (freeForgetAdjunction R), + Equiv.apply_symm_apply + ] + apply Sheaf.Hom.ext + rw [ + (coherentTopology LightProfinite).yonedaEquiv_symm_naturality_right, + hx, + (coherentTopology LightProfinite).map_yonedaEquiv', + ←(coherentTopology LightProfinite).yonedaEquiv_symm_naturality_right + ] + rfl + + have : Epi π := (LightProfinite.epi_iff_surjective π).mpr hπ + use T, π, g + +instance : PreservesFiniteCoproducts (lightProfiniteToLightCondSet ⋙ (free R)) := by + have : PreservesFiniteCoproducts lightProfiniteToLightCondSet := sorry + have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩ + infer_instance + +noncomputable def hc {S T : LightProfinite} (π : T ⟶ S) [Epi π] + : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π)) := by + have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩ + exact isColimitOfPreserves _ (explicitPullback.explicitRegularIsColimit π) + +lemma eq_sub_self {G : Type} [AddGroup G] {a b : G} : a = a - b ↔ b = 0 := by + rw [←sub_eq_self (a := a), eq_comm] + +noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S ⊗ ℕ∪{∞})) + [Epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smart_cover π)] + (g : ((lightProfiniteToLightCondSet ⋙ free R).obj T) ⟶ X) + (r_inf : T ⟶ (fibre ∞ (π ≫ snd _ _))) (σ : S ⟶ (fibre ∞ (π ≫ snd _ _))) + (hr : fibre_incl ∞ (π ≫ snd _ _) ≫ r_inf = 𝟙 (fibre ∞ (π ≫ snd _ _))) + : Cocone ((parallelPair (lightProfiniteToLightCondSet.map (explicitPullback.fst π π)) + (lightProfiniteToLightCondSet.map (explicitPullback.snd π π))) ⋙ (free R)) := { + pt := X + ι := by + let ι_inf := fibre_incl ∞ (π ≫ snd _ _) + let π_inf := (fibre_incl ∞ (π ≫ snd _ _) ≫ π ≫ fst _ _) + + let g_tilde : (lightProfiniteToLightCondSet ⋙ (free R)).obj T ⟶ X := + g - (lightProfiniteToLightCondSet ⋙ (free R)).map (r_inf ≫ ι_inf) ≫ g + + (lightProfiniteToLightCondSet ⋙ (free R)).map (r_inf ≫ π_inf ≫ σ ≫ ι_inf) ≫ g + refine parallelPair.hom (_ ≫ g_tilde) g_tilde ?_ (by rfl) + + rw [←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smart_cover π)] + + let hcc := isColimitOfHasBinaryCoproductOfPreservesColimit + (lightProfiniteToLightCondSet ⋙ (free R)) T + (explicitPullback (fibre_incl ∞ (π ≫ snd _ _) ≫ π) (fibre_incl ∞ (π ≫ snd _ _) ≫ π)) + + apply hcc.hom_ext + rintro (j | j) + · simp only [const_obj_obj, Functor.comp_map, BinaryCofan.mk_pt, + BinaryCofan.ι_app_left, BinaryCofan.mk_inl, smart_cover, parallelPair_obj_zero, + parallelPair_obj_one, parallelPair_map_left, parallelPair_map_right, const_obj_map, + Category.comp_id] + simp only [comp_obj, pair_obj_left, explicitPullback.diagonal, parallelPair_obj_zero, + parallelPair_obj_one, ← map_comp_assoc, ← Functor.map_comp, coprod.desc_comp, + colimit.ι_desc, BinaryCofan.mk_pt, BinaryCofan.ι_app_left, BinaryCofan.mk_inl] + erw [PullbackCone.IsLimit.lift_fst] + · simp only [comp_obj, CompHausLike.coe_comp, Function.comp_apply, Set.coe_setOf, + Set.mem_setOf_eq, pair_obj_right, const_obj_obj, Functor.comp_map, BinaryCofan.mk_pt, + BinaryCofan.ι_app_right, BinaryCofan.mk_inr, smart_cover, parallelPair_obj_zero, + parallelPair_obj_one, parallelPair_map_left, parallelPair_map_right, const_obj_map, + Category.comp_id] + simp only [Category.assoc, ←Functor.map_comp, ←Functor.comp_map] + simp only [←Category.assoc] + simp only [←Functor.map_comp, ←Functor.comp_map] + rw [coprod.inr_desc] + simp only [Preadditive.comp_add, Preadditive.comp_sub, g_tilde] + simp [←Category.assoc, ←Functor.map_comp, ←Functor.comp_map] + rw [ + explicitPullback.map_fst, explicitPullback.map_snd, + Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _)) r_inf, hr, Category.comp_id, + Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _)) r_inf, hr, Category.comp_id, + sub_self, zero_add, + sub_self, zero_add, + ] + unfold π_inf + rw [ + ←Category.assoc _ π _, + ←Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _) ≫ π) _, + explicitPullback.condition + ] + rfl + } + +set_option maxHeartbeats 500000 +theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} + (f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y) : + ∃ (S' : LightProfinite) + (ψ : S' ⟶ S) + (g : (free R).obj (S' ⊗ ℕ∪{∞}).toCondensed ⟶ X), Epi ψ + ∧ ((free R).map (lightProfiniteToLightCondSet.map (MonoidalCategoryStruct.tensorHom ψ (𝟙 ℕ∪{∞}))) ≫ f = g ≫ p) := by + + obtain ⟨T, π, g, hπ, comm⟩ := comm_sq R p f + obtain ⟨S', T', y', π', g', hπ', hy', comp, ⟨⟨split⟩⟩, epi⟩ := xyz π + + use S', y' + + have : PreservesEpimorphisms (lightProfiniteToLightCondSet ⋙ (free R)) := by + have : IsLeftAdjoint (free R) := (freeForgetAdjunction R).isLeftAdjoint + infer_instance + + by_cases hS' : Nonempty S' + -- ⨯ + · let hc : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π')) := hc R π' + + let ι_inf := fibre_incl ∞ (π' ≫ snd _ _) + have : Mono ι_inf := fibre_incl_mono _ _ + have : Nonempty (fibre ∞ (π' ≫ snd _ _)) := by + have : Epi (snd S' ℕ∪{∞}) := by + apply prod_epi + exact fibre_nonempty _ _ + + have fibre_injective : Injective (fibre ∞ (π' ≫ snd _ _)) := injective_of_light _ + obtain ⟨r_inf, hr⟩ := fibre_injective.factors (𝟙 _) ι_inf + + simp only [ι_inf] at hr + + let π_inf := (fibre_incl ∞ (π' ≫ snd _ _) ≫ π' ≫ fst _ _) + let σ := split.section_ + let hσ := split.id + + let gg := (lightProfiniteToLightCondSet ⋙ (free R)).map g' ≫ g + + let c' := c R π' gg r_inf σ hr + + have : fibre_incl ∞ (π' ≫ snd _ _) ≫ π' + = fibre_incl ∞ (π' ≫ snd _ _) ≫ π' + ≫ fst _ _ + ≫ lift (𝟙 _) + (CompHausLike.ofHom _ (ContinuousMap.const S' (∞ : ℕ∪{∞}))) := by + apply ChosenFiniteProducts.hom_ext _ _ (by simp) + simp only [Category.assoc] + rw [fibre_condition ∞ (π' ≫ snd _ _)] + ext + simp + + have : c'.ι.app WalkingParallelPair.one ≫ p + = (lightProfiniteToLightCondSet ⋙ (free R)).map (π' ≫ MonoidalCategoryStruct.tensorHom y' (𝟙 ℕ∪{∞})) ≫ f := by + simp only [gg, comp_obj, parallelPair_obj_one, c, Functor.comp_map, + const_obj_obj, Functor.map_comp, Category.assoc, + Preadditive.comp_add, Preadditive.comp_sub, parallelPair.hom_app, + Preadditive.add_comp, Preadditive.sub_comp, ι_inf, c'] + rw [comm] + simp only [←Functor.map_comp, ←Functor.comp_map, ←Category.assoc, ←comp] + simp only [Category.assoc] + rw [ + sub_add, + sub_eq_self, + sub_eq_zero, + ←Category.assoc _ π' _, + this, + ←Category.assoc _ (fst _ _), + ←Category.assoc _ (π' ≫ fst _ _), + ←Category.assoc σ, + ←Category.assoc σ, + hσ, + Category.id_comp + ] + rfl + + let abc : ((free R).obj (S' ⊗ ℕ∪{∞}).toCondensed) ⟶ X := hc.desc c' + refine ⟨abc, inferInstance, ?_⟩ + + dsimp [abc] + + have reg_eq : (free R).map ((regular π').ι.app WalkingParallelPair.one) = ((lightProfiniteToLightCondSet ⋙ (free R)).map π') := rfl + rw [ + ←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map π'), + ←Functor.comp_map, ←Functor.map_comp_assoc, ←reg_eq, + ←Category.assoc _ (hc.desc c') + ] + change _ = (((free R).mapCocone (explicitPullback.explicitRegular π')).ι.app one ≫ hc.desc c') ≫ p + erw [hc.fac] + rw [this] + · have : ¬Nonempty (S' ⊗ ℕ∪{∞} : LightProfinite) := empty_map hS' (fst _ _) + have : IsIso π' := empty_iso this _ + obtain ⟨π'inv, h, _⟩ := this + use (lightProfiniteToLightCondSet ⋙ (free R)).map (π'inv ≫ g') ≫ g + refine ⟨hy', ?_⟩ + rw [←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map π')] + simp only [← Category.assoc, ← Functor.map_comp] + rw [h, Category.id_comp] + simp only [Category.assoc] + rw [comm] + simp only [← Category.assoc, ← Functor.map_comp] + rw [←comp] + simp + +theorem internallyProjective : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := by + rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}] + intro X Y p hp S f + obtain ⟨S', π, g, hπ, comm⟩ := proj_explicit R p f + rw [LightProfinite.epi_iff_surjective] at hπ + use S', π, hπ, g, comm diff --git a/LeanCondensed/Projects/Pullbacks.lean b/LeanCondensed/Projects/Pullbacks.lean new file mode 100644 index 0000000..27e462f --- /dev/null +++ b/LeanCondensed/Projects/Pullbacks.lean @@ -0,0 +1,274 @@ +import Mathlib + +open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed + MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom Topology + +universe u + +variable {X Y : LightProfinite} (y : Y) (f : X ⟶ Y) + +section + +instance (x : X) : IsClosed {x} := isClosed_singleton + +instance (S : Set Y) [IsClosed S] : IsClosed (f ⁻¹' S) := by + exact IsClosed.preimage f.1.continuous inferInstance + +instance : IsClosed (f ⁻¹' {y}) := + inferInstance + +instance (S : Set X) [IsClosed S] : CompactSpace S := by + exact isCompact_iff_compactSpace.mp (IsClosed.isCompact inferInstance) + +instance : CompactSpace (f ⁻¹' {y}) := inferInstance + +end + +instance : TotallyDisconnectedSpace PUnit := by + have := TotallySeparatedSpace.of_discrete + apply TotallySeparatedSpace.totallyDisconnectedSpace + +def fibre : LightProfinite := + ⟨ + TopCat.of (f ⁻¹' {y}), + Subtype.totallyDisconnectedSpace, + TopologicalSpace.Subtype.secondCountableTopology (f ⁻¹' {y}) + ⟩ + +def fibre_incl : fibre y f ⟶ X := + CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩ + +def fibre_condition + : fibre_incl y f ≫ f = (CompHausLike.ofHom _ <| ContinuousMap.const (fibre y f) y) + := by ext x; exact x.2 + +lemma fibre_incl_mono : Mono (fibre_incl y f) := by + rw [CompHausLike.mono_iff_injective] + exact Subtype.val_injective + +lemma fibre_incl_embedding : IsEmbedding (fibre_incl y f) := IsEmbedding.subtypeVal + +lemma fibre_nonempty [hepi : Epi f] : Nonempty (fibre y f) := by + rw [epi_iff_surjective f] at hepi + obtain ⟨x, hx⟩ := hepi y + exact ⟨x, hx⟩ + +def point : LightProfinite := LightProfinite.of PUnit + +def fibreCone : PullbackCone (CompHausLike.ofHom _ <| ContinuousMap.const point y) f + := + let space := f ⁻¹' {y} + have : IsClosed space := IsClosed.preimage f.1.continuous isClosed_singleton + have : IsCompact space := this.isCompact + have : CompactSpace space := by + exact isCompact_iff_compactSpace.mp this + PullbackCone.mk (CompHausLike.ofHom _ <| ContinuousMap.const (fibre y f) PUnit.unit) (fibre_incl y f) + (by ext x; simp only [fibre_incl, ConcreteCategory.comp_apply, CompHausLike.hom_ofHom, + ContinuousMap.const_apply, ContinuousMap.coe_mk]; rw [x.2]) + +def fibreConeIsLimit : IsLimit (fibreCone y f) := by + refine PullbackCone.IsLimit.mk ?_ ?_ ?_ ?_ ?_ + · exact (fibreCone _ _).condition + · intro cone + have : ∀ z : cone.pt, f (cone.snd z) = y := by + intro z + rw [ + ←ConcreteCategory.comp_apply, + ←cone.condition, + ConcreteCategory.comp_apply + ] + rfl + refine CompHausLike.ofHom _ <| ⟨fun z ↦ ⟨cone.snd z, this z⟩, ?_⟩ + rw [IsInducing.continuous_iff (fibre_incl_embedding y f).1] + exact cone.snd.1.continuous + repeat {exact fun cone ↦ rfl} + · intro cone m hm hm' + have := fibre_incl_mono y f + rw [←cancel_mono (fibre_incl y f), hm'] + rfl + +def fibreLift {Z : LightProfinite} (g : Z ⟶ X) (hg : ∀ z, f (g z) = y) : Z ⟶ fibre y f := + let space := f ⁻¹' {y} + have : IsClosed space := IsClosed.preimage f.1.continuous isClosed_singleton + have : IsCompact space := this.isCompact + have : CompactSpace space := by + exact isCompact_iff_compactSpace.mp this + CompHausLike.ofHom _ <| ⟨fun z ↦ ⟨g z, hg z⟩, by rw [IsInducing.continuous_iff (fibre_incl_embedding y f).1]; exact g.1.continuous⟩ + +@[simp] +lemma fibreLift_comp {Z : LightProfinite} (g : Z ⟶ X) (hg : ∀ z, f (g z) = y) + : fibreLift y f g hg ≫ fibre_incl y f = g := rfl + +section + +variable {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) + +instance : IsClosed {⟨x,y⟩ : X × Y | f x = g y} := by + apply IsClosed.mk + rw [isOpen_prod_iff] + intro a b hab + obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab + refine ⟨ + f⁻¹'u, g⁻¹'v, + f.1.continuous.isOpen_preimage _ hu, + g.1.continuous.isOpen_preimage _ hv, + ha, hb, ?_ + ⟩ + intro ⟨x, y⟩ ⟨hx, hy⟩ + simp only [Set.mem_preimage] at hx hy + intro hxy + rw [hxy] at hx + exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩ + +instance : IsCompact {⟨x,y⟩ : X × Y | f x = g y} := by + apply IsClosed.isCompact + infer_instance + +instance : CompactSpace {⟨x,y⟩ : X × Y | f x = g y} := by + rw [←isCompact_iff_compactSpace] + exact + instIsCompactProdCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologySetOfMatch_1PropEqCoeContinuousMapHomLightProfinite + f g + +end + +def explicitPullback {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) : LightProfinite + := + ⟨TopCat.of {⟨x,y⟩ : X × Y | f x = g y}, inferInstance, inferInstance⟩ + +namespace explicitPullback + +variable {X Y Z : LightProfinite} {f : X ⟶ Z} {g : Y ⟶ Z} + +def fst (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ X := + CompHausLike.ofHom _ + ⟨ + (Prod.fst : X × Y → X) ∘ (Subtype.val : _ → X × Y), + Continuous.comp continuous_fst continuous_subtype_val + ⟩ + +def snd (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ Y := + let space := {⟨x,y⟩ : X × Y | f x = g y} + have : IsClosed space := by + apply IsClosed.mk + rw [isOpen_prod_iff] + intro a b hab + obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab + refine ⟨ + f⁻¹'u, g⁻¹'v, + f.1.continuous.isOpen_preimage _ hu, + g.1.continuous.isOpen_preimage _ hv, + ha, hb, ?_ + ⟩ + intro ⟨x, y⟩ ⟨hx, hy⟩ + simp only [Set.mem_preimage] at hx hy + intro hxy + rw [hxy] at hx + exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩ + have : IsCompact space := this.isCompact + have : CompactSpace space := by + exact isCompact_iff_compactSpace.mp this + CompHausLike.ofHom _ + ⟨ + Prod.snd ∘ Subtype.val, + Continuous.comp continuous_snd continuous_subtype_val + ⟩ + +instance epi_pullback [hepi : Epi f] : Epi (snd (f := f) (g := g)) := by + rw [LightProfinite.epi_iff_surjective] at hepi ⊢ + intro y + obtain ⟨x, hx⟩ := hepi (g y) + exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩ + + +lemma condition : fst (f := f) (g := g) ≫ f = snd (f := f) (g := g) ≫ g := by + ext ⟨_,hxy⟩ + exact hxy + +def Cone (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g := + PullbackCone.mk (fst _ _) (snd _ _) condition + +lemma Cone.fst_eq : (Cone f g).fst = fst _ _ := rfl +lemma Cone.snd_eq : (Cone f g).snd = snd _ _ := rfl + +def IsLimit : IsLimit (Cone f g) := by + let space := {⟨x,y⟩ : X × Y | f x = g y} + have : IsClosed space := by + apply IsClosed.mk + rw [isOpen_prod_iff] + intro a b hab + obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab + refine ⟨ + f⁻¹'u, g⁻¹'v, + f.1.continuous.isOpen_preimage _ hu, + g.1.continuous.isOpen_preimage _ hv, + ha, hb, ?_ + ⟩ + intro ⟨x, y⟩ ⟨hx, hy⟩ + simp only [Set.mem_preimage] at hx hy + intro hxy + rw [hxy] at hx + exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩ + have : IsCompact space := this.isCompact + have : CompactSpace space := by + exact isCompact_iff_compactSpace.mp this + + refine PullbackCone.IsLimit.mk ?_ ?_ ?_ ?_ ?_ + · intro cone + have : ∀ z, ⟨cone.fst z, cone.snd z⟩ ∈ space := by + intro z + simp only [Set.mem_setOf_eq, space] + rw [←ConcreteCategory.comp_apply, cone.condition] + rfl + refine CompHausLike.ofHom _ ⟨fun z ↦ ⟨⟨cone.fst z, cone.snd z⟩, this z⟩, ?_⟩ + + rw [(IsInducing.continuous_iff IsEmbedding.subtypeVal.1)] + have : Continuous (fun z ↦ (⟨cone.fst z, cone.snd z⟩ : X × Y)) + = Continuous + (Subtype.val ∘ fun z ↦ ⟨ + ((ConcreteCategory.hom cone.fst) z, + (ConcreteCategory.hom cone.snd) z), + this z + ⟩) := by + exact congr_arg (f := Continuous) (rfl) + rw [←this] + refine Continuous.prodMk cone.fst.1.continuous cone.snd.1.continuous + repeat {intro cone; ext z; rfl} + · intro cone m hm hm' + ext z + apply Subtype.ext + apply Prod.ext + change fst _ _ (↑((ConcreteCategory.hom m) z)) = _ + rw [←ConcreteCategory.comp_apply, hm] + rfl + change snd _ _ (↑((ConcreteCategory.hom m) z)) = _ + rw [←ConcreteCategory.comp_apply, hm'] + rfl + +def diagonal (f : X ⟶ Y) : X ⟶ explicitPullback f f + := PullbackCone.IsLimit.lift IsLimit (𝟙 _) (𝟙 _) rfl + +def map {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z') + (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z') + (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') + : explicitPullback f g ⟶ explicitPullback f' g' := + PullbackCone.IsLimit.lift IsLimit (fst _ _ ≫ i₁) (snd _ _ ≫ i₂) + (by rw [Category.assoc, Category.assoc, ←eq₁, ←eq₂, ←Cone.fst_eq, + PullbackCone.condition_assoc, Cone.snd_eq]) + +lemma map_fst {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z') + (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z') + (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') : map f g f' g' i₁ i₂ i₃ eq₁ eq₂ ≫ fst f' g' = fst f g ≫ i₁ := rfl + +lemma map_snd {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z') + (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z') + (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') : map f g f' g' i₁ i₂ i₃ eq₁ eq₂ ≫ snd f' g' = snd f g ≫ i₂ := rfl + +def explicitRegular {X Y : LightProfinite} (π : X ⟶ Y) + : Cofork (lightProfiniteToLightCondSet.map <| fst π π) + (lightProfiniteToLightCondSet.map <| snd π π) := + Cofork.ofπ (lightProfiniteToLightCondSet.map π) + (by simp only [←Functor.map_comp, condition]) + +def explicitRegularIsColimit {X Y : LightProfinite} (π : X ⟶ Y) : IsColimit (explicitRegular π) := by + sorry diff --git a/LeanCondensed/Projects/test.lean b/LeanCondensed/Projects/test.lean new file mode 100644 index 0000000..29eea88 --- /dev/null +++ b/LeanCondensed/Projects/test.lean @@ -0,0 +1,18 @@ +import Mathlib + +example {J : Type*} {A : Type*} [DecidableEq J] {types : J → Type*} + (nonempty : ∀j, Nonempty (types j)) (f : (j : J) → types j → A) + (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), ∀ j, i = j → f j (p j) = f i t := + ⟨ + fun j ↦ ( + if hij : i = j then + hij ▸ t + else + Classical.choice (nonempty j) + ), + by + intro j h + simp [dif_pos h] + subst h + rfl + ⟩ From 01739a36a2db57b17b9e3db945978aacf4302e42 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Sun, 29 Jun 2025 18:52:13 +0200 Subject: [PATCH 02/13] Coproducts --- LeanCondensed/Projects/Epi.lean | 10 +++++-- LeanCondensed/Projects/PreservesCoprod.lean | 23 ++++++++++++++- LeanCondensed/Projects/Proj.lean | 4 ++- LeanCondensed/Projects/Pullbacks.lean | 31 +++++++++++++++++++-- LeanCondensed/Projects/test.lean | 18 ------------ 5 files changed, 61 insertions(+), 25 deletions(-) delete mode 100644 LeanCondensed/Projects/test.lean diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index 604b100..1bb6204 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -1,7 +1,6 @@ import Mathlib import LeanCondensed.Mathlib.CategoryTheory.Countable -import LeanCondensed.Projects.Pullbacks open Function CategoryTheory Limits Opposite @@ -74,9 +73,14 @@ instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := { ⟩ } -lemma abc {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y +lemma stupid {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y := congr_arg (fun (a : s) ↦ (↑a : A)) h +noncomputable def πpair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet := + parallelPair + (lightProfiniteToLightCondSet.map <| pullback.fst π π) + (lightProfiniteToLightCondSet.map <| pullback.snd π π) + noncomputable def regular {X Y : LightProfinite} (π : X ⟶ Y) : Cofork (lightProfiniteToLightCondSet.map <| pullback.fst π π) (lightProfiniteToLightCondSet.map <| pullback.snd π π) := Cofork.ofπ (lightProfiniteToLightCondSet.map <| π) (by rw [ @@ -126,7 +130,7 @@ lemma regularLift_comp {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] ( : (regular π).π ≫ regularLift π cone = cone.π := by refine Sheaf.Hom.ext (yonedaEquiv.injective ?_) erw [←yonedaEquiv_naturality (F := cone.pt.val), Equiv.apply_symm_apply] - exact abc (s := {x : cone.pt.val.obj (Opposite.op X) | cone.pt.val.map (pullback.fst π π).op x = cone.pt.val.map (pullback.snd π π).op x}) (regularLift_prop π cone) + exact stupid (s := {x : cone.pt.val.obj (Opposite.op X) | cone.pt.val.map (pullback.fst π π).op x = cone.pt.val.map (pullback.snd π π).op x}) (regularLift_prop π cone) lemma regularLift_unique {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) (m : (lightProfiniteToLightCondSet.obj Y) ⟶ cone.pt) (hm : (regular π).π ≫ m = cone.π) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index aa55e64..2002acd 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -6,7 +6,18 @@ open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondens def coprod_desc {n : ℕ} {K : Discrete (Fin n) ⥤ LightProfinite} {c : Cocone K} (hc : IsColimit c) (s : Cocone (K ⋙ lightProfiniteToLightCondSet)) - : c.pt.toCondensed ⟶ s.pt := sorry + : c.pt.toCondensed ⟶ s.pt := + have pres : PreservesFiniteProducts s.pt.val := inferInstance + let K' := (Discrete.opposite (Fin n)).inverse ⋙ K.op + let cc := (Cones.whiskeringEquivalence (Discrete.opposite (Fin n)).symm (F := K.op)).functor.obj c.op + let hcc : IsLimit cc := by apply IsLimit.whiskerEquivalence hc.op + let scc := s.pt.val.mapCone cc + let hscc := (pres.preserves n).preservesLimit (K := K').preserves hcc + + let elems : (i : Fin n) → s.pt.val.obj (K'.obj ⟨i⟩) := + fun i ↦ (coherentTopology LightProfinite).yonedaEquiv (s.ι.app (Discrete.mk i)) + let lift : s.pt.val.obj cc.pt := sorry + sorry instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where preserves n := { @@ -18,3 +29,13 @@ instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where }⟩ } } + +instance : PreservesColimitsOfShape (Discrete WalkingPair) lightProfiniteToLightCondSet := by + sorry + +instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) lightProfiniteToLightCondSet := by + sorry + +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{0} where + preserves _ := + preservesShape_fin_of_preserves_binary_and_initial lightProfiniteToLightCondSet _ diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index a4b1053..9938c40 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -3,6 +3,7 @@ import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.Initial import LeanCondensed.Projects.OverN import LeanCondensed.Projects.InternallyProjective +import LeanCondensed.Projects.PreservesCoprod import LeanCondensed.Mathlib.CategoryTheory.Countable import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts import LeanCondensed.Projects.Pullbacks @@ -354,7 +355,8 @@ lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfin use T, π, g instance : PreservesFiniteCoproducts (lightProfiniteToLightCondSet ⋙ (free R)) := by - have : PreservesFiniteCoproducts lightProfiniteToLightCondSet := sorry + have : PreservesFiniteCoproducts lightProfiniteToLightCondSet := + instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet_leanCondensed have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩ infer_instance diff --git a/LeanCondensed/Projects/Pullbacks.lean b/LeanCondensed/Projects/Pullbacks.lean index 27e462f..dc5148e 100644 --- a/LeanCondensed/Projects/Pullbacks.lean +++ b/LeanCondensed/Projects/Pullbacks.lean @@ -1,4 +1,5 @@ import Mathlib +import LeanCondensed.Projects.Epi open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom Topology @@ -264,11 +265,37 @@ lemma map_snd {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z') (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') : map f g f' g' i₁ i₂ i₃ eq₁ eq₂ ≫ snd f' g' = snd f g ≫ i₂ := rfl +def explicitPair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet + := parallelPair + (lightProfiniteToLightCondSet.map (fst π π)) (lightProfiniteToLightCondSet.map (snd π π)) + +noncomputable def explicitPullbackIsoPullback {X Y : LightProfinite} (π : X ⟶ Y) : explicitPullback π π ≅ pullback π π := + Limits.IsLimit.conePointUniqueUpToIso (IsLimit (f := π) (g := π)) (pullback.isLimit π π) + +noncomputable def explicitPairIsoPair {X Y : LightProfinite} (π : X ⟶ Y) : explicitPair π ≅ πpair π := + parallelPair.ext + (lightProfiniteToLightCondSet.mapIso (explicitPullbackIsoPullback π) : (explicitPair π).obj zero ≅ (πpair π).obj zero) + (Iso.refl _) + ( + by simp [←Functor.map_comp, explicitPair, πpair, explicitPullbackIsoPullback]; rfl + ) + ( + by simp [←Functor.map_comp, explicitPair, πpair, explicitPullbackIsoPullback]; rfl + ) + def explicitRegular {X Y : LightProfinite} (π : X ⟶ Y) : Cofork (lightProfiniteToLightCondSet.map <| fst π π) (lightProfiniteToLightCondSet.map <| snd π π) := Cofork.ofπ (lightProfiniteToLightCondSet.map π) (by simp only [←Functor.map_comp, condition]) -def explicitRegularIsColimit {X Y : LightProfinite} (π : X ⟶ Y) : IsColimit (explicitRegular π) := by - sorry +noncomputable def explicitRegularIsColimit {X Y : LightProfinite} (π : X ⟶ Y) [hepi : Epi π] + : IsColimit (explicitRegular π) := by + rw [LightProfinite.epi_iff_surjective, ←LightProfinite.effectiveEpi_iff_surjective] at hepi + exact ( + IsColimit.equivOfNatIsoOfIso + (explicitPairIsoPair _) + _ + (regular _) + (Cofork.ext (Iso.refl _) rfl) + ).symm (regular_IsColimit _) diff --git a/LeanCondensed/Projects/test.lean b/LeanCondensed/Projects/test.lean deleted file mode 100644 index 29eea88..0000000 --- a/LeanCondensed/Projects/test.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Mathlib - -example {J : Type*} {A : Type*} [DecidableEq J] {types : J → Type*} - (nonempty : ∀j, Nonempty (types j)) (f : (j : J) → types j → A) - (i : J) (t : types i) : ∃ (p : (Π(j : J), types j)), ∀ j, i = j → f j (p j) = f i t := - ⟨ - fun j ↦ ( - if hij : i = j then - hij ▸ t - else - Classical.choice (nonempty j) - ), - by - intro j h - simp [dif_pos h] - subst h - rfl - ⟩ From f5aeefdd5f128ddae2e8b7b0771bcebbd6b56d98 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Sun, 29 Jun 2025 20:25:34 +0200 Subject: [PATCH 03/13] One more suggestion --- LeanCondensed/Projects/PreservesCoprod.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 2002acd..063191a 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -30,12 +30,27 @@ instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where } } +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{0} where + preserves _ := + preservesShape_fin_of_preserves_binary_and_initial lightProfiniteToLightCondSet _ + instance : PreservesColimitsOfShape (Discrete WalkingPair) lightProfiniteToLightCondSet := by sorry instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) lightProfiniteToLightCondSet := by sorry +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where + preserves n := { + preservesColimit {K} := { + preserves {c} hc := by + apply Nonempty.map isColimitOfOp + apply coyonedaFunctor_reflectsLimits.reflectsLimitsOfShape.reflectsLimit.reflects + -- use the coyoneda lemma here + sorry + } + } + instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{0} where preserves _ := preservesShape_fin_of_preserves_binary_and_initial lightProfiniteToLightCondSet _ From 96db41f2c40acd96afcbe6dffea566eb54805e90 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Tue, 8 Jul 2025 11:10:26 +0200 Subject: [PATCH 04/13] Bump mathlib, last sorry and a bunch of errors --- LeanCondensed/LightCondensed/Yoneda.lean | 4 +- .../CategoryTheory/Functor/EpiMono.lean | 27 +++ .../Localization/Bifunctor.lean | 2 +- .../Localization/Monoidal/Braided.lean | 2 +- LeanCondensed/Projects/Initial.lean | 3 +- LeanCondensed/Projects/LightSolid.lean | 4 +- LeanCondensed/Projects/PreservesCoprod.lean | 182 +++++++++++++----- LeanCondensed/Projects/PreservesEpi.lean | 3 +- LeanCondensed/Projects/Proj.lean | 2 + lake-manifest.json | 20 +- lean-toolchain | 2 +- 11 files changed, 180 insertions(+), 71 deletions(-) create mode 100644 LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index 9c94407..6c4f176 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -26,7 +26,7 @@ lemma yoneda_symm_naturality {S S' : LightProfinite} (f : S' ⟶ S) (A : LightCo (x : A.val.obj ⟨S⟩) : lightProfiniteToLightCondSet.map f ≫ (yoneda S A).symm x = (yoneda S' A).symm ((A.val.map f.op) x) := by apply Sheaf.hom_ext - rw [Sheaf.instCategorySheaf_comp_val] + rw [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)] @@ -36,7 +36,7 @@ attribute [local instance] Types.instConcreteCategory Types.instFunLike lemma yoneda_symm_conaturality (S : LightProfinite) {A A' : LightCondSet} (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 - rw [Sheaf.instCategorySheaf_comp_val] + rw [Sheaf.comp_val] ext T y exact NatTrans.naturality_apply (φ := f.val) (Y := T) _ _ diff --git a/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean b/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean new file mode 100644 index 0000000..3ca04a5 --- /dev/null +++ b/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean @@ -0,0 +1,27 @@ +import Mathlib + +open CategoryTheory + +variable {C : Type*} [Category C] {D : Type*} [Category D] {F G : C ⥤ D} + +lemma epi_of_Retract {f g : Arrow C} (π : f ⟶ g) [Epi f.hom] [Epi π.right] : Epi g.hom := + have : Epi (π.left ≫ g.hom) := by + rw [←Functor.id_map π.left, π.w, Functor.id_map] + exact epi_comp f.hom π.right + epi_of_epi (π.left) _ + +lemma preservesEpi_of_Epi (f : F ⟶ G) (hf : ∀ X, Epi (f.app X)) (preserves : F.PreservesEpimorphisms) + : G.PreservesEpimorphisms where + preserves {X Y} π hπ := + have : Epi (f.app X ≫ G.map π) := by + rw [←f.naturality π] + exact epi_comp (F.map π) (f.app Y) + epi_of_epi (f.app X) (G.map π) + +lemma preservesEpi_ofRetract (r : Retract G F) (preserves : F.PreservesEpimorphisms) + : G.PreservesEpimorphisms where + preserves := ( + preservesEpi_of_Epi _ + (fun _ ↦ (SplitEpi.mk (r.i.app _) (by rw [←NatTrans.comp_app, r.retract, NatTrans.id_app])).epi) + preserves + ).preserves diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean index 3efc937..ef48f6b 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Localization/Bifunctor.lean @@ -2,7 +2,7 @@ import Mathlib.CategoryTheory.Localization.Bifunctor namespace CategoryTheory -open Category +open Category Functor variable {C₁ C₂ D₁ D₂ E E' : Type*} [Category C₁] [Category C₂] [Category D₁] [Category D₂] [Category E] [Category E'] diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean index 3a30f92..e437dae 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean @@ -20,7 +20,7 @@ braided, in such a way that the localization functor is braided. If `C` is symme the monoidal structure on `D` is also symmetric. -/ -open CategoryTheory Category MonoidalCategory BraidedCategory +open CategoryTheory Category MonoidalCategory BraidedCategory Functor namespace CategoryTheory.Localization.Monoidal diff --git a/LeanCondensed/Projects/Initial.lean b/LeanCondensed/Projects/Initial.lean index 948e936..095fd87 100644 --- a/LeanCondensed/Projects/Initial.lean +++ b/LeanCondensed/Projects/Initial.lean @@ -22,8 +22,7 @@ def empty_iso {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : IsIso f rw [empty_subset hY ((fun y ↦ _root_.empty_elim hY y) ⁻¹' s)] exact TopologicalSpace.isOpen_univ } - apply IsIso.mk - use finv + refine IsIso.mk ⟨finv, ?_⟩ constructor <;> ext x exact empty_elim hY (f x) exact empty_elim hY x diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean index a05da03..4a8ce58 100644 --- a/LeanCondensed/Projects/LightSolid.lean +++ b/LeanCondensed/Projects/LightSolid.lean @@ -82,7 +82,9 @@ def oneMinusShift' : (free R).obj (ℕ∪{∞}).toCondensed ⟶ (free R).obj ( def oneMinusShift : P R ⟶ P R := by refine P_homMk R _ (oneMinusShift' R) ?_ ≫ P_proj R - sorry + erw [Preadditive.comp_sub, Category.comp_id] + simp only [sub_eq_zero, P_map, ←Functor.map_comp] + rfl variable {R : Type} [CommRing R] diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 063191a..02465fe 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -1,56 +1,136 @@ import Mathlib +import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic +import LeanCondensed.LightCondensed.Yoneda open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom - ChosenFiniteProducts Topology - -def coprod_desc {n : ℕ} {K : Discrete (Fin n) ⥤ LightProfinite} {c : Cocone K} - (hc : IsColimit c) (s : Cocone (K ⋙ lightProfiniteToLightCondSet)) - : c.pt.toCondensed ⟶ s.pt := - have pres : PreservesFiniteProducts s.pt.val := inferInstance - let K' := (Discrete.opposite (Fin n)).inverse ⋙ K.op - let cc := (Cones.whiskeringEquivalence (Discrete.opposite (Fin n)).symm (F := K.op)).functor.obj c.op - let hcc : IsLimit cc := by apply IsLimit.whiskerEquivalence hc.op - let scc := s.pt.val.mapCone cc - let hscc := (pres.preserves n).preservesLimit (K := K').preserves hcc - - let elems : (i : Fin n) → s.pt.val.obj (K'.obj ⟨i⟩) := - fun i ↦ (coherentTopology LightProfinite).yonedaEquiv (s.ι.app (Discrete.mk i)) - let lift : s.pt.val.obj cc.pt := sorry - sorry - -instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where - preserves n := { - preservesColimit {K} := { - preserves {c} hc := ⟨{ - desc s := coprod_desc hc s - fac := sorry - uniq := sorry - }⟩ - } - } - -instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{0} where - preserves _ := - preservesShape_fin_of_preserves_binary_and_initial lightProfiniteToLightCondSet _ - -instance : PreservesColimitsOfShape (Discrete WalkingPair) lightProfiniteToLightCondSet := by - sorry - -instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) lightProfiniteToLightCondSet := by - sorry - -instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet where - preserves n := { - preservesColimit {K} := { - preserves {c} hc := by - apply Nonempty.map isColimitOfOp - apply coyonedaFunctor_reflectsLimits.reflectsLimitsOfShape.reflectsLimit.reflects - -- use the coyoneda lemma here - sorry - } - } + Topology Function + +universe u + +attribute [local instance] Types.instFunLike Types.instConcreteCategory + +instance {n : ℕ} (S : Fin n → LightProfinite.{u}) : + PreservesColimit (Discrete.functor S) lightProfiniteToLightCondSet.{u} := by + have : HasColimitsOfSize.{u} (LightCondSet.{u}) := + inferInstanceAs (HasColimitsOfSize.{u} (Sheaf _ _)) + apply (config := { allowSynthFailures := true}) PreservesCoproduct.of_iso_comparison + rw [isIso_iff_isIso_coyoneda_map] -- or maybe `rw [isIso_iff_coyoneda_map_bijective]` + intro X + rw [isIso_iff_bijective] + have := instIsIsoPiComparison X.val (fun i ↦ ⟨S i⟩) + + let map : ((∐ S).toCondensed ⟶ X) → ((∐ fun i ↦ (S i).toCondensed) ⟶ X) := + (inv (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)) + ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv) + ∘ (Types.productIso (fun i ↦ (S i).toCondensed ⟶ X)).inv + ∘ (Pi.map (fun i ↦ (LightCondensed.yoneda (S i) X).symm)) + ∘ ( + (X.val.mapIso (opCoproductIsoProduct S)).hom + ≫ (piComparison X.val (fun i ↦ ⟨S i⟩)) + ≫ (Types.productIso (fun i ↦ X.val.obj (op (S i)))).hom + ) + ∘ (LightCondensed.yoneda (∐ S) X) + + have map_bij : Bijective map := by + refine Bijective.comp ?_ + ( + Bijective.comp ?_ + (Bijective.comp ?_ (Bijective.comp ?_ ?_)) + ) + repeat {rw [←isIso_iff_bijective]; infer_instance} + exact Bijective.piMap (fun i ↦ (LightCondensed.yoneda _ _).symm.bijective) + rw [←isIso_iff_bijective]; infer_instance + exact (LightCondensed.yoneda _ _).bijective + + have : Injective ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom + ≫ (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩))) := by + apply Bijective.injective + rw [←isIso_iff_bijective] + infer_instance -instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{0} where - preserves _ := - preservesShape_fin_of_preserves_binary_and_initial lightProfiniteToLightCondSet _ + have : ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) + = map := by + apply this.comp_left + simp only [Equiv.invFun_as_coe, mapIso_hom, map] + rw [ + ←Function.comp_assoc, + ] + erw [ + ←coe_comp + (f := (CategoryTheory.inv (piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed) + ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv)) + (g := ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom + ≫ piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed)), + ] + ext1 f + ext1 ⟨i⟩ + simp only [yoneda_obj_obj, Discrete.functor_obj_eq_as, coyoneda_obj_obj, Function.comp_apply, + coyoneda_map_app, Quiver.Hom.unop_op, types_comp_apply, yoneda_obj_map, Category.assoc, + Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, yoneda_apply, CategoryTheory.id_apply, map] + + change + ( + piComparison (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩) + ≫ Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i + ) + ( + (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom.unop + ≫ sigmaComparison lightProfiniteToLightCondSet S + ≫ f + ) = + ( + (Types.productIso fun i ↦ (S i).toCondensed ⟶ X).inv + ≫ Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i + ) _ + + erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)] + rw [Types.productIso_inv_comp_π] + simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply] + + let _ : X.val.obj (⟨∐ S⟩) ⟶ X.val.obj (∏ᶜ fun i ↦ ⟨S i⟩) := (X.val.map (opCoproductIsoProduct S).hom) + + let _ : X.val.obj (⟨∐ S⟩) ⟶ X.val.obj ⟨S i⟩ := + (X.val.map (opCoproductIsoProduct S).hom) ≫ piComparison X.val (fun i ↦ ⟨S i⟩) ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i + + change + _ = + (LightCondensed.yoneda (S i) X).symm ( + ( + (X.val.map (opCoproductIsoProduct S).hom) + ≫ piComparison X.val (fun i ↦ ⟨S i⟩) + ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i + ) + (LightCondensed.yoneda (∐ S) X f) + ) + rw [ + piComparison_comp_π, + ←X.val.map_comp, + opCoproductIsoProduct_hom_comp_π + ] + rw [ + yoneda_obj_map, + ←unop_comp_assoc, + opCoproductIsoProduct_hom_comp_π, + Quiver.Hom.unop_op, + ι_comp_sigmaComparison_assoc, + ←yoneda_symm_naturality + ] + change _ = (lightProfiniteToLightCondSet.map (Sigma.ι S i) ≫ + (((LightCondensed.yoneda (∐ S) X).symm ∘ (LightCondensed.yoneda (∐ S) X)) f)) + rw [Equiv.symm_comp_self, id_eq] + + -- Now the approach is to write `(coyoneda.map (sigmaComparison _ _).op).app X` as + -- `piComparison X.val _` pre- and post-composed with isos given by the coyoneda lemma. + -- The issue is that the homs in `LightCondSet` a priori live in one universe higher than the + -- S-valued points of `X` (but they are small). There is some API in a file called + -- `LightCondensed/Yoneda.lean` in the condensed repo that might be helpful. + rw [this] + exact map_bij + +instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} where + preserves n := + { preservesColimit {S} := by + let i : S ≅ Discrete.functor (fun i ↦ S.obj ⟨i⟩) := Discrete.natIso (fun _ ↦ Iso.refl _) + exact preservesColimit_of_iso_diagram lightProfiniteToLightCondSet i.symm + } diff --git a/LeanCondensed/Projects/PreservesEpi.lean b/LeanCondensed/Projects/PreservesEpi.lean index fe30c20..e5166e5 100644 --- a/LeanCondensed/Projects/PreservesEpi.lean +++ b/LeanCondensed/Projects/PreservesEpi.lean @@ -84,8 +84,7 @@ noncomputable def πSplit : SplitEpi (P_proj R) where id := by apply (P_proj_Epi R).left_cancellation erw [ - ←assoc _ (cokernel.desc (P_map R) (xyz R) (comp_zero _)) _, - cokernel.π_desc, + cokernel.π_desc_assoc, sub_comp, id_comp, assoc, diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index 9938c40..e6f0c77 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -538,3 +538,5 @@ theorem internallyProjective : InternallyProjective ((free R).obj (ℕ∪{∞}). obtain ⟨S', π, g, hπ, comm⟩ := proj_explicit R p f rw [LightProfinite.epi_iff_surjective] at hπ use S', π, hπ, g, comm + +#print axioms internallyProjective diff --git a/lake-manifest.json b/lake-manifest.json index ab3c7be..d365926 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "287febc23a1ff0df9c02d934fb82934e8bc90a85", + "rev": "b8e6a885d66b785df96f75779307fc2daf82b331", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "304c5e2f490d546134c06bf8919e13b175272084", + "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48", + "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a", + "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.59", + "inputRev": "v0.0.67", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1", + "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130", + "rev": "867d9dc77534341321179c9aa40fceda675c50d4", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6", + "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", + "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 22d92c5..28f76d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.20.0-rc5 +leanprover/lean4:v4.22.0-rc3 \ No newline at end of file From 1e3e903c2426c47da35a32d74b2f7ccc8a877cb4 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Tue, 8 Jul 2025 12:07:28 +0200 Subject: [PATCH 05/13] Fix a bunch of stuff --- .../Localization/Monoidal/Braided.lean | 16 ++++---- .../Monoidal/Braided/Transport.lean | 2 +- .../LightProfinite/ChosenFiniteProducts.lean | 12 +++--- LeanCondensed/Projects/Epi.lean | 3 +- LeanCondensed/Projects/LocalizedMonoidal.lean | 38 +++++++++---------- LeanCondensed/Projects/OverN.lean | 1 - 6 files changed, 35 insertions(+), 37 deletions(-) diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean index e437dae..34281a0 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean @@ -100,8 +100,8 @@ lemma braidingNatIso_hom_μ_right (X Y Z : C) : @[reassoc] lemma braiding_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : X' ⟶ Y') : - (f ⊗ g) ≫ ((braidingNatIso L W ε).hom.app Y).app Y' = - ((braidingNatIso L W ε).hom.app X).app X' ≫ (g ⊗ f) := by + (f ⊗ₘ g) ≫ ((braidingNatIso L W ε).hom.app Y).app Y' = + ((braidingNatIso L W ε).hom.app X).app X' ≫ (g ⊗ₘ f) := by rw [← id_comp f, ← comp_id g, tensor_comp, id_tensorHom, tensorHom_id, tensor_comp, id_tensorHom, tensorHom_id, ← assoc] erw [← ((braidingNatIso L W ε).app _).hom.naturality g] @@ -176,8 +176,8 @@ noncomputable instance : BraidedCategory (LocalizedMonoidal L W ε) where (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj y)).hom ▷ ((L').obj z) ≫ (α_ ((L').obj y) ((L').obj x) ((L').obj z)).hom ≫ ((L').obj y) ◁ (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj z)).hom by - refine Eq.trans ?_ ((((eX.inv ⊗ eY.inv) ⊗ eZ.inv) ≫= this =≫ - (eY.hom ⊗ eZ.hom ⊗ eX.hom)).trans ?_) + refine Eq.trans ?_ ((((eX.inv ⊗ₘ eY.inv) ⊗ₘ eZ.inv) ≫= this =≫ + (eY.hom ⊗ₘ eZ.hom ⊗ₘ eX.hom)).trans ?_) · simp only [Iso.app_hom, associator_conjugation, Functor.flip_obj_obj, assoc, Iso.inv_hom_id_assoc, Iso.cancel_iso_hom_left] rw [← Iso.eq_comp_inv] @@ -200,8 +200,8 @@ noncomputable instance : BraidedCategory (LocalizedMonoidal L W ε) where ((L').obj x) ◁ (((braidingNatIso L W ε).app ((L').obj y)).app ((L').obj z)).hom ≫ (α_ ((L').obj x) ((L').obj z) ((L').obj y)).inv ≫ (((braidingNatIso L W ε).app ((L').obj x)).app ((L').obj z)).hom ▷ ((L').obj y) by - refine Eq.trans ?_ (((eX.inv ⊗ (eY.inv ⊗ eZ.inv)) ≫= this =≫ - ((eZ.hom ⊗ eX.hom) ⊗ eY.hom)).trans ?_) + refine Eq.trans ?_ (((eX.inv ⊗ₘ (eY.inv ⊗ₘ eZ.inv)) ≫= this =≫ + ((eZ.hom ⊗ₘ eX.hom) ⊗ₘ eY.hom)).trans ?_) · simp [← braiding_naturality_assoc, ← whiskerLeft_comp_assoc] · simp only [Functor.flip_obj_obj, Iso.app_hom, assoc, ← id_tensorHom] rw [← tensor_comp_assoc, braiding_naturality] @@ -243,8 +243,8 @@ noncomputable instance : SymmetricCategory (LocalizedMonoidal L W ε) where obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ obtain ⟨y, ⟨eY⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ suffices (β_ ((L').obj x) ((L').obj y)).hom ≫ (β_ ((L').obj y) ((L').obj x)).hom = 𝟙 _ by - refine Eq.trans ?_ (((eX.inv ⊗ eY.inv) ≫= this =≫ - (eX.hom ⊗ eY.hom)).trans ?_) + refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ + (eX.hom ⊗ₘ eY.hom)).trans ?_) all_goals simp simp [-Functor.map_braiding, β_hom_app, ← Functor.map_comp_assoc] diff --git a/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean b/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean index 08b599e..f617c0c 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean @@ -33,7 +33,7 @@ Given two lax monoidal, monoidally isomorphic functors, if one is lax braided, s def ofNatIso (F G : C ⥤ D) (i : F ≅ G) [F.LaxBraided] [G.LaxMonoidal] [NatTrans.IsMonoidal i.hom] : G.LaxBraided where braided X Y := by - have (X Y : C) : μ G X Y = (i.inv.app X ⊗ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by + have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by simp [NatTrans.IsMonoidal.tensor X Y, ← tensor_comp_assoc] rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc] simp diff --git a/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean b/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean index ca0b0dd..e72b78d 100644 --- a/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean +++ b/LeanCondensed/Mathlib/Topology/Category/LightProfinite/ChosenFiniteProducts.lean @@ -44,13 +44,13 @@ noncomputable def productIsLimit : IsLimit (productCone X Y hP) where apply_fun fun e => e x at h exact h -noncomputable def chosenFiniteProducts (hP : ∀ (X Y : CompHausLike.{u} P), HasProp P (X × Y)) - [HasProp P PUnit.{u + 1}] : ChosenFiniteProducts (CompHausLike.{u} P) where - product X Y := ⟨productCone X Y (hP X Y), productIsLimit X Y (hP X Y)⟩ - terminal := ⟨_, CompHausLike.isTerminalPUnit⟩ +-- noncomputable def chosenFiniteProducts (hP : ∀ (X Y : CompHausLike.{u} P), HasProp P (X × Y)) +-- [HasProp P PUnit.{u + 1}] : CartesianMonoidalCategory (CompHausLike.{u} P) where +-- tensorProductIsBinaryProduct X Y := productIsLimit X Y (hP X Y) +-- isTerminalTensorUnit := CompHausLike.isTerminalPUnit -noncomputable instance : ChosenFiniteProducts LightProfinite.{u} := - chosenFiniteProducts (fun _ _ => inferInstance) +noncomputable instance : CartesianMonoidalCategory LightProfinite.{u} := + CartesianMonoidalCategory.ofChosenFiniteProducts ⟨_, (CompHausLike.isTerminalPUnit)⟩ (fun X Y ↦ ⟨_, (productIsLimit X Y (inferInstance))⟩) example : LightProfinite ⥤ TopCat := by exact LightProfinite.toTopCat diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index 1bb6204..6b65e53 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -45,8 +45,7 @@ instance surj_widePullback {J : Type*} (B : LightProfinite.{u}) (objs : J → Li intro j unfold point_maps by_cases h : i = j - · simp only [↓reduceDIte] - rw [dif_pos h] + · rw [dif_pos h] subst h rfl · rw [dif_neg h] diff --git a/LeanCondensed/Projects/LocalizedMonoidal.lean b/LeanCondensed/Projects/LocalizedMonoidal.lean index 6cc3e84..4743a16 100644 --- a/LeanCondensed/Projects/LocalizedMonoidal.lean +++ b/LeanCondensed/Projects/LocalizedMonoidal.lean @@ -13,7 +13,7 @@ universe u namespace CategoryTheory -open CategoryTheory Limits Opposite Monoidal MonoidalCategory +open CategoryTheory Functor Limits Opposite Monoidal MonoidalCategory namespace Functor.Monoidal @@ -47,24 +47,24 @@ set_option maxHeartbeats 300000 in instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] [MonoidalCategory E] (L : D ⥤ E) [L.LaxMonoidal] : ((whiskeringRight C D E).obj L).LaxMonoidal where - ε' := { app X := Functor.LaxMonoidal.ε L } - μ' F G := { app X := Functor.LaxMonoidal.μ L (F.obj X) (G.obj X) } + ε := { app X := Functor.LaxMonoidal.ε L } + μ F G := { app X := Functor.LaxMonoidal.μ L (F.obj X) (G.obj X) } set_option maxHeartbeats 300000 in instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] [MonoidalCategory E] (L : D ⥤ E) [L.OplaxMonoidal] : ((whiskeringRight C D E).obj L).OplaxMonoidal where - η' := { app X := Functor.OplaxMonoidal.η L } - δ' F G := { app X := Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X) } - oplax_left_unitality' := by aesop -- `aesop_cat` fails for some reason - oplax_right_unitality' := by aesop -- `aesop_cat` fails for some reason + η := { app X := Functor.OplaxMonoidal.η L } + δ F G := { app X := Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X) } + oplax_left_unitality := by aesop -- `aesop_cat` fails for some reason + oplax_right_unitality := by aesop -- `aesop_cat` fails for some reason instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategory D] [MonoidalCategory E] (L : D ⥤ E) [L.Monoidal] : ((whiskeringRight C D E).obj L).Monoidal where - ε_η := by ext; exact Functor.Monoidal.ε_η - η_ε := by ext; exact Functor.Monoidal.η_ε - μ_δ _ _ := by ext; exact Functor.Monoidal.μ_δ _ _ - δ_μ _ _ := by ext; exact Functor.Monoidal.δ_μ _ _ + ε_η := by ext; exact Functor.Monoidal.ε_η _ + η_ε := by ext; exact Functor.Monoidal.η_ε _ + μ_δ _ _ := by ext; apply Functor.Monoidal.μ_δ + δ_μ _ _ := by ext; apply Functor.Monoidal.δ_μ end FunctorCategory @@ -165,7 +165,7 @@ noncomputable def μNatIso : ((((whiskeringLeft₂ _).obj F).obj F).obj (curried ext simp only [Functor.comp_obj, whiskeringRight_obj_obj, curriedTensor_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_obj, Functor.comp_map, whiskeringRight_obj_map, - NatTrans.comp_app, whiskerRight_app, curriedTensor_map_app, NatIso.ofComponents_hom_app, + NatTrans.comp_app, Functor.whiskerRight_app, curriedTensor_map_app, NatIso.ofComponents_hom_app, Iso.symm_hom, μIso_inv, whiskeringLeft₂_obj_obj_obj_map_app] change _ = _ ≫ (L' ⋙ F).map _ rw [map_whiskerRight] @@ -186,8 +186,8 @@ lemma μNatIso_inv_app_app (X Y : C) : @[reassoc] lemma μNatIso_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ X') (g : Y ⟶ Y') : - (F.map f ⊗ F.map g) ≫ ((μNatIso L W ε F).hom.app X').app Y' = - ((μNatIso L W ε F).hom.app X).app Y ≫ F.map (f ⊗ g) := by + (F.map f ⊗ₘ F.map g) ≫ ((μNatIso L W ε F).hom.app X').app Y' = + ((μNatIso L W ε F).hom.app X).app Y ≫ F.map (f ⊗ₘ g) := by have := ((μNatIso L W ε F).hom.app X').naturality g simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_map, curriedTensor_obj_map, @@ -198,7 +198,7 @@ lemma μNatIso_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ X') apply NatTrans.congr_app at this simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, NatTrans.comp_app, whiskeringLeft₂_obj_obj_obj_map_app, - curriedTensor_map_app, Functor.comp_map, whiskeringRight_obj_map, whiskerRight_app] at this + curriedTensor_map_app, Functor.comp_map, whiskeringRight_obj_map, Functor.whiskerRight_app] at this specialize this Y rw [MonoidalCategory.tensorHom_id, ← Category.assoc, this] rw [Category.assoc, ← F.map_comp] @@ -227,7 +227,7 @@ lemma μNatIso_associativity_aux (X Y Z : C) : simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, NatTrans.comp_app, whiskeringLeft₂_obj_obj_obj_map_app, curriedTensor_map_app, Functor.comp_map, - whiskeringRight_obj_map, whiskerRight_app] at this + whiskeringRight_obj_map, Functor.whiskerRight_app] at this change _ = _ ≫ (F.mapIso ((Functor.mapIso _ (Functor.Monoidal.μIso L' _ _)).app _)).hom at this rw [← Iso.comp_inv_eq] at this simp only [Functor.mapIso_inv, Iso.app_inv, Category.assoc] at this @@ -267,11 +267,11 @@ noncomputable def functorCoremonoidalOfComp : F.CoreMonoidal where (α_ (F.obj ((L').obj x)) (F.obj ((L').obj y)) (F.obj ((L').obj z))).hom ≫ F.obj ((L').obj x) ◁ ((μNatIso L W ε F).hom.app ((L').obj y)).app ((L').obj z) ≫ ((μNatIso L W ε F).hom.app ((L').obj x)).app (((L').obj y) ⊗ ((L').obj z)) by - refine Eq.trans ?_ ((((F.map eX.inv ⊗ F.map eY.inv) ⊗ F.map eZ.inv) ≫= this =≫ - (F.map (eX.hom ⊗ eY.hom ⊗ eZ.hom))).trans ?_) + refine Eq.trans ?_ ((((F.map eX.inv ⊗ₘ F.map eY.inv) ⊗ₘ F.map eZ.inv) ≫= this =≫ + (F.map (eX.hom ⊗ₘ eY.hom ⊗ₘ eZ.hom))).trans ?_) · simp only [Category.assoc] rw [← F.map_comp, ← associator_naturality, F.map_comp, ← μNatIso_naturality_assoc] - rw [← Category.comp_id (F.map eZ.inv), ← Category.id_comp (F.map eX.inv ⊗ F.map eY.inv)] + rw [← Category.comp_id (F.map eZ.inv), ← Category.id_comp (F.map eX.inv ⊗ₘ F.map eY.inv)] rw [MonoidalCategory.tensor_comp, MonoidalCategory.tensorHom_id] simp only [MonoidalCategory.id_tensorHom, whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, Category.assoc] diff --git a/LeanCondensed/Projects/OverN.lean b/LeanCondensed/Projects/OverN.lean index 3d8ccaa..9a6320f 100644 --- a/LeanCondensed/Projects/OverN.lean +++ b/LeanCondensed/Projects/OverN.lean @@ -3,7 +3,6 @@ import LeanCondensed.Projects.Pullbacks open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom - ChosenFiniteProducts lemma IsClosedThingy {T : LightProfinite} (f : T ⟶ ℕ∪{∞}) (s : ℕ → Set T) From 8e5b826b905dcb551c1b61f08f39595182c85055 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Tue, 8 Jul 2025 16:13:44 +0200 Subject: [PATCH 06/13] All but one error --- LeanCondensed/Projects/MonoidalLinear.lean | 16 ++++++++-------- LeanCondensed/Projects/SheafMonoidal.lean | 16 ++++++++-------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/LeanCondensed/Projects/MonoidalLinear.lean b/LeanCondensed/Projects/MonoidalLinear.lean index b1b1d7d..e591efb 100644 --- a/LeanCondensed/Projects/MonoidalLinear.lean +++ b/LeanCondensed/Projects/MonoidalLinear.lean @@ -58,7 +58,7 @@ def monoidalPreadditive [L.Additive] (R : D ⥤ C) [R.Full] [R.Faithful] (adj : obtain ⟨Y', ⟨eY⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ obtain ⟨Z', ⟨eZ⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Z) := ⟨_, ⟨(L').objObjPreimageIso Z⟩⟩ suffices (L').obj X' ◁ (0 : (L').obj Y' ⟶ (L').obj Z') = 0 by - refine Eq.trans ?_ (((eX.inv ⊗ eY.inv) ≫= this =≫ (eX.hom ⊗ eZ.hom)).trans ?_) + refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ (eX.hom ⊗ₘ eZ.hom)).trans ?_) · rw [← id_tensorHom, ← id_tensorHom, ← tensor_comp, ← tensor_comp] simp · simp @@ -69,7 +69,7 @@ def monoidalPreadditive [L.Additive] (R : D ⥤ C) [R.Full] [R.Faithful] (adj : obtain ⟨Y', ⟨eY⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y) := ⟨_, ⟨(L').objObjPreimageIso Y⟩⟩ obtain ⟨Z', ⟨eZ⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Z) := ⟨_, ⟨(L').objObjPreimageIso Z⟩⟩ suffices (0 : (L').obj Y' ⟶ (L').obj Z') ▷ (L').obj X' = 0 by - refine Eq.trans ?_ (((eY.inv ⊗ eX.inv) ≫= this =≫ (eZ.hom ⊗ eX.hom)).trans ?_) + refine Eq.trans ?_ (((eY.inv ⊗ₘ eX.inv) ≫= this =≫ (eZ.hom ⊗ₘ eX.hom)).trans ?_) · rw [← tensorHom_id, ← tensorHom_id, ← tensor_comp, ← tensor_comp] simp · simp @@ -81,7 +81,7 @@ def monoidalPreadditive [L.Additive] (R : D ⥤ C) [R.Full] [R.Faithful] (adj : let eZ : (L').obj (R.obj Z) ≅ Z := asIso (adj.counit.app Z) suffices (L').obj (R.obj X) ◁ ((L').map (R.map f) + (L').map (R.map g)) = ((L').obj (R.obj X) ◁ (L').map (R.map f)) + ((L').obj (R.obj X) ◁ (L').map (R.map g)) by - refine Eq.trans ?_ (((eX.inv ⊗ eY.inv) ≫= this =≫ (eX.hom ⊗ eZ.hom)).trans ?_) + refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ (eX.hom ⊗ₘ eZ.hom)).trans ?_) · rw [← id_tensorHom, ← id_tensorHom, ← tensor_comp_assoc, ← Functor.map_add, ← tensor_comp] simp [eZ, eY] · rw [← id_tensorHom, ← id_tensorHom, ← id_tensorHom, @@ -96,7 +96,7 @@ def monoidalPreadditive [L.Additive] (R : D ⥤ C) [R.Full] [R.Faithful] (adj : let eZ : (L').obj (R.obj Z) ≅ Z := asIso (adj.counit.app Z) suffices ((L').map (R.map f) + (L').map (R.map g)) ▷ (L').obj (R.obj X) = ((L').map (R.map f)) ▷ (L').obj (R.obj X) + ((L').map (R.map g) ▷ (L').obj (R.obj X)) by - refine Eq.trans ?_ (((eY.inv ⊗ eX.inv) ≫= this =≫ (eZ.hom ⊗ eX.hom)).trans ?_) + refine Eq.trans ?_ (((eY.inv ⊗ₘ eX.inv) ≫= this =≫ (eZ.hom ⊗ₘ eX.hom)).trans ?_) · rw [← tensorHom_id, ← tensorHom_id, ← tensor_comp_assoc, ← Functor.map_add, ← tensor_comp] simp [eZ, eY] · rw [← tensorHom_id, ← tensorHom_id, ← tensorHom_id, @@ -121,7 +121,7 @@ def monoidalLinear (A : Type u) [Ring A] [L.Additive] (R : D ⥤ C) [R.Full] [R. let eZ : (L').obj (R.obj Z) ≅ Z := asIso (adj.counit.app Z) suffices ((L').obj (R.obj X)) ◁ (r • (L').map (R.map f)) = r • ((L').obj (R.obj X)) ◁ ((L').map (R.map f)) by - refine Eq.trans ?_ (((eX.inv ⊗ eY.inv) ≫= this =≫ (eX.hom ⊗ eZ.hom)).trans ?_) + refine Eq.trans ?_ (((eX.inv ⊗ₘ eY.inv) ≫= this =≫ (eX.hom ⊗ₘ eZ.hom)).trans ?_) · rw [← id_tensorHom, ← id_tensorHom, ← tensor_comp_assoc, ← Functor.map_smul, ← tensor_comp] simp [eZ, eY] · simp [eX, eY, eZ, ← MonoidalCategory.id_tensorHom, ← MonoidalCategory.tensor_comp] @@ -133,7 +133,7 @@ def monoidalLinear (A : Type u) [Ring A] [L.Additive] (R : D ⥤ C) [R.Full] [R. let eZ : (L').obj (R.obj Z) ≅ Z := asIso (adj.counit.app Z) suffices (r • (L').map (R.map f)) ▷ ((L').obj (R.obj X)) = r • ((L').map (R.map f)) ▷ ((L').obj (R.obj X)) by - refine Eq.trans ?_ (((eY.inv ⊗ eX.inv) ≫= this =≫ (eZ.hom ⊗ eX.hom)).trans ?_) + refine Eq.trans ?_ (((eY.inv ⊗ₘ eX.inv) ≫= this =≫ (eZ.hom ⊗ₘ eX.hom)).trans ?_) · rw [← tensorHom_id, ← tensorHom_id, ← tensor_comp_assoc, ← Functor.map_smul, ← tensor_comp] simp [eZ, eY] · simp [eX, eY, eZ, ← MonoidalCategory.tensorHom_id, ← MonoidalCategory.tensor_comp] @@ -166,12 +166,12 @@ instance [Linear R A] : Linear R (Sheaf J A) where smul_comp X Y Z r f g := by have : (r • f.val) ≫ g.val = r • (f.val ≫ g.val) := by simp apply hom_ext - simp only [instCategorySheaf_comp_val] + simp only [comp_val] exact this comp_smul X Y Z f r g := by have : f.val ≫ (r • g.val) = r • (f.val ≫ g.val) := by simp apply hom_ext - simp only [instCategorySheaf_comp_val] + simp only [comp_val] exact this end Linear diff --git a/LeanCondensed/Projects/SheafMonoidal.lean b/LeanCondensed/Projects/SheafMonoidal.lean index 382c57b..073396d 100644 --- a/LeanCondensed/Projects/SheafMonoidal.lean +++ b/LeanCondensed/Projects/SheafMonoidal.lean @@ -59,14 +59,14 @@ noncomputable instance : letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm -noncomputable instance foo : - letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A - (composeAndSheafify J F).Monoidal := by - letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A - letI : (presheafToSheaf J (Type (max u v))).Monoidal := sorry - exact - Functor.Monoidal.instComp (sheafToPresheaf J (Type (max u v))) - ((whiskeringRight Cᵒᵖ (Type (max u v)) A).obj F ⋙ presheafToSheaf J A) +-- noncomputable instance foo : +-- letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A +-- (composeAndSheafify J F).Monoidal := by +-- letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A +-- letI : (presheafToSheaf J (Type (max u v))).Monoidal := sorry +-- exact +-- Functor.Monoidal.instComp (sheafToPresheaf J (Type (max u v))) +-- ((whiskeringRight Cᵒᵖ (Type (max u v)) A).obj F ⋙ presheafToSheaf J A) end From 6b8e0ba26e9af12532bfed77dedad9990e49dedc Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Tue, 8 Jul 2025 16:36:35 +0200 Subject: [PATCH 07/13] Went through all files --- LeanCondensed/LightCondensed/Yoneda.lean | 2 +- .../Localization/Monoidal/Braided.lean | 2 +- .../CategoryTheory/Sites/DirectImage.lean | 2 + LeanCondensed/Projects/LocalizedMonoidal.lean | 12 +- LeanCondensed/Projects/PreservesCoprod.lean | 130 ++++++++---------- LeanCondensed/Projects/SheafMonoidal.lean | 1 - 6 files changed, 68 insertions(+), 81 deletions(-) diff --git a/LeanCondensed/LightCondensed/Yoneda.lean b/LeanCondensed/LightCondensed/Yoneda.lean index 6c4f176..fa170d5 100644 --- a/LeanCondensed/LightCondensed/Yoneda.lean +++ b/LeanCondensed/LightCondensed/Yoneda.lean @@ -54,7 +54,7 @@ lemma freeYoneda_symm_naturality {S S' : LightProfinite} (f : S' ⟶ S) (A : Lig (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, Functor.id_obj] + Adjunction.homEquiv_counit] simp only [← Category.assoc, ← Functor.map_comp] erw [yoneda_symm_naturality] rfl diff --git a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean index 34281a0..a638761 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean @@ -205,7 +205,7 @@ noncomputable instance : BraidedCategory (LocalizedMonoidal L W ε) where · simp [← braiding_naturality_assoc, ← whiskerLeft_comp_assoc] · simp only [Functor.flip_obj_obj, Iso.app_hom, assoc, ← id_tensorHom] rw [← tensor_comp_assoc, braiding_naturality] - simp only [comp_id, Functor.flip_obj_obj, assoc, associator_conjugation, + simp only [comp_id, Functor.flip_obj_obj, associator_conjugation, MonoidalCategory.id_tensorHom] rw [← id_comp eX.inv, tensor_comp, id_tensorHom] simp only [← associator_conjugation] diff --git a/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean b/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean index dc9e037..d789803 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Sites/DirectImage.lean @@ -15,6 +15,8 @@ noncomputable section namespace CategoryTheory +open Functor + variable {C D : Type*} [Category C] [Category D] variable (J : GrothendieckTopology C) (K : GrothendieckTopology D) variable (A : Type*) [Category A] [HasWeakSheafify K A] -- [HasWeakSheafify J A] diff --git a/LeanCondensed/Projects/LocalizedMonoidal.lean b/LeanCondensed/Projects/LocalizedMonoidal.lean index 4743a16..d6ab2cf 100644 --- a/LeanCondensed/Projects/LocalizedMonoidal.lean +++ b/LeanCondensed/Projects/LocalizedMonoidal.lean @@ -93,7 +93,7 @@ def coreMonoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.CoreMon simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc, Iso.inv_hom_id_assoc] rw [← tensorHom_id, associator_naturality_assoc] - simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp, ← tensor_comp_assoc] + simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp_assoc] left_unitality X := by simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom, μIso_hom, Category.assoc, ← tensor_comp_assoc, Iso.hom_inv_id_app, Category.comp_id, @@ -166,7 +166,7 @@ noncomputable def μNatIso : ((((whiskeringLeft₂ _).obj F).obj F).obj (curried simp only [Functor.comp_obj, whiskeringRight_obj_obj, curriedTensor_obj_obj, whiskeringLeft₂_obj_obj_obj_obj_obj, Functor.comp_map, whiskeringRight_obj_map, NatTrans.comp_app, Functor.whiskerRight_app, curriedTensor_map_app, NatIso.ofComponents_hom_app, - Iso.symm_hom, μIso_inv, whiskeringLeft₂_obj_obj_obj_map_app] + whiskeringLeft₂_obj_obj_obj_map_app] change _ = _ ≫ (L' ⋙ F).map _ rw [map_whiskerRight] simp @@ -308,9 +308,9 @@ noncomputable def functorCoremonoidalOfComp : F.CoreMonoidal where curriedTensor_obj_obj, μNatIso_inv_app_app, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, comp_whiskerRight, μNatIso_hom_app_app, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, Category.assoc, Iso.map_inv_hom_id, Category.comp_id] - simp only [← MonoidalCategory.tensorHom_id, ← MonoidalCategory.id_tensorHom, ← - MonoidalCategory.tensor_comp, Category.comp_id, ← MonoidalCategory.tensor_comp_assoc, - map_δ_μ_assoc, μ_δ, Functor.comp_obj] + simp only [← MonoidalCategory.tensorHom_id, ← MonoidalCategory.id_tensorHom, + Category.comp_id, ← MonoidalCategory.tensor_comp_assoc, map_δ_μ_assoc, μ_δ, + Functor.comp_obj] simp left_unitality X := by obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ @@ -392,7 +392,7 @@ noncomputable def functorCoremonoidalOfComp : F.CoreMonoidal where MonoidalCategory.id_tensorHom, Category.assoc, ← Functor.map_comp] have : Functor.LaxMonoidal.ε L' = ε.inv := rfl rw [this, ← MonoidalCategory.whiskerLeft_comp_assoc] - simp only [Iso.hom_inv_id, id_whiskerRight, Category.id_comp, δ_μ_assoc, Functor.map_comp] + simp only [Iso.hom_inv_id, Functor.map_comp] slice_rhs 2 3 => rw [← MonoidalCategory.id_tensorHom, ← Functor.map_id, μNatIso_naturality] rw [@rightUnitor_inv_naturality_assoc] diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index 02465fe..c5f82c4 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -49,84 +49,70 @@ instance {n : ℕ} (S : Fin n → LightProfinite.{u}) : rw [←isIso_iff_bijective] infer_instance - have : ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) - = map := by - apply this.comp_left - simp only [Equiv.invFun_as_coe, mapIso_hom, map] - rw [ - ←Function.comp_assoc, - ] - erw [ - ←coe_comp - (f := (CategoryTheory.inv (piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed) - ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv)) - (g := ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom - ≫ piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed)), - ] - ext1 f - ext1 ⟨i⟩ - simp only [yoneda_obj_obj, Discrete.functor_obj_eq_as, coyoneda_obj_obj, Function.comp_apply, - coyoneda_map_app, Quiver.Hom.unop_op, types_comp_apply, yoneda_obj_map, Category.assoc, - Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, yoneda_apply, CategoryTheory.id_apply, map] + suffices ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) = map by + rw [this] + exact map_bij - 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 - ) _ + apply this.comp_left + simp only [mapIso_hom, map] + rw [ + ←Function.comp_assoc, + ] + erw [ + ←coe_comp + (f := (CategoryTheory.inv (piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed) + ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv)) + (g := ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom + ≫ piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed)), + ] + ext1 f + ext1 ⟨i⟩ + simp only [yoneda_obj_obj, Discrete.functor_obj_eq_as, coyoneda_obj_obj, Function.comp_apply, + coyoneda_map_app, Quiver.Hom.unop_op, types_comp_apply, yoneda_obj_map, Category.assoc, + Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, yoneda_apply, CategoryTheory.id_apply] - erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)] - rw [Types.productIso_inv_comp_π] - simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply] + change + ( + 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 + ) _ - let _ : X.val.obj (⟨∐ S⟩) ⟶ X.val.obj (∏ᶜ fun i ↦ ⟨S i⟩) := (X.val.map (opCoproductIsoProduct S).hom) + erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)] + rw [Types.productIso_inv_comp_π] + simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply] - let _ : X.val.obj (⟨∐ S⟩) ⟶ X.val.obj ⟨S i⟩ := - (X.val.map (opCoproductIsoProduct S).hom) ≫ piComparison X.val (fun i ↦ ⟨S i⟩) ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i - - change - _ = - (LightCondensed.yoneda (S i) X).symm ( - ( - (X.val.map (opCoproductIsoProduct S).hom) - ≫ piComparison X.val (fun i ↦ ⟨S i⟩) - ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i - ) - (LightCondensed.yoneda (∐ S) X f) + change + _ = + (LightCondensed.yoneda (S i) X).symm ( + ( + (X.val.map (opCoproductIsoProduct S).hom) + ≫ piComparison X.val (fun i ↦ ⟨S i⟩) + ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i ) - rw [ - piComparison_comp_π, - ←X.val.map_comp, - opCoproductIsoProduct_hom_comp_π - ] - rw [ - yoneda_obj_map, - ←unop_comp_assoc, - opCoproductIsoProduct_hom_comp_π, - Quiver.Hom.unop_op, - ι_comp_sigmaComparison_assoc, - ←yoneda_symm_naturality - ] - change _ = (lightProfiniteToLightCondSet.map (Sigma.ι S i) ≫ - (((LightCondensed.yoneda (∐ S) X).symm ∘ (LightCondensed.yoneda (∐ S) X)) f)) - rw [Equiv.symm_comp_self, id_eq] + (LightCondensed.yoneda (∐ S) X f) + ) - -- Now the approach is to write `(coyoneda.map (sigmaComparison _ _).op).app X` as - -- `piComparison X.val _` pre- and post-composed with isos given by the coyoneda lemma. - -- The issue is that the homs in `LightCondSet` a priori live in one universe higher than the - -- S-valued points of `X` (but they are small). There is some API in a file called - -- `LightCondensed/Yoneda.lean` in the condensed repo that might be helpful. - rw [this] - exact map_bij + 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, + ←yoneda_symm_naturality, + (yoneda _ _).symm_apply_apply + ] instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} where preserves n := diff --git a/LeanCondensed/Projects/SheafMonoidal.lean b/LeanCondensed/Projects/SheafMonoidal.lean index 073396d..4bd8d5b 100644 --- a/LeanCondensed/Projects/SheafMonoidal.lean +++ b/LeanCondensed/Projects/SheafMonoidal.lean @@ -5,7 +5,6 @@ Authors: Dagur Asgeirsson -/ import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced import Mathlib.CategoryTheory.Limits.Shapes.Countable -import Mathlib.CategoryTheory.Sites.ChosenFiniteProducts import Mathlib.CategoryTheory.Sites.LeftExact import Mathlib.CategoryTheory.Sites.Monoidal import Mathlib.CategoryTheory.Sites.PreservesSheafification From 77690ca9e07e8a5cc469ad499debd2d9d1eb55b9 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Wed, 9 Jul 2025 17:43:25 +0200 Subject: [PATCH 08/13] Changes --- .../Monoidal/Braided/Transport.lean | 1 + .../Mathlib/Condensed/Light/Monoidal.lean | 5 ++-- .../Projects/InternallyProjective.lean | 5 +++- LeanCondensed/Projects/Proj.lean | 14 +++++----- LeanCondensed/Projects/SheafMonoidal.lean | 26 +++++++++---------- 5 files changed, 28 insertions(+), 23 deletions(-) diff --git a/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean b/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean index f617c0c..f31b83b 100644 --- a/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean +++ b/LeanCondensed/Mathlib/CategoryTheory/Monoidal/Braided/Transport.lean @@ -92,6 +92,7 @@ instance (e : C ≌ D) [MonoidalCategory C] [BraidedCategory C] : Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, Functor.LaxMonoidal.comp_μ, Functor.comp_map, Equivalence.inv_fun_map, Functor.id_obj, Functor.OplaxMonoidal.comp_δ, assoc] at this simp [← this] + sorry instance Transported.instSymmetricCategory (e : C ≌ D) [MonoidalCategory C] [SymmetricCategory C] : SymmetricCategory (Transported e) := diff --git a/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean b/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean index 1a8ff93..4b38c48 100644 --- a/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean +++ b/LeanCondensed/Mathlib/Condensed/Light/Monoidal.lean @@ -17,7 +17,8 @@ universe u noncomputable section -open CategoryTheory Monoidal Sheaf MonoidalCategory MonoidalClosed MonoidalClosed.FunctorCategory +open CategoryTheory Functor Monoidal Sheaf MonoidalCategory MonoidalClosed + MonoidalClosed.FunctorCategory section @@ -177,7 +178,7 @@ instance : (free R).Monoidal := by whiskeringLeft_obj_map, Equivalence.op_functor, Equivalence.op_counitIso, isoWhiskerRight_trans, isoWhiskerRight_twice, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, isoWhiskerRight_hom, NatIso.op_inv, NatTrans.comp_app, - CategoryTheory.whiskerLeft_app, CategoryTheory.whiskerRight_app, + Functor.whiskerLeft_app, Functor.whiskerRight_app, Functor.associator_inv_app, Functor.associator_hom_app, Functor.id_obj, NatTrans.op_app, Functor.leftUnitor_hom_app, CategoryTheory.Functor.map_id, Category.comp_id, Category.id_comp, Category.assoc] diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean index 5978830..7cd58cb 100644 --- a/LeanCondensed/Projects/InternallyProjective.lean +++ b/LeanCondensed/Projects/InternallyProjective.lean @@ -48,6 +48,9 @@ def ihomPoints (A B : LightCondMod.{u} R) (S : LightProfinite) : -- 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. + +lemma tensorLeft_obj (X Y : LightCondMod.{u} R) : (tensorLeft X).obj Y = X ⊗ Y := rfl + lemma ihom_map_val_app (A B P : LightCondMod.{u} R) (S : LightProfinite) (e : A ⟶ B) : ∀ x, ConcreteCategory.hom (((ihom P).map e).val.app ⟨S⟩) x = (ihomPoints R P B S).symm (ihomPoints R P A S x ≫ e) := by @@ -99,7 +102,7 @@ lemma ihomPoints_symm_comp (B P : LightCondMod.{u} R) (S S' : LightProfinite) ( def tensorFreeIso (X Y : LightCondSet.{u}) : (free R).obj X ⊗ (free R).obj Y ≅ (free R).obj (X ⨯ Y) := Functor.Monoidal.μIso (free R) X Y ≪≫ ((free R).mapIso - ((ChosenFiniteProducts.product X Y).isLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)))) + ((CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y).conePointUniqueUpToIso (limit.isLimit (pair X Y)))) def tensorFreeIso' (S T : LightProfinite) : (free R).obj S.toCondensed ⊗ (free R).obj T.toCondensed ≅ diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index e6f0c77..bc148b0 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -11,7 +11,7 @@ import Mathlib open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom - ChosenFiniteProducts Topology + CartesianMonoidalCategory Topology universe u @@ -244,12 +244,12 @@ lemma xyz { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] (lift (𝟙 S') (CompHausLike.ofHom _ <| ContinuousMap.const S' n)) ( by - simp only [Category.assoc, limit.cone_x, prod.lift_map, Category.id_comp, - Category.comp_id] - apply ChosenFiniteProducts.hom_ext + simp only [Category.assoc, limit.cone_x] + apply CartesianMonoidalCategory.hom_ext · simp [y'] · ext - simp [←ConcreteCategory.comp_apply, fibre_condition] + simp only [Category.assoc, fibre_condition, tensorHom_id, lift_whiskerRight, + Category.id_comp, lift_snd, CompHausLike.hom_ofHom, ContinuousMap.const_apply] rfl ) have hσ : ∀ n, σ' n ≫ π_tilde ≫ fst _ _ = 𝟙 _ := by @@ -287,7 +287,7 @@ lemma xyz { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] t, by simp only [Set.mem_preimage, ConcreteCategory.comp_apply, ht, - Set.mem_singleton_iff, S', y', Ttilde, σ'] + Set.mem_singleton_iff] rfl ⟩ rw [ConcreteCategory.comp_apply] @@ -474,7 +474,7 @@ theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : Lig ≫ fst _ _ ≫ lift (𝟙 _) (CompHausLike.ofHom _ (ContinuousMap.const S' (∞ : ℕ∪{∞}))) := by - apply ChosenFiniteProducts.hom_ext _ _ (by simp) + apply CartesianMonoidalCategory.hom_ext _ _ (by simp) simp only [Category.assoc] rw [fibre_condition ∞ (π' ≫ snd _ _)] ext diff --git a/LeanCondensed/Projects/SheafMonoidal.lean b/LeanCondensed/Projects/SheafMonoidal.lean index 4bd8d5b..adb8d5d 100644 --- a/LeanCondensed/Projects/SheafMonoidal.lean +++ b/LeanCondensed/Projects/SheafMonoidal.lean @@ -13,7 +13,7 @@ import LeanCondensed.Projects.LocalizedMonoidal universe v u -open CategoryTheory MonoidalCategory +open CategoryTheory MonoidalCategory Functor namespace CategoryTheory.Functor.Monoidal @@ -37,11 +37,11 @@ variable {A B : Type*} [Category A] [Category B] attribute [local instance] monoidalCategory --- noncomputable instance : (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal := --- monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm +noncomputable instance : (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal := + monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm --- noncomputable instance : (composeAndSheafify J F).Monoidal := --- Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (Iso.refl _) _ +noncomputable instance : (composeAndSheafify J F).Monoidal := + Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (Iso.refl _) _ end @@ -58,14 +58,14 @@ noncomputable instance : letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm --- noncomputable instance foo : --- letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A --- (composeAndSheafify J F).Monoidal := by --- letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A --- letI : (presheafToSheaf J (Type (max u v))).Monoidal := sorry --- exact --- Functor.Monoidal.instComp (sheafToPresheaf J (Type (max u v))) --- ((whiskeringRight Cᵒᵖ (Type (max u v)) A).obj F ⋙ presheafToSheaf J A) +noncomputable instance foo : + letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A + (composeAndSheafify J F).Monoidal := by + letI : MonoidalCategory (Sheaf J A) := monoidalCategory J A + letI : (presheafToSheaf J (Type (max u v))).Monoidal := sorry + exact + Functor.Monoidal.instComp (sheafToPresheaf J (Type (max u v))) + ((whiskeringRight Cᵒᵖ (Type (max u v)) A).obj F ⋙ presheafToSheaf J A) end From 49f7342215296eb422793d707e4c84fe0614da2e Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Sat, 12 Jul 2025 13:02:39 +0200 Subject: [PATCH 09/13] Forgot to merge file --- LeanCondensed/Projects/LocalizedMonoidal.lean | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/LeanCondensed/Projects/LocalizedMonoidal.lean b/LeanCondensed/Projects/LocalizedMonoidal.lean index 3e2b211..d35603c 100644 --- a/LeanCondensed/Projects/LocalizedMonoidal.lean +++ b/LeanCondensed/Projects/LocalizedMonoidal.lean @@ -63,13 +63,8 @@ instance {C D E : Type*} [Category C] [Category D] [Category E] [MonoidalCategor [MonoidalCategory E] (L : D ⥤ E) [L.Monoidal] : ((whiskeringRight C D E).obj L).Monoidal where ε_η := by ext; exact Functor.Monoidal.ε_η _ η_ε := by ext; exact Functor.Monoidal.η_ε _ -<<<<<<< HEAD - μ_δ _ _ := by ext; apply Functor.Monoidal.μ_δ - δ_μ _ _ := by ext; apply Functor.Monoidal.δ_μ -======= μ_δ _ _ := by ext; exact Functor.Monoidal.μ_δ _ _ _ δ_μ _ _ := by ext; exact Functor.Monoidal.δ_μ _ _ _ ->>>>>>> upstream/master end FunctorCategory @@ -203,12 +198,8 @@ lemma μNatIso_naturality {X X' Y Y' : LocalizedMonoidal L W ε} (f : X ⟶ X') apply NatTrans.congr_app at this simp only [whiskeringLeft₂_obj_obj_obj_obj_obj, curriedTensor_obj_obj, Functor.comp_obj, whiskeringRight_obj_obj, NatTrans.comp_app, whiskeringLeft₂_obj_obj_obj_map_app, -<<<<<<< HEAD - curriedTensor_map_app, Functor.comp_map, whiskeringRight_obj_map, Functor.whiskerRight_app] at this -======= curriedTensor_map_app, Functor.comp_map, whiskeringRight_obj_map, Functor.whiskerRight_app] at this ->>>>>>> upstream/master specialize this Y rw [MonoidalCategory.tensorHom_id, ← Category.assoc, this] rw [Category.assoc, ← F.map_comp] @@ -319,13 +310,8 @@ noncomputable def functorCoremonoidalOfComp : F.CoreMonoidal where comp_whiskerRight, μNatIso_hom_app_app, Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, Category.assoc, Iso.map_inv_hom_id, Category.comp_id] simp only [← MonoidalCategory.tensorHom_id, ← MonoidalCategory.id_tensorHom, -<<<<<<< HEAD - Category.comp_id, ← MonoidalCategory.tensor_comp_assoc, map_δ_μ_assoc, μ_δ, - Functor.comp_obj] -======= ← MonoidalCategory.tensor_comp, Category.comp_id, ← MonoidalCategory.tensor_comp_assoc, map_δ_μ_assoc, μ_δ, Functor.comp_obj] ->>>>>>> upstream/master simp left_unitality X := by obtain ⟨x, ⟨eX⟩⟩ : ∃ x, Nonempty ((L').obj x ≅ X) := ⟨_, ⟨(L').objObjPreimageIso X⟩⟩ From 95984ccfef5cd7c1ea3e02bc41a80ae69621cb31 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Mon, 14 Jul 2025 14:10:19 +0200 Subject: [PATCH 10/13] Version for thesis --- LeanCondensed/Projects/Epi.lean | 4 +- .../Projects/InternallyProjective.lean | 11 + LeanCondensed/Projects/LightSolid.lean | 20 +- LeanCondensed/Projects/OverN.lean | 45 --- LeanCondensed/Projects/PreservesEpi.lean | 107 ------- LeanCondensed/Projects/Proj.lean | 286 ++++++++++++++---- LeanCondensed/Projects/Pullbacks.lean | 1 + LeanCondensed/Projects/Sequence.lean | 53 ++++ 8 files changed, 302 insertions(+), 225 deletions(-) delete mode 100644 LeanCondensed/Projects/OverN.lean delete mode 100644 LeanCondensed/Projects/PreservesEpi.lean create mode 100644 LeanCondensed/Projects/Sequence.lean diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index 6b65e53..cbb43d5 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -73,7 +73,9 @@ instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := { } lemma stupid {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y - := congr_arg (fun (a : s) ↦ (↑a : A)) h + := by + rw [Subtype.ext_iff] at h + exact h noncomputable def πpair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet := parallelPair diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean index 8f264a5..ccf2e84 100644 --- a/LeanCondensed/Projects/InternallyProjective.lean +++ b/LeanCondensed/Projects/InternallyProjective.lean @@ -5,6 +5,7 @@ Authors: Dagur Asgeirsson -/ import Mathlib.Condensed.Light.Epi import LeanCondensed.LightCondensed.Yoneda +import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono import LeanCondensed.Mathlib.Condensed.Light.Limits import LeanCondensed.Mathlib.Condensed.Light.Monoidal import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts @@ -30,6 +31,16 @@ variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C] class InternallyProjective (P : C) : Prop where preserves_epi : (ihom P).PreservesEpimorphisms +theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X) + : InternallyProjective Y := + haveI : Retract (ihom Y) (ihom X) := { + i := MonoidalClosed.pre r.r + r := MonoidalClosed.pre r.i + retract := by + rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id] + } + InternallyProjective.mk <| preservesEpi_ofRetract this proj.preserves_epi + end InternallyProjective open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean index 4a8ce58..48503ac 100644 --- a/LeanCondensed/Projects/LightSolid.lean +++ b/LeanCondensed/Projects/LightSolid.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Dagur Asgeirsson -/ import LeanCondensed.Projects.InternallyProjective +import LeanCondensed.Projects.Proj +import LeanCondensed.Projects.Sequence /-! # Project: light solid abelian groups @@ -47,7 +49,7 @@ def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := TopCat.ofHom { intro U h hU simp only [isOpen_iff_of_mem h, isClosed_discrete, isCompact_iff_finite, true_and] at hU refine ⟨sSup (Option.some ⁻¹' U)ᶜ + 1, fun n hn ↦ by - simpa using not_mem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ } + simpa using notMem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ } end LightProfinite @@ -56,20 +58,10 @@ namespace LightCondensed variable (R : Type _) [CommRing R] -- might need some more assumptions eventually, finite type over `ℤ`? -def P_map : - (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed := - (lightProfiniteToLightCondSet ⋙ free R).map (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) +instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := + internallyProjective_ℕinfty _ -def P : LightCondMod R := cokernel (P_map R) - -def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _ - -def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A) - (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf - -instance : InternallyProjective (P R) := sorry - -instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry +instance : InternallyProjective (P R) := ofRetract (P_retract _) inferInstance variable (R : Type) [CommRing R] diff --git a/LeanCondensed/Projects/OverN.lean b/LeanCondensed/Projects/OverN.lean deleted file mode 100644 index 9a6320f..0000000 --- a/LeanCondensed/Projects/OverN.lean +++ /dev/null @@ -1,45 +0,0 @@ -import Mathlib -import LeanCondensed.Projects.Pullbacks - -open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed - MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom - - -lemma IsClosedThingy {T : LightProfinite} (f : T ⟶ ℕ∪{∞}) (s : ℕ → Set T) - (hs : ∀ n (x : s n), f x = n) (hs' : ∀ n, IsClosed (s n)) : IsClosed ({t | f t = ∞} ∪ ⋃ n, s n) := by - apply IsClosed.mk - let fibre : ℕ → Set T := fun n ↦ f ⁻¹' {OnePoint.some n} - have clopen : ∀ n, IsClopen (fibre n) := by - intro n - refine IsClopen.preimage ⟨isClosed_singleton, ?_⟩ f.1.continuous - rw [isOpen_def] - refine ⟨fun h ↦ by simp at h, trivial⟩ - have : ({t | f t = ∞} ∪ ⋃ n, s n)ᶜ = ⋃ n, (s n)ᶜ ∩ fibre n := by - ext x - simp only [Set.compl_union, Set.compl_iUnion, Set.mem_inter_iff, Set.mem_compl_iff, - Set.mem_setOf_eq, Set.mem_iInter, Set.mem_iUnion] - constructor - · intro ⟨h, h'⟩ - obtain ⟨n', hn⟩ := Option.ne_none_iff_exists'.mp h - exact ⟨n', h' n', hn⟩ - · intro ⟨n, hn, hn'⟩ - refine ⟨?_, ?_⟩ - rw [hn'] - simp - intro i - by_cases h : i = n - rw [h] - exact hn - intro h' - have := hs i ⟨x, h'⟩ - apply h - simp [fibre] at hn' - rw [hn'] at this - rw [OnePoint.coe_eq_coe] at this - symm - exact this - rw [this] - refine isOpen_iUnion (fun i ↦ ?_) - apply IsOpen.inter - exact (hs' i).1 - exact (clopen i).2 diff --git a/LeanCondensed/Projects/PreservesEpi.lean b/LeanCondensed/Projects/PreservesEpi.lean deleted file mode 100644 index e5166e5..0000000 --- a/LeanCondensed/Projects/PreservesEpi.lean +++ /dev/null @@ -1,107 +0,0 @@ -import Mathlib - -import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono -import LeanCondensed.Projects.LightProfiniteInjective - - -universe u v - -open CategoryTheory Category Preadditive LightProfinite OnePoint Limits LightCondensed - -variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C] - -class InternallyProjective (P : C) : Prop where - preserves_epi : (ihom P).PreservesEpimorphisms - -namespace InternallyProjective - -theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X) - : InternallyProjective Y := - haveI : Retract (ihom Y) (ihom X) := { - i := MonoidalClosed.pre r.r - r := MonoidalClosed.pre r.i - retract := by - rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id] - } - InternallyProjective.mk <| preservesEpi_ofRetract this proj.preserves_epi - -end InternallyProjective - -open LightCondensed - -variable (R : Type _) [CommRing R] - -instance : TotallyDisconnectedSpace PUnit := by - have := TotallySeparatedSpace.of_discrete - apply TotallySeparatedSpace.totallyDisconnectedSpace - -def pt := LightProfinite.of PUnit.{1} - -def ι : pt ⟶ ℕ∪{∞} := (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) - -instance : Mono ι := (CompHausLike.mono_iff_injective ι).mpr fun _ _ ↦ congrFun rfl - -instance : Nonempty pt := by - unfold pt - infer_instance - -noncomputable def ι_SplitMono : SplitMono ι where - retraction := ((injective_of_light (LightProfinite.of PUnit.{1})).factors (𝟙 pt) ι).choose - id := ((injective_of_light pt).factors _ _).choose_spec - -noncomputable def P_map : - (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed := - (lightProfiniteToLightCondSet ⋙ free R).map (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) - -noncomputable def ιSplit : SplitMono (P_map R) := SplitMono.map ι_SplitMono (lightProfiniteToLightCondSet ⋙ (free R)) - -noncomputable def P : LightCondMod R := cokernel (P_map R) - -noncomputable def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _ - -noncomputable def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A) - (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf - -noncomputable def xyz := (Preadditive.homGroup _ _).sub (𝟙 (free R).obj (ℕ∪{∞}).toCondensed) ((ιSplit R).retraction ≫ ((lightProfiniteToLightCondSet ⋙ free R).map ι)) - -lemma comp_zero : P_map R ≫ xyz R = 0 := by - erw [ - Preadditive.comp_sub, - comp_id, - Functor.comp_map, - SplitMono.id_assoc, - sub_eq_zero - ] - rfl - -instance P_proj_Epi : Epi (P_proj R) := by - unfold P_proj - rw [←coequalizer_as_cokernel] - exact coequalizer.π_epi - -noncomputable def πSplit : SplitEpi (P_proj R) where - section_ := P_homMk R ((free R).obj (ℕ∪{∞}).toCondensed) (xyz R) (comp_zero _) - id := by - apply (P_proj_Epi R).left_cancellation - erw [ - cokernel.π_desc_assoc, - sub_comp, - id_comp, - assoc, - cokernel.condition, - HasZeroMorphisms.comp_zero, - sub_zero - ] - -noncomputable def r : Retract (P R) ((free R).obj ℕ∪{∞}.toCondensed) where - i := (πSplit R).section_ - r := P_proj R - retract := (πSplit R).id - -instance : MonoidalCategory (LightCondMod.{u} R) := sorry - -instance : MonoidalClosed (LightCondMod.{u} R) := sorry - -instance qwerty : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry - -theorem qwerty' : InternallyProjective (P R) := (qwerty _).ofRetract (r _) diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index bc148b0..7a075f7 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -1,7 +1,6 @@ import LeanCondensed.Projects.Epi import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.Initial -import LeanCondensed.Projects.OverN import LeanCondensed.Projects.InternallyProjective import LeanCondensed.Projects.PreservesCoprod import LeanCondensed.Mathlib.CategoryTheory.Countable @@ -32,6 +31,40 @@ def CategoryTheory.Limits.parallelPair.hom {C : Type*} [Category C] naturality := (by rintro _ _ ⟨_⟩ <;> simp [left, right]) } +lemma isClosed_fibres {T : LightProfinite} (f : T ⟶ ℕ∪{∞}) (s : ℕ → Set T) + (hs : ∀ n (x : s n), f x = n) (hs' : ∀ n, IsClosed (s n)) : IsClosed ({t | f t = ∞} ∪ ⋃ n, s n) := by + apply IsClosed.mk + let fibre : ℕ → Set T := fun n ↦ f ⁻¹' {OnePoint.some n} + have clopen : ∀ n, IsClopen (fibre n) := by + intro n + refine IsClopen.preimage ⟨isClosed_singleton, ?_⟩ f.1.continuous + exact ⟨fun h ↦ by simp at h, trivial⟩ + + suffices ({t | f t = ∞} ∪ ⋃ n, s n)ᶜ = ⋃ n, (s n)ᶜ ∩ fibre n by + rw [this] + exact isOpen_iUnion (fun i ↦ IsOpen.inter (hs' i).1 (clopen i).2) + + ext x + simp only [Set.compl_union, Set.compl_iUnion, Set.mem_inter_iff, Set.mem_compl_iff, + Set.mem_setOf_eq, Set.mem_iInter, Set.mem_iUnion] + constructor + · intro ⟨h, h'⟩ + obtain ⟨n', hn⟩ := Option.ne_none_iff_exists'.mp h + exact ⟨n', h' n', hn⟩ + · intro ⟨n, hn, hn'⟩ + refine ⟨?_, ?_⟩ + · rw [hn'] + exact OnePoint.coe_ne_infty _ + intro i + by_cases h : i = n + exact h ▸ hn + intro h' + have := hs i ⟨x, h'⟩ + apply h + rw [hn', OnePoint.coe_eq_coe,] at this + exact Eq.symm this + + set_option maxHeartbeats 500000 noncomputable def smart_cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : coprod T (explicitPullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)) ⟶ explicitPullback π π := coprod.desc @@ -58,11 +91,9 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep have : IsClosed space := by unfold space rw [Set.union_comm] - apply IsClosedThingy - intro n ⟨x, ⟨s, hs⟩⟩ - simp only [←hs, ←ConcreteCategory.comp_apply, Category.assoc] - exact hσ' n s - exact fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous) + exact isClosed_fibres _ _ + (fun n ⟨x, ⟨s, hs⟩⟩ ↦ by simp only [←hs, ←ConcreteCategory.comp_apply, hσ' _ _]) + (fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous)) let T' : LightProfinite := ⟨TopCat.of space, inferInstance, inferInstance⟩ @@ -78,17 +109,12 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep fun s ↦ ⟨σ' n s, by rcases n with (n | n) - · apply Or.inr - simp only [Set.mem_setOf_eq, ←ConcreteCategory.comp_apply]; - exact hσ' ∞ s + · exact Or.inr (hσ' ∞ s) · apply Or.inl rw [Set.mem_iUnion] exact ⟨n, s, rfl⟩ ⟩, - by - have : IsInducing i := by exact { eq_induced := rfl } - rw [IsInducing.continuous_iff this] - exact (σ' n).1.continuous + by continuity ⟩) have hσ'' : ∀ (n : ℕ∪{∞}) (t : T'), t ∈ Set.range (σ n) → (i ≫ π ≫ fst _ _ ≫ σ n) t = t := by @@ -105,8 +131,7 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep rw [Category.id_comp, hs] have coe_i : ∀ (t : T'), ↑t = i t := fun _ ↦ rfl - - have σ_i : ∀ n, σ' n = σ n ≫ i := fun n ↦ rfl + have σ_i : ∀ n, σ' n = σ n ≫ i := fun _ ↦ rfl have hT' : ∀ (n : ℕ) t, t ∈ Set.range (σ n) ↔ (i ≫ π ≫ snd _ _) t = n := by intro n t' @@ -146,8 +171,7 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep · rw [LightProfinite.epi_iff_surjective] intro ⟨⟨t,t'⟩, ht⟩ by_cases h : (i ≫ π ≫ snd _ _) t = ∞ - · unfold smart_cover - have : (i ≫ π ≫ snd _ _) t' = ∞ := by + · have : (i ≫ π ≫ snd _ _) t' = ∞ := by rw [←Category.assoc, ConcreteCategory.comp_apply, ←ht, ←ConcreteCategory.comp_apply, Category.assoc, h ] @@ -163,15 +187,14 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep ⟩ let p := coprod.inr (X := T') (Y := (explicitPullback _ _)) x use coprod.inr (X := T') (Y := (explicitPullback _ _)) x - rw [←ConcreteCategory.comp_apply] - simp only [←Category.assoc, coprod.inr_desc] + rw [smart_cover, ←ConcreteCategory.comp_apply] + simp only [coprod.inr_desc] rfl · rw [←ne_eq, OnePoint.ne_infty_iff_exists] at h obtain ⟨n, hn⟩ := h symm at hn use coprod.inl (X := T') (Y := (explicitPullback _ _)) ((i ≫ π ≫ fst _ _ ≫ σ n) t) - unfold smart_cover - simp only [←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc] + simp only [smart_cover, ←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc] rw [ ←Category.assoc (fst _ _), ←Category.assoc π, ←Category.assoc i, ConcreteCategory.comp_apply @@ -198,10 +221,168 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (σ n), hs, hs' ] - erw [←Category.assoc, ConcreteCategory.comp_apply,ConcreteCategory.comp_apply (i ≫ π), ht] + erw [←Category.assoc, ConcreteCategory.comp_apply, + ConcreteCategory.comp_apply (i ≫ π), ht] rfl - · rw [hT'] - exact hn + · exact (hT' _ _).mpr hn + · have : σ ∞ ≫ i = σ' ∞ := rfl + + let σσ : S ⟶ fibre ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) := + fibreLift ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞) + + exact ⟨⟨ + σσ, + by + simp only [←Category.assoc] + rw [ + fibreLift_comp ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞), + ] + erw [hσ] + ⟩⟩ + +lemma subspaceCover' { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hepi : Epi π] + {σ' : ℕ∪{∞} → (S ⟶ T)} (hσ : ∀ n, σ' n ≫ π ≫ fst _ _ = 𝟙 _) + (hσ' : ∀ n s, (σ' n ≫ π ≫ snd S ℕ∪{∞}) s = ↑n) + : ∃ (T' : LightProfinite) (i : T' ⟶ T), + Epi (i ≫ π) ∧ Epi (smart_cover (i ≫ π)) + ∧ IsSplitEpi + (fibre_incl ∞ ((i ≫ π) ≫ snd _ _) ≫ i ≫ π ≫ fst S ℕ∪{∞}) := by + + let space : Set T := + Set.iUnion (fun (n : ℕ) ↦ Set.range (σ' (OnePoint.some n))) ∪ {t : T | (π ≫ snd _ _) t = ∞} + have : IsClosed space := by + unfold space + rw [Set.union_comm] + exact isClosed_fibres _ _ + (fun n ⟨x, ⟨s, hs⟩⟩ ↦ by simp only [←hs, ←ConcreteCategory.comp_apply, hσ' _ _]) + (fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous)) + + let T' : LightProfinite := ⟨TopCat.of space, inferInstance, inferInstance⟩ + + let i : T' ⟶ T := + CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩ + + have : Mono i := by + rw [CompHausLike.mono_iff_injective] + exact Subtype.val_injective + + let σ : ℕ∪{∞} → (S ⟶ T') := fun n ↦ (CompHausLike.ofHom _ + ⟨ + fun s ↦ ⟨σ' n s, + by + rcases n with (n | n) + · exact Or.inr (hσ' ∞ s) + · apply Or.inl + rw [Set.mem_iUnion] + exact ⟨n, s, rfl⟩ + ⟩, + by continuity + ⟩) + + have hσ'' : ∀ (n : ℕ∪{∞}) (t : T'), t ∈ Set.range (σ n) → (i ≫ π ≫ fst _ _ ≫ σ n) t = t := by + intro n t ht + obtain ⟨s, hs⟩ := ht + rw (config := { occs := .pos [1]}) [←hs] + rw [ + ←ConcreteCategory.comp_apply, + ←Category.assoc π, + ←Category.assoc i, + ←Category.assoc (σ n), + ] + erw [hσ] + rw [Category.id_comp, hs] + + have coe_i : ∀ (t : T'), ↑t = i t := fun _ ↦ rfl + have σ_i : ∀ n, σ' n = σ n ≫ i := fun _ ↦ rfl + + have hT' : ∀ (n : ℕ) t, t ∈ Set.range (σ n) ↔ (i ≫ π ≫ snd _ _) t = n := by + intro n t' + constructor <;> intro h + · obtain ⟨_, ht⟩ := h + rw [←ht, ←ConcreteCategory.comp_apply] + erw [hσ'] + · rcases t'.2 with (fin | inf) + · rw [Set.mem_iUnion] at fin + obtain ⟨j, ⟨s, hs⟩⟩ := fin + suffices h' : j = n by + rw [h'] at hs + use s + exact Subtype.ext hs + rw [coe_i] at hs + rw [ConcreteCategory.comp_apply, ←hs, ←ConcreteCategory.comp_apply, hσ'] at h + rw [←OnePoint.coe_eq_coe] + exact h + · simp only [Set.mem_setOf_eq] at inf + erw [inf] at h + exact (Option.some_ne_none n (Eq.symm h)).elim + + refine ⟨T', i, ?_, ?_, ?_⟩ + · rw [LightProfinite.epi_iff_surjective] + rintro ⟨s, (n | n)⟩ + obtain ⟨t, ht⟩ := (LightProfinite.epi_iff_surjective π).mp hepi ⟨s, none⟩ + have : t ∈ space := by apply Or.inr; rw [Set.mem_setOf_eq, ConcreteCategory.comp_apply, ht]; rfl + use ⟨t, this⟩ + rw [←ht] + rfl + · use σ n s + apply Prod.ext + change ConcreteCategory.hom (σ' n ≫ π ≫ fst _ _) s = s + rw [hσ]; rfl + change ConcreteCategory.hom (σ' n ≫ π ≫ snd _ _) s = (OnePoint.some n) + rw [hσ'] + · rw [LightProfinite.epi_iff_surjective] + intro ⟨⟨t,t'⟩, ht⟩ + simp only [Set.mem_setOf_eq] at ht + have proj_eq : (i ≫ π ≫ snd _ _) t = (i ≫ π ≫ snd _ _) t' := by + rw [←Category.assoc, ConcreteCategory.comp_apply, ht, + ←ConcreteCategory.comp_apply, Category.assoc + ] + by_cases h : (i ≫ π ≫ snd _ _) t = ∞ + · let x : explicitPullback (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) + (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) := + ⟨⟨⟨t, h⟩, ⟨t', by rw [Set.mem_preimage, Category.assoc, Set.mem_singleton_iff, ←proj_eq, h]⟩⟩, + by + simp only [Set.mem_setOf_eq] + rw [ConcreteCategory.comp_apply (fibre_incl _ _), ConcreteCategory.comp_apply (fibre_incl _ _)] + unfold fibre_incl + simp only [CompHausLike.hom_ofHom, ContinuousMap.coe_mk] + exact ht + ⟩ + let p := coprod.inr (X := T') (Y := (explicitPullback _ _)) x + use coprod.inr (X := T') (Y := (explicitPullback _ _)) x + rw [smart_cover, ←ConcreteCategory.comp_apply] + simp only [coprod.inr_desc] + rfl + · rw [←ne_eq, OnePoint.ne_infty_iff_exists] at h + obtain ⟨n, hn⟩ := h + symm at hn + use coprod.inl (X := T') (Y := (explicitPullback _ _)) ((i ≫ π ≫ fst _ _ ≫ σ n) t) + simp only [smart_cover, ←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc] + rw [ + ←Category.assoc (fst _ _), ←Category.assoc π, ←Category.assoc i, + ConcreteCategory.comp_apply + ] + rw [hσ''] + · apply Subtype.ext + apply Prod.ext (by rfl) + change t = t' + have hn' : (ConcreteCategory.hom (i ≫ π ≫ snd S ℕ∪{∞})) t' = n := by + rw [←proj_eq, hn] + rw [←hT'] at hn hn' + obtain ⟨s, hs⟩ := hn + obtain ⟨s', hs'⟩ := hn' + rw [←hs, ←hs'] + apply congr_arg + rw [←ConcreteCategory.id_apply s, ←ConcreteCategory.id_apply s'] + erw [←hσ n, σ_i] + simp only [Category.assoc] + erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (σ n), + hs, hs' + ] + erw [←Category.assoc, ConcreteCategory.comp_apply, + ConcreteCategory.comp_apply (i ≫ π), ht] + rfl + · exact (hT' _ _).mpr hn · have : σ ∞ ≫ i = σ' ∞ := rfl let σσ : S ⟶ fibre ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) := @@ -320,7 +501,7 @@ lemma prod_epi (X Y : LightProfinite.{u}) [hempty : Nonempty X] : Epi (snd X Y) rw [LightProfinite.epi_iff_surjective] exact fun y ↦ ⟨⟨Classical.choice hempty, y⟩, rfl⟩ -lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} +private lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} (f : (free R).obj (S).toCondensed ⟶ Y) : ∃ (T : LightProfinite) (π : T ⟶ S) (g : ((free R).obj T.toCondensed) ⟶ X), Epi π ∧ g ≫ p = (lightProfiniteToLightCondSet ⋙ (free R)).map π ≫ f := by @@ -338,12 +519,10 @@ lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfin have comm : g ≫ p = (lightProfiniteToLightCondSet ⋙ (LightCondensed.free R)).map π ≫ f := by symm rw [ - Functor.comp_map, + Functor.comp_map, ←Adjunction.homEquiv_naturality_left_square_iff (freeForgetAdjunction R), - Equiv.apply_symm_apply - ] - apply Sheaf.Hom.ext - rw [ + Equiv.apply_symm_apply, + Sheaf.hom_ext_iff, (coherentTopology LightProfinite).yonedaEquiv_symm_naturality_right, hx, (coherentTopology LightProfinite).map_yonedaEquiv', @@ -351,8 +530,7 @@ lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfin ] rfl - have : Epi π := (LightProfinite.epi_iff_surjective π).mpr hπ - use T, π, g + exact ⟨T, π, g, (LightProfinite.epi_iff_surjective π).mpr hπ, comm⟩ instance : PreservesFiniteCoproducts (lightProfiniteToLightCondSet ⋙ (free R)) := by have : PreservesFiniteCoproducts lightProfiniteToLightCondSet := @@ -401,17 +579,16 @@ noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S parallelPair_obj_one, ← map_comp_assoc, ← Functor.map_comp, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt, BinaryCofan.ι_app_left, BinaryCofan.mk_inl] erw [PullbackCone.IsLimit.lift_fst] - · simp only [comp_obj, CompHausLike.coe_comp, Function.comp_apply, Set.coe_setOf, - Set.mem_setOf_eq, pair_obj_right, const_obj_obj, Functor.comp_map, BinaryCofan.mk_pt, - BinaryCofan.ι_app_right, BinaryCofan.mk_inr, smart_cover, parallelPair_obj_zero, - parallelPair_obj_one, parallelPair_map_left, parallelPair_map_right, const_obj_map, - Category.comp_id] - simp only [Category.assoc, ←Functor.map_comp, ←Functor.comp_map] + · simp only [comp_obj, pair_obj_right, const_obj_obj, Functor.comp_map, + BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr, + smart_cover, parallelPair_obj_zero, parallelPair_obj_one, parallelPair_map_left, + parallelPair_map_right, const_obj_map, Category.comp_id] + simp only [←Functor.comp_map] simp only [←Category.assoc] - simp only [←Functor.map_comp, ←Functor.comp_map] + simp only [←Functor.map_comp] rw [coprod.inr_desc] simp only [Preadditive.comp_add, Preadditive.comp_sub, g_tilde] - simp [←Category.assoc, ←Functor.map_comp, ←Functor.comp_map] + simp [←Category.assoc, ←Functor.map_comp] rw [ explicitPullback.map_fst, explicitPullback.map_snd, Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _)) r_inf, hr, Category.comp_id, @@ -429,7 +606,7 @@ noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S } set_option maxHeartbeats 500000 -theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} +private theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} (f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y) : ∃ (S' : LightProfinite) (ψ : S' ⟶ S) @@ -446,7 +623,8 @@ theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : Lig infer_instance by_cases hS' : Nonempty S' - -- ⨯ + -- The argument below only works if S' is non-empty. If S' is empty, the proof + -- is easier anyway. · let hc : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π')) := hc R π' let ι_inf := fibre_incl ∞ (π' ≫ snd _ _) @@ -473,19 +651,15 @@ theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : Lig = fibre_incl ∞ (π' ≫ snd _ _) ≫ π' ≫ fst _ _ ≫ lift (𝟙 _) - (CompHausLike.ofHom _ (ContinuousMap.const S' (∞ : ℕ∪{∞}))) := by - apply CartesianMonoidalCategory.hom_ext _ _ (by simp) - simp only [Category.assoc] - rw [fibre_condition ∞ (π' ≫ snd _ _)] - ext - simp + (CompHausLike.ofHom _ (ContinuousMap.const S' (∞ : ℕ∪{∞}))) := + CartesianMonoidalCategory.hom_ext _ _ (by simp) (by ext; simp) have : c'.ι.app WalkingParallelPair.one ≫ p = (lightProfiniteToLightCondSet ⋙ (free R)).map (π' ≫ MonoidalCategoryStruct.tensorHom y' (𝟙 ℕ∪{∞})) ≫ f := by simp only [gg, comp_obj, parallelPair_obj_one, c, Functor.comp_map, const_obj_obj, Functor.map_comp, Category.assoc, Preadditive.comp_add, Preadditive.comp_sub, parallelPair.hom_app, - Preadditive.add_comp, Preadditive.sub_comp, ι_inf, c'] + Preadditive.add_comp, Preadditive.sub_comp, c'] rw [comm] simp only [←Functor.map_comp, ←Functor.comp_map, ←Category.assoc, ←comp] simp only [Category.assoc] @@ -504,16 +678,12 @@ theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : Lig ] rfl - let abc : ((free R).obj (S' ⊗ ℕ∪{∞}).toCondensed) ⟶ X := hc.desc c' - refine ⟨abc, inferInstance, ?_⟩ - - dsimp [abc] + let desc_map : ((free R).obj (S' ⊗ ℕ∪{∞}).toCondensed) ⟶ X := hc.desc c' + refine ⟨desc_map, inferInstance, ?_⟩ - have reg_eq : (free R).map ((regular π').ι.app WalkingParallelPair.one) = ((lightProfiniteToLightCondSet ⋙ (free R)).map π') := rfl rw [ ←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map π'), - ←Functor.comp_map, ←Functor.map_comp_assoc, ←reg_eq, - ←Category.assoc _ (hc.desc c') + ←Functor.comp_map, ←Functor.map_comp_assoc ] change _ = (((free R).mapCocone (explicitPullback.explicitRegular π')).ι.app one ≫ hc.desc c') ≫ p erw [hc.fac] @@ -532,11 +702,11 @@ theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : Lig rw [←comp] simp -theorem internallyProjective : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := by +theorem internallyProjective_ℕinfty : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := by rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}] intro X Y p hp S f obtain ⟨S', π, g, hπ, comm⟩ := proj_explicit R p f rw [LightProfinite.epi_iff_surjective] at hπ use S', π, hπ, g, comm -#print axioms internallyProjective +#print axioms internallyProjective_ℕinfty diff --git a/LeanCondensed/Projects/Pullbacks.lean b/LeanCondensed/Projects/Pullbacks.lean index dc5148e..face9bf 100644 --- a/LeanCondensed/Projects/Pullbacks.lean +++ b/LeanCondensed/Projects/Pullbacks.lean @@ -39,6 +39,7 @@ def fibre : LightProfinite := def fibre_incl : fibre y f ⟶ X := CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩ +@[simp] def fibre_condition : fibre_incl y f ≫ f = (CompHausLike.ofHom _ <| ContinuousMap.const (fibre y f) y) := by ext x; exact x.2 diff --git a/LeanCondensed/Projects/Sequence.lean b/LeanCondensed/Projects/Sequence.lean new file mode 100644 index 0000000..9bf1c71 --- /dev/null +++ b/LeanCondensed/Projects/Sequence.lean @@ -0,0 +1,53 @@ +import Mathlib + +open CategoryTheory Limits LightProfinite OnePoint + +namespace LightCondensed + +noncomputable section + +variable (R : Type _) [CommRing R] + +def ι : LightProfinite.of PUnit.{1} ⟶ ℕ∪{∞} := + (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) + +def ι_split : SplitMono ι where + retraction := (TopCat.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩) + id := rfl + +def P_map : + (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed := + (lightProfiniteToLightCondSet ⋙ free R).map ι + +def P : LightCondMod R := cokernel (P_map R) + +def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _ + +def PSequence : ShortComplex (LightCondMod R) := + ShortComplex.mk (P_map R) (P_proj R) (cokernel.condition _) + +lemma PSequence_exact : (PSequence R).ShortExact := by + refine ShortComplex.ShortExact.mk' ?_ + (SplitMono.mono ((ι_split).map (lightProfiniteToLightCondSet ⋙ free R))) + coequalizer.π_epi + rw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, + ←kernel.condition (P_proj R)] + rfl + +def PSequence_split : (PSequence R).Splitting := + ShortComplex.Splitting.ofExactOfRetraction _ + (PSequence_exact R).exact _ + ((ι_split).map (lightProfiniteToLightCondSet ⋙ free R)).id + coequalizer.π_epi + +def P_proj_split : SplitEpi (P_proj R) where + section_ := (PSequence_split R).s + id := (PSequence_split R).s_g + +def P_retract : Retract (P R) ((free R).obj (ℕ∪{∞}).toCondensed) where + i := _ + r := _ + retract := (PSequence_split R).s_g + +def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A) + (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf From 9b95eaccc2c001dc2d3b4f6f53d7268e2520c538 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Tue, 15 Jul 2025 12:32:55 +0200 Subject: [PATCH 11/13] Remove duplicate --- LeanCondensed/Projects/Proj.lean | 158 ------------------------------- 1 file changed, 158 deletions(-) diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index 7a075f7..2b69b21 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -240,164 +240,6 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep erw [hσ] ⟩⟩ -lemma subspaceCover' { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hepi : Epi π] - {σ' : ℕ∪{∞} → (S ⟶ T)} (hσ : ∀ n, σ' n ≫ π ≫ fst _ _ = 𝟙 _) - (hσ' : ∀ n s, (σ' n ≫ π ≫ snd S ℕ∪{∞}) s = ↑n) - : ∃ (T' : LightProfinite) (i : T' ⟶ T), - Epi (i ≫ π) ∧ Epi (smart_cover (i ≫ π)) - ∧ IsSplitEpi - (fibre_incl ∞ ((i ≫ π) ≫ snd _ _) ≫ i ≫ π ≫ fst S ℕ∪{∞}) := by - - let space : Set T := - Set.iUnion (fun (n : ℕ) ↦ Set.range (σ' (OnePoint.some n))) ∪ {t : T | (π ≫ snd _ _) t = ∞} - have : IsClosed space := by - unfold space - rw [Set.union_comm] - exact isClosed_fibres _ _ - (fun n ⟨x, ⟨s, hs⟩⟩ ↦ by simp only [←hs, ←ConcreteCategory.comp_apply, hσ' _ _]) - (fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous)) - - let T' : LightProfinite := ⟨TopCat.of space, inferInstance, inferInstance⟩ - - let i : T' ⟶ T := - CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩ - - have : Mono i := by - rw [CompHausLike.mono_iff_injective] - exact Subtype.val_injective - - let σ : ℕ∪{∞} → (S ⟶ T') := fun n ↦ (CompHausLike.ofHom _ - ⟨ - fun s ↦ ⟨σ' n s, - by - rcases n with (n | n) - · exact Or.inr (hσ' ∞ s) - · apply Or.inl - rw [Set.mem_iUnion] - exact ⟨n, s, rfl⟩ - ⟩, - by continuity - ⟩) - - have hσ'' : ∀ (n : ℕ∪{∞}) (t : T'), t ∈ Set.range (σ n) → (i ≫ π ≫ fst _ _ ≫ σ n) t = t := by - intro n t ht - obtain ⟨s, hs⟩ := ht - rw (config := { occs := .pos [1]}) [←hs] - rw [ - ←ConcreteCategory.comp_apply, - ←Category.assoc π, - ←Category.assoc i, - ←Category.assoc (σ n), - ] - erw [hσ] - rw [Category.id_comp, hs] - - have coe_i : ∀ (t : T'), ↑t = i t := fun _ ↦ rfl - have σ_i : ∀ n, σ' n = σ n ≫ i := fun _ ↦ rfl - - have hT' : ∀ (n : ℕ) t, t ∈ Set.range (σ n) ↔ (i ≫ π ≫ snd _ _) t = n := by - intro n t' - constructor <;> intro h - · obtain ⟨_, ht⟩ := h - rw [←ht, ←ConcreteCategory.comp_apply] - erw [hσ'] - · rcases t'.2 with (fin | inf) - · rw [Set.mem_iUnion] at fin - obtain ⟨j, ⟨s, hs⟩⟩ := fin - suffices h' : j = n by - rw [h'] at hs - use s - exact Subtype.ext hs - rw [coe_i] at hs - rw [ConcreteCategory.comp_apply, ←hs, ←ConcreteCategory.comp_apply, hσ'] at h - rw [←OnePoint.coe_eq_coe] - exact h - · simp only [Set.mem_setOf_eq] at inf - erw [inf] at h - exact (Option.some_ne_none n (Eq.symm h)).elim - - refine ⟨T', i, ?_, ?_, ?_⟩ - · rw [LightProfinite.epi_iff_surjective] - rintro ⟨s, (n | n)⟩ - obtain ⟨t, ht⟩ := (LightProfinite.epi_iff_surjective π).mp hepi ⟨s, none⟩ - have : t ∈ space := by apply Or.inr; rw [Set.mem_setOf_eq, ConcreteCategory.comp_apply, ht]; rfl - use ⟨t, this⟩ - rw [←ht] - rfl - · use σ n s - apply Prod.ext - change ConcreteCategory.hom (σ' n ≫ π ≫ fst _ _) s = s - rw [hσ]; rfl - change ConcreteCategory.hom (σ' n ≫ π ≫ snd _ _) s = (OnePoint.some n) - rw [hσ'] - · rw [LightProfinite.epi_iff_surjective] - intro ⟨⟨t,t'⟩, ht⟩ - simp only [Set.mem_setOf_eq] at ht - have proj_eq : (i ≫ π ≫ snd _ _) t = (i ≫ π ≫ snd _ _) t' := by - rw [←Category.assoc, ConcreteCategory.comp_apply, ht, - ←ConcreteCategory.comp_apply, Category.assoc - ] - by_cases h : (i ≫ π ≫ snd _ _) t = ∞ - · let x : explicitPullback (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) - (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) := - ⟨⟨⟨t, h⟩, ⟨t', by rw [Set.mem_preimage, Category.assoc, Set.mem_singleton_iff, ←proj_eq, h]⟩⟩, - by - simp only [Set.mem_setOf_eq] - rw [ConcreteCategory.comp_apply (fibre_incl _ _), ConcreteCategory.comp_apply (fibre_incl _ _)] - unfold fibre_incl - simp only [CompHausLike.hom_ofHom, ContinuousMap.coe_mk] - exact ht - ⟩ - let p := coprod.inr (X := T') (Y := (explicitPullback _ _)) x - use coprod.inr (X := T') (Y := (explicitPullback _ _)) x - rw [smart_cover, ←ConcreteCategory.comp_apply] - simp only [coprod.inr_desc] - rfl - · rw [←ne_eq, OnePoint.ne_infty_iff_exists] at h - obtain ⟨n, hn⟩ := h - symm at hn - use coprod.inl (X := T') (Y := (explicitPullback _ _)) ((i ≫ π ≫ fst _ _ ≫ σ n) t) - simp only [smart_cover, ←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc] - rw [ - ←Category.assoc (fst _ _), ←Category.assoc π, ←Category.assoc i, - ConcreteCategory.comp_apply - ] - rw [hσ''] - · apply Subtype.ext - apply Prod.ext (by rfl) - change t = t' - have hn' : (ConcreteCategory.hom (i ≫ π ≫ snd S ℕ∪{∞})) t' = n := by - rw [←proj_eq, hn] - rw [←hT'] at hn hn' - obtain ⟨s, hs⟩ := hn - obtain ⟨s', hs'⟩ := hn' - rw [←hs, ←hs'] - apply congr_arg - rw [←ConcreteCategory.id_apply s, ←ConcreteCategory.id_apply s'] - erw [←hσ n, σ_i] - simp only [Category.assoc] - erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (σ n), - hs, hs' - ] - erw [←Category.assoc, ConcreteCategory.comp_apply, - ConcreteCategory.comp_apply (i ≫ π), ht] - rfl - · exact (hT' _ _).mpr hn - · have : σ ∞ ≫ i = σ' ∞ := rfl - - let σσ : S ⟶ fibre ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) := - fibreLift ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞) - - exact ⟨⟨ - σσ, - by - simp only [←Category.assoc] - rw [ - fibreLift_comp ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞), - ] - erw [hσ] - ⟩⟩ - lemma xyz { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : ∃ (S' T' : LightProfinite) (y' : S' ⟶ S) (π' : T' ⟶ S' ⊗ ℕ∪{∞}) (g' : T' ⟶ T), Epi π' From e8159c4a3187d44dc4e2aa5233da097dace916f0 Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Sat, 16 Aug 2025 15:58:03 +0200 Subject: [PATCH 12/13] Small tweaks --- LeanCondensed/Projects/Epi.lean | 3 +- LeanCondensed/Projects/PreservesCoprod.lean | 2 +- LeanCondensed/Projects/Proj.lean | 11 ++--- LeanCondensed/Projects/Pullbacks.lean | 48 ++++----------------- 4 files changed, 14 insertions(+), 50 deletions(-) diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index cbb43d5..f6624ae 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -74,8 +74,7 @@ instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := { lemma stupid {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y := by - rw [Subtype.ext_iff] at h - exact h + rwa [Subtype.ext_iff] at h noncomputable def πpair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet := parallelPair diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean index c5f82c4..f1a85ba 100644 --- a/LeanCondensed/Projects/PreservesCoprod.lean +++ b/LeanCondensed/Projects/PreservesCoprod.lean @@ -15,7 +15,7 @@ instance {n : ℕ} (S : Fin n → LightProfinite.{u}) : have : HasColimitsOfSize.{u} (LightCondSet.{u}) := inferInstanceAs (HasColimitsOfSize.{u} (Sheaf _ _)) apply (config := { allowSynthFailures := true}) PreservesCoproduct.of_iso_comparison - rw [isIso_iff_isIso_coyoneda_map] -- or maybe `rw [isIso_iff_coyoneda_map_bijective]` + rw [isIso_iff_isIso_coyoneda_map] intro X rw [isIso_iff_bijective] have := instIsIsoPiComparison X.val (fun i ↦ ⟨S i⟩) diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index 2b69b21..d42e8e1 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -240,7 +240,7 @@ lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hep erw [hσ] ⟩⟩ -lemma xyz { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] +lemma refinedCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : ∃ (S' T' : LightProfinite) (y' : S' ⟶ S) (π' : T' ⟶ S' ⊗ ℕ∪{∞}) (g' : T' ⟶ T), Epi π' ∧ Epi y' @@ -383,10 +383,7 @@ instance : PreservesFiniteCoproducts (lightProfiniteToLightCondSet ⋙ (free R)) noncomputable def hc {S T : LightProfinite} (π : T ⟶ S) [Epi π] : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π)) := by have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩ - exact isColimitOfPreserves _ (explicitPullback.explicitRegularIsColimit π) - -lemma eq_sub_self {G : Type} [AddGroup G] {a b : G} : a = a - b ↔ b = 0 := by - rw [←sub_eq_self (a := a), eq_comm] + exact isColimitOfPreserves _ (explicitPullback.explicitRegularIsColimit _) noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S ⊗ ℕ∪{∞})) [Epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smart_cover π)] @@ -447,7 +444,7 @@ noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S rfl } -set_option maxHeartbeats 500000 +-- set_option maxHeartbeats 500000 private theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite} (f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y) : ∃ (S' : LightProfinite) @@ -456,7 +453,7 @@ private theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] ∧ ((free R).map (lightProfiniteToLightCondSet.map (MonoidalCategoryStruct.tensorHom ψ (𝟙 ℕ∪{∞}))) ≫ f = g ≫ p) := by obtain ⟨T, π, g, hπ, comm⟩ := comm_sq R p f - obtain ⟨S', T', y', π', g', hπ', hy', comp, ⟨⟨split⟩⟩, epi⟩ := xyz π + obtain ⟨S', T', y', π', g', hπ', hy', comp, ⟨⟨split⟩⟩, epi⟩ := refinedCover π use S', y' diff --git a/LeanCondensed/Projects/Pullbacks.lean b/LeanCondensed/Projects/Pullbacks.lean index face9bf..8c1a7c5 100644 --- a/LeanCondensed/Projects/Pullbacks.lean +++ b/LeanCondensed/Projects/Pullbacks.lean @@ -69,8 +69,7 @@ def fibreCone : PullbackCone (CompHausLike.ofHom _ <| ContinuousMap.const point ContinuousMap.const_apply, ContinuousMap.coe_mk]; rw [x.2]) def fibreConeIsLimit : IsLimit (fibreCone y f) := by - refine PullbackCone.IsLimit.mk ?_ ?_ ?_ ?_ ?_ - · exact (fibreCone _ _).condition + refine PullbackCone.IsLimit.mk (fibreCone _ _).condition ?_ ?_ ?_ ?_ · intro cone have : ∀ z : cone.pt, f (cone.snd z) = y := by intro z @@ -86,7 +85,7 @@ def fibreConeIsLimit : IsLimit (fibreCone y f) := by repeat {exact fun cone ↦ rfl} · intro cone m hm hm' have := fibre_incl_mono y f - rw [←cancel_mono (fibre_incl y f), hm'] + erw [←cancel_mono (fibre_incl y f), hm'] rfl def fibreLift {Z : LightProfinite} (g : Z ⟶ X) (hg : ∀ z, f (g z) = y) : Z ⟶ fibre y f := @@ -116,9 +115,8 @@ instance : IsClosed {⟨x,y⟩ : X × Y | f x = g y} := by g.1.continuous.isOpen_preimage _ hv, ha, hb, ?_ ⟩ - intro ⟨x, y⟩ ⟨hx, hy⟩ + intro ⟨x, y⟩ ⟨hx, hy⟩ hxy simp only [Set.mem_preimage] at hx hy - intro hxy rw [hxy] at hx exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩ @@ -143,36 +141,16 @@ namespace explicitPullback variable {X Y Z : LightProfinite} {f : X ⟶ Z} {g : Y ⟶ Z} def fst (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ X := - CompHausLike.ofHom _ + TopCat.ofHom ⟨ (Prod.fst : X × Y → X) ∘ (Subtype.val : _ → X × Y), Continuous.comp continuous_fst continuous_subtype_val ⟩ def snd (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ Y := - let space := {⟨x,y⟩ : X × Y | f x = g y} - have : IsClosed space := by - apply IsClosed.mk - rw [isOpen_prod_iff] - intro a b hab - obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab - refine ⟨ - f⁻¹'u, g⁻¹'v, - f.1.continuous.isOpen_preimage _ hu, - g.1.continuous.isOpen_preimage _ hv, - ha, hb, ?_ - ⟩ - intro ⟨x, y⟩ ⟨hx, hy⟩ - simp only [Set.mem_preimage] at hx hy - intro hxy - rw [hxy] at hx - exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩ - have : IsCompact space := this.isCompact - have : CompactSpace space := by - exact isCompact_iff_compactSpace.mp this - CompHausLike.ofHom _ + TopCat.ofHom ⟨ - Prod.snd ∘ Subtype.val, + (Prod.snd : X × Y → Y) ∘ (Subtype.val : _ → X × Y), Continuous.comp continuous_snd continuous_subtype_val ⟩ @@ -222,19 +200,9 @@ def IsLimit : IsLimit (Cone f g) := by simp only [Set.mem_setOf_eq, space] rw [←ConcreteCategory.comp_apply, cone.condition] rfl - refine CompHausLike.ofHom _ ⟨fun z ↦ ⟨⟨cone.fst z, cone.snd z⟩, this z⟩, ?_⟩ - + refine TopCat.ofHom ⟨fun z ↦ ⟨⟨cone.fst z, cone.snd z⟩, this z⟩, ?_⟩ rw [(IsInducing.continuous_iff IsEmbedding.subtypeVal.1)] - have : Continuous (fun z ↦ (⟨cone.fst z, cone.snd z⟩ : X × Y)) - = Continuous - (Subtype.val ∘ fun z ↦ ⟨ - ((ConcreteCategory.hom cone.fst) z, - (ConcreteCategory.hom cone.snd) z), - this z - ⟩) := by - exact congr_arg (f := Continuous) (rfl) - rw [←this] - refine Continuous.prodMk cone.fst.1.continuous cone.snd.1.continuous + exact Continuous.prodMk cone.fst.1.continuous cone.snd.1.continuous repeat {intro cone; ext z; rfl} · intro cone m hm hm' ext z From 62d2ca76a0b87af9314be07c651c9601357afd7f Mon Sep 17 00:00:00 2001 From: Jonas van der Schaaf Date: Fri, 22 Aug 2025 10:54:54 +0200 Subject: [PATCH 13/13] Revert lake manifest --- lake-manifest.json | 211 ++++++++++++++++++++------------------------- 1 file changed, 95 insertions(+), 116 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 86dbc7b..ab3c7be 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,116 +1,95 @@ -{ - "version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c30c25bf81ec9a1983c7381a45be6287c13953ed", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.67", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "867d9dc77534341321179c9aa40fceda675c50d4", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - } - ], - "name": "LeanCondensed", - "lakeDir": ".lake" -} \ No newline at end of file +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "287febc23a1ff0df9c02d934fb82934e8bc90a85", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "304c5e2f490d546134c06bf8919e13b175272084", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.59", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "LeanCondensed", + "lakeDir": ".lake"}