From d4919fa2b77cf6bfe882d3e2b082eceaffb28750 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Wed, 28 Jan 2026 10:10:49 -0700 Subject: [PATCH] bump mathlib --- LeanCondensed.lean | 2 - .../Category/CompHausLike/Limits.lean | 29 -- LeanCondensed/Projects/Epi.lean | 7 +- LeanCondensed/Projects/FreeCondensed.lean | 4 +- .../Projects/LightProfiniteInjective.lean | 380 ------------------ LeanCondensed/Projects/LightSolid.lean | 67 ++- LeanCondensed/Projects/Proj.lean | 12 +- LeanCondensed/Projects/Sequence.lean | 11 +- lake-manifest.json | 22 +- lean-toolchain | 2 +- 10 files changed, 68 insertions(+), 468 deletions(-) delete mode 100644 LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean delete mode 100644 LeanCondensed/Projects/LightProfiniteInjective.lean diff --git a/LeanCondensed.lean b/LeanCondensed.lean index 5633bf4..a7e1cec 100644 --- a/LeanCondensed.lean +++ b/LeanCondensed.lean @@ -4,11 +4,9 @@ import LeanCondensed.Mathlib.CategoryTheory.Sites.DirectImage import LeanCondensed.Mathlib.Condensed.Adjunctions import LeanCondensed.Mathlib.Condensed.Light.Limits import LeanCondensed.Mathlib.Condensed.Light.Monoidal -import LeanCondensed.Mathlib.Topology.Category.CompHausLike.Limits import LeanCondensed.Projects.Epi import LeanCondensed.Projects.FreeCondensed import LeanCondensed.Projects.IsLocalizedMonoidal -import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.LightSolid import LeanCondensed.Projects.MonoidalLinear import LeanCondensed.Projects.PreservesCoprod diff --git a/LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean b/LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean deleted file mode 100644 index 6aa6546..0000000 --- a/LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts -import Mathlib.Topology.Category.LightProfinite.Limits - -open CategoryTheory Topology Limits - -namespace CompHausLike - -universe u - -section BinaryCoproducts - -variable {P : TopCat.{u} → Prop} (X Y : CompHausLike P) - -section Coproduct - -variable [HasProp P (X ⊕ Y)] - -def coproductCocone : BinaryCofan X Y := BinaryCofan.mk (P := CompHausLike.of P (X ⊕ Y)) - (TopCat.ofHom { toFun := Sum.inl }) (TopCat.ofHom { toFun := Sum.inr }) - -def coproductIsColimit : IsColimit (coproductCocone X Y) := by - refine BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr }) - (by cat_disch) (by cat_disch) fun _ _ h₁ h₂ ↦ ?_ - ext ⟨⟩ - exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _] - -end Coproduct - -end BinaryCoproducts diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean index 3d8826a..e764d99 100644 --- a/LeanCondensed/Projects/Epi.lean +++ b/LeanCondensed/Projects/Epi.lean @@ -8,7 +8,12 @@ import Mathlib.Combinatorics.Quiver.ReflQuiver import Mathlib.Condensed.Light.Epi import Mathlib.Condensed.Light.Explicit import Mathlib.Condensed.Light.Functors -import Mathlib.Topology.Compactness.PseudometrizableLindelof +import Mathlib.Data.Finset.Attr +import Mathlib.Tactic.Common +import Mathlib.Tactic.Continuity +import Mathlib.Tactic.Finiteness.Attr +import Mathlib.Tactic.SetLike +import Mathlib.Util.CompileInductive import Mathlib.Topology.Connected.Separation import Mathlib.Topology.Spectral.Prespectral diff --git a/LeanCondensed/Projects/FreeCondensed.lean b/LeanCondensed/Projects/FreeCondensed.lean index 1cbd3e5..1cc44f3 100644 --- a/LeanCondensed/Projects/FreeCondensed.lean +++ b/LeanCondensed/Projects/FreeCondensed.lean @@ -30,7 +30,9 @@ def profiniteComponent (S : LightProfinite.{0}) (c : ℤ) : LightProfinite := def _root_.lightProfiniteToSequential : LightProfinite ⥤ Sequential where obj X := Sequential.of X - map f := f + map f := ConcreteCategory.ofHom ⟨f, by continuity⟩ + map_id := sorry + map_comp := sorry -- This functor should probably be defined as a right Kan extension of the analogous functor to -- `FintypeCat`, similarly to `Condensed.profiniteSolid`, defined in `Mathlib.Condensed.Solid`. diff --git a/LeanCondensed/Projects/LightProfiniteInjective.lean b/LeanCondensed/Projects/LightProfiniteInjective.lean deleted file mode 100644 index 10e109d..0000000 --- a/LeanCondensed/Projects/LightProfiniteInjective.lean +++ /dev/null @@ -1,380 +0,0 @@ -/- -Copyright (c) 2024 Lenny Taelman. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lenny Taelman --/ - -import Mathlib.CategoryTheory.Preadditive.Injective.Basic -import Mathlib.Topology.Category.LightProfinite.AsLimit -import Mathlib.Topology.Category.CompHausLike.Limits -import Mathlib.CategoryTheory.Functor.OfSequence -import Mathlib.CategoryTheory.EpiMono - -/-! - -# Injectivity of light profinite spaces - -This file establishes the non-empty light profinite spaces are injective in the -category of light profinite spaces. This is used in the proof the the null sequence -module is projective in light condensed abelian groups. - -The code below also prepares for proving that non-empty light -profinite spaces are injective in the category of all profinite spaces. - -## Implementation notes - -The main result is `injective_of_light`, which provides an instance of `Injective S` for -a non-empty light profinite space `S`. The proof uses an inductive extension argument -along a presentation of S as sequential limit of finite spaces. The key lemma is -`light_key_extension_lemma`. - -## References - -* -* - --/ -noncomputable section -universe u - -open Set Profinite Topology CategoryTheory LightProfinite Fin Limits - -namespace Profinite - -/-- In a totally disconnected compact Hausdorff space `X`, if `Z ⊆ U` are subsets with `Z` closed -and `U` open, there exists a clopen `C` with `Z ⊆ C ⊆ U`. -/ -lemma exists_clopen_of_closed_subset_open {X : Type u} - [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] - {Z U : Set X} (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : - ∃ C : Set X, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U := by - -- every `z ∈ Z` has clopen neighborhood `V z ⊆ U` - choose V hV using fun (z : Z) ↦ compact_exists_isClopen_in_isOpen hU (hZU z.property) - -- the `V z` cover `Z` - have V_cover : Z ⊆ iUnion V := fun z hz ↦ mem_iUnion.mpr ⟨⟨z, hz⟩, (hV ⟨z, hz⟩).2.1⟩ - -- choose a finite subcover - choose I hI using hZ.isCompact.elim_finite_subcover V (fun z ↦ (hV z).1.isOpen) V_cover - -- the union of this finite subcover does the job - exact ⟨⋃ (i ∈ I), V i, I.finite_toSet.isClopen_biUnion (fun i _ ↦ (hV i).1), hI, by simp_all⟩ - - -/- - Let X be profinite, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. - Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i - with the C i disjoint, and such that ∪ C i = ∪ D i --/ - -lemma clopen_partition_of_disjoint_closeds_in_clopens - {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] - {I : Type*} [Finite I] {Z D : I → Set X} - (Z_closed : ∀ i, IsClosed (Z i)) (D_clopen : ∀ i, IsClopen (D i)) - (Z_subset_D : ∀ i, Z i ⊆ D i) (Z_disj : univ.PairwiseDisjoint Z) : - ∃ C : I → Set X, (∀ i, IsClopen (C i)) ∧ (∀ i, Z i ⊆ C i) ∧ (∀ i, C i ⊆ D i) ∧ - (⋃ i, D i) ⊆ (⋃ i, C i) ∧ (univ.PairwiseDisjoint C) := by - induction I using Finite.induction_empty_option with - | of_equiv e IH => - obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e) - (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i)) - (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image]) - refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i), - fun i ↦ by simpa using h3 (e.symm i), ?_, - by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩ - simp only [Function.comp_apply, iUnion_subset_iff] at h4 ⊢ - intro i - simpa [e.symm.surjective.iUnion_comp C] using h4 (e.symm i) - | h_empty => exact ⟨fun _ ↦ univ, by simp, by simp, by simp, by simp, fun i ↦ PEmpty.elim i⟩ - | @h_option I _ IH => - -- let Z' be the restriction of Z along succ : Fin n → Fin (n+1) - let Z' : I → Set X := fun i ↦ Z (some i) - have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i) - have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by - rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image] - exact PairwiseDisjoint.subset Z_disj (by simp) - -- find Z 0 ⊆ V ⊆ D 0 \ ⋃ Z' using clopen_sandwich - let U : Set X := D none \ iUnion (Z ∘ some) - have U_open : IsOpen U := IsOpen.sdiff (D_clopen none).2 - (isClosed_iUnion_of_finite (fun i ↦ Z_closed (some i))) - have Z0_subset_U : Z none ⊆ U := by - rw [subset_diff] - simpa using ⟨Z_subset_D none, fun i ↦ (by apply Z_disj; all_goals simp)⟩ - obtain ⟨V, V_clopen, Z0_subset_V, V_subset_U⟩ := - exists_clopen_of_closed_subset_open (Z_closed none) U_open Z0_subset_U - have V_subset_D0 : V ⊆ D none := subset_trans V_subset_U diff_subset - -- choose Z' i ⊆ C' i ⊆ D' i = D i.succ \ V using induction hypothesis - let D' : I → Set X := fun i ↦ D (some i) \ V - have D'_clopen (i : I): IsClopen (D' i) := IsClopen.diff (D_clopen (some i)) V_clopen - have Z'_subset_D' (i : I) : Z' i ⊆ D' i := by - rw [subset_diff] - refine ⟨by grind, Disjoint.mono_right V_subset_U ?_⟩ - exact Disjoint.mono_left (subset_iUnion_of_subset i fun _ h ↦ h) disjoint_sdiff_right - obtain ⟨C', C'_clopen, Z'_subset_C', C'_subset_D', C'_cover_D', C'_disj⟩ := - IH Z'_closed D'_clopen Z'_subset_D' Z'_disj - have C'_subset_D (i : I): C' i ⊆ D (some i) := subset_trans (C'_subset_D' i) diff_subset - -- now choose C0 = D 0 \ ⋃ C' i - let C0 : Set X := D none \ iUnion (fun i ↦ C' i) - have C0_subset_D0 : C0 ⊆ D none := diff_subset - have C0_clopen : IsClopen C0 := IsClopen.diff (D_clopen none) - (isClopen_iUnion_of_finite C'_clopen) - have Z0_subset_C0 : Z none ⊆ C0 := by - unfold C0 - apply subset_diff.mpr - constructor - · exact Z_subset_D none - · apply Disjoint.mono_left Z0_subset_V - exact disjoint_iUnion_right.mpr fun i ↦ Disjoint.mono_right (C'_subset_D' i) - disjoint_sdiff_right - -- patch together to define C := cases C0 C', and verify the needed properties - let C : Option I → Set X := fun i ↦ Option.casesOn i C0 C' - have C_clopen : ∀ i, IsClopen (C i) := fun i ↦ Option.casesOn i C0_clopen C'_clopen - have Z_subset_C : ∀ i, Z i ⊆ C i := fun i ↦ Option.casesOn i Z0_subset_C0 Z'_subset_C' - have C_subset_D : ∀ i, C i ⊆ D i := fun i ↦ Option.casesOn i C0_subset_D0 C'_subset_D - have C_cover_D : (⋃ i, D i) ⊆ (⋃ i, C i) := by - intro x hx - rw [mem_iUnion] at hx ⊢ - by_cases hx0 : x ∈ C0; { exact ⟨none, hx0⟩ } - by_cases hxD : x ∈ D none - · have hxC' : x ∈ ⋃ i, C' i := by grind - obtain ⟨i, hi⟩ := mem_iUnion.mp hxC' - exact ⟨some i, hi⟩ - · obtain ⟨none | j, hi⟩ := hx; {grind} - have hxD' : x ∈ ⋃ i, D' i := mem_iUnion.mpr ⟨j, by grind⟩ - obtain ⟨k, hk⟩ := mem_iUnion.mp <| C'_cover_D' hxD' - exact ⟨some k, hk⟩ - have C_disj : univ.PairwiseDisjoint C := by - rw [Set.pairwiseDisjoint_iff] - rintro (none | i) _ (none | j) _ - · simp - · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using - Disjoint.mono_right (subset_iUnion (fun i ↦ C' i) j) disjoint_sdiff_left - · simpa [C, C0, Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty] using - Disjoint.mono_left (subset_iUnion (fun j ↦ C' j) i) disjoint_sdiff_right - · simpa using (Set.pairwiseDisjoint_iff.mp C'_disj) - (i := i) (by trivial) (j := j) (by trivial) - exact ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ - - -/- - This is the key statement for the inductive proof of injectivity of light - profinite spaces. Given a commutative square - X >-f-> Y - |g |g' - v v - S -f'->> T - where Y is profinite, S is finite, f is injective and f' is surjective, - there exists a diagonal map k : Y → S making the diagram commute. - - It is mathematically equivalent to the previous lemma: - take Z s to be the fiber of g at s, and D s the fiber of g' at f' s --/ - -lemma key_extension_lemma (X Y S T : Type u) - [TopologicalSpace X] [CompactSpace X] - [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] - [TopologicalSpace S] [T2Space S] [Finite S] - [TopologicalSpace T] [T2Space T] - (f : X → Y) (hf : Continuous f) (f_inj : Function.Injective f) - (f' : S → T) (f'_surj : Function.Surjective f') - (g : X → S) (hg : Continuous g) (g' : Y → T) (hg' : Continuous g') - (h_comm : g' ∘ f = f' ∘ g) : - ∃ k : Y → S, (Continuous k) ∧ (f' ∘ k = g') ∧ (k ∘ f = g) := by - -- help the instance inference a bit: T is finite - have : Finite T := Finite.of_surjective f' f'_surj - -- pick bijection between Fin n and S - -- obtain ⟨n, φ, ψ, h1, h2⟩ := Finite.exists_equiv_fin S - -- define Z i to be the image of the fiber of g at i - let Z : S → Set Y := fun i ↦ f '' (g⁻¹' {i}) - have Z_closed (i) : IsClosed (Z i) := - (IsClosedEmbedding.isClosed_iff_image_isClosed (Continuous.isClosedEmbedding hf f_inj)).mp - (IsClosed.preimage hg isClosed_singleton) - have Z_disj : univ.PairwiseDisjoint Z := by - rw [Set.pairwiseDisjoint_iff] - simp only [image_inter_nonempty_iff, Z] - rintro _ _ _ _ ⟨_, rfl, ⟨_, rfl, hy⟩⟩ - rw [f_inj hy] - -- define D i to be the fiber of g' at f' i - let D : S → Set Y := fun i ↦ g' ⁻¹' ( {f' i}) - have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg' - have Z_subset_D i : Z i ⊆ D i := by - intro z hz - rw [mem_preimage, mem_singleton_iff] - obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz - have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm x - simp_all - have D_cover_univ : univ ⊆ (⋃ i, D i) := by - intro y _ - simp only [mem_iUnion] - obtain ⟨s, hs⟩ := f'_surj (g' y) - use s - rw [mem_preimage] - exact hs.symm - -- obtain clopens Z i ⊆ C i ⊆ D i with C i disjoint, covering Y - obtain ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ := - clopen_partition_of_disjoint_closeds_in_clopens Z_closed D_clopen Z_subset_D Z_disj - have C_cover_univ : ⋃ i, C i = univ := univ_subset_iff.mp - (subset_trans D_cover_univ C_cover_D) - -- define k to be the unique map sending C i to ψ i - have h_glue (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : i = j := by - rw [Set.pairwiseDisjoint_iff] at C_disj - exact C_disj (by simp) (by simp) ⟨x, by grind⟩ - refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩ - · rw [IsLocallyConstant.iff_isOpen_fiber] - intro s - convert (C_clopen s).2 - ext y - simp [preimage_liftCover] - · ext y - -- y is contained in C i for some i - have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ] - obtain ⟨i, hi⟩ := mem_iUnion.mp hy - simpa [liftCover_of_mem hi] using symm (C_subset_D i hi) - · ext x - simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)] - - --- categorically stated versions of key_extension_lemma - -lemma profinite_key_extension_lemma (X Y S T : Profinite.{u}) [Finite S] - (f : X ⟶ Y) [Mono f] (f' : S ⟶ T) [Epi f'] - (g : X ⟶ S) (g' : Y ⟶ T) (h_comm : f ≫ g' = g ≫ f') : - ∃ k : Y ⟶ S, (k ≫ f' = g') ∧ (f ≫ k = g) := by - obtain ⟨k_fun, k_cont, h2, h3⟩ := key_extension_lemma X Y S T - f f.hom.continuous ((CompHausLike.mono_iff_injective f).mp inferInstance) - f' ((epi_iff_surjective f').mp inferInstance) - g g.hom.continuous g' g'.hom.continuous (by simp [← CompHausLike.coe_comp, h_comm]) - exact ⟨TopCat.ofHom ⟨k_fun, k_cont⟩, ConcreteCategory.hom_ext_iff.mpr (congrFun h2), - ConcreteCategory.hom_ext_iff.mpr (congrFun h3)⟩ - -end Profinite - -namespace LightProfinite - -lemma light_key_extension_lemma (X Y S T : LightProfinite.{u}) [hS : Finite S] - (f : X ⟶ Y) [Mono f] (f' : S ⟶ T) [Epi f'] - (g : X ⟶ S) (g' : Y ⟶ T) (h_comm : f ≫ g' = g ≫ f') : - ∃ k : Y ⟶ S, (k ≫ f' = g') ∧ (f ≫ k = g) := by - obtain ⟨k_fun, k_cont, h2, h3⟩ := key_extension_lemma X Y S T - f f.hom.continuous ((CompHausLike.mono_iff_injective f).mp inferInstance) - f' ((epi_iff_surjective f').mp inferInstance) - g g.hom.continuous g' g'.hom.continuous (by simp [← CompHausLike.coe_comp, h_comm]) - exact ⟨TopCat.ofHom ⟨k_fun, k_cont⟩, ConcreteCategory.hom_ext_iff.mpr (congrFun h2), - ConcreteCategory.hom_ext_iff.mpr (congrFun h3)⟩ - -end LightProfinite - -namespace CompHausLike - -/- - The map from a nonempty space to pt is (split) epi in a CompHausLike category of spaces --/ - -instance {P : TopCat.{u} → Prop} [HasProp P PUnit.{u + 1}] - (X : CompHausLike.{u} P) [Nonempty X] : - IsSplitEpi (isTerminalPUnit.from X) := IsSplitEpi.mk' - { section_ := const _ (Nonempty.some inferInstance), id := isTerminalPUnit.hom_ext _ _ } - -end CompHausLike - -/- - Next we show that nonempty (light) profinite spaces are injective. --/ - -instance LightProfinite.injective_of_finite (S : LightProfinite.{u}) [Nonempty S] [Finite S] : - Injective (S) where - factors {X Y} g f _ := by - let f' := CompHausLike.isTerminalPUnit.from S - let g' := CompHausLike.isTerminalPUnit.from Y - obtain ⟨k, _, h2⟩ := light_key_extension_lemma _ _ S _ f f' g g' - (CompHausLike.isTerminalPUnit.hom_ext _ _) - exact ⟨k, h2⟩ - -instance Profinite.injective_of_finite (S : Profinite.{u}) [Nonempty S] [Finite S] : - Injective (S) where - factors {X Y} g f _ := by - let f' := CompHausLike.isTerminalPUnit.from S - let g' := CompHausLike.isTerminalPUnit.from Y - obtain ⟨k, _, h2⟩ := profinite_key_extension_lemma _ _ S _ f f' g g' - (CompHausLike.isTerminalPUnit.hom_ext _ _) - exact ⟨k, h2⟩ - - -namespace LightProfinite - -/- - Main theorem: a nonempty light profinite space is injective in LightProfinite - TODO: a nonempty light profinite space is injective in Profinite --/ - -/- - Induction step in the proof: - - X --f--> Y - |g' (n+1) |k n - v v - S. (n+1) --p n-> S. n - - find k n+1 : Y ⟶ S' (n+1) making both diagrams commute. That is: - - h_up n+1 : k (n+1) ≫ p n = k n **** recursive, requires k n - - h_down n+1 : f ≫ k (n+1) = g' (n+1) - Construction of k (n+1) through extension lemma requires as input: - - h_comm n : g' (n+1) ≫ p n = f ≫ k n, which can be obtained from h_down n - --/ - -instance injective_of_light (S : LightProfinite.{u}) [Nonempty S] : Injective S where - factors {X Y} g f h := by - -- help the instance inference a bit - haveI (n : ℕ) : Finite (S.component n) := - inferInstanceAs (Finite (FintypeCat.toLightProfinite.obj _)) - haveI : Nonempty (S.component 0) := Nonempty.map (S.proj 0) inferInstance - haveI (n : ℕ) : Epi (S.transitionMap n) := (LightProfinite.epi_iff_surjective _).mpr - (S.surjective_transitionMap n) - -- base step of the induction: find k0 : Y ⟶ S.component 0 - obtain ⟨k0, h_down0⟩ := Injective.factors (g ≫ S.proj 0) f - have h_comm0 : f ≫ k0 = g ≫ S.proj 1 ≫ S.transitionMap 0 := by - rw [h_down0] - exact congrArg _ (S.proj_comp_transitionMap 0).symm - -- key part of induction step: next produces k n+1 out of k n, see diagram above - have h_step (n : ℕ) (k : Y ⟶ S.component n) (h_down : f ≫ k = g ≫ S.proj n) : - ∃ k' : Y ⟶ S.component (n+1), k' ≫ S.transitionMap n = k ∧ f ≫ k' = g ≫ S.proj (n+1) := by - have h_comm : f ≫ k = g ≫ S.proj (n+1) ≫ S.transitionMap n := by - rw [h_down] - exact congrArg _ (S.proj_comp_transitionMap n).symm - exact light_key_extension_lemma _ _ _ _ f (S.transitionMap n) (g ≫ (S.proj (n+1))) k h_comm - let lifts (n : ℕ) := { k : Y ⟶ S.component n // f ≫ k = g ≫ S.proj n } - let next (n : ℕ) : lifts n → lifts (n+1) := - fun k ↦ ⟨Classical.choose (h_step n k.val k.property), - (Classical.choose_spec (h_step n k.val k.property)).2⟩ - -- now define sequence of lifts using induction - let k_seq (n : Nat) : lifts n := Nat.rec ⟨k0, h_down0⟩ next n - -- h_up and h_down are the required commutativity properties - have h_down (n : ℕ) : f ≫ (k_seq n).val = g ≫ S.proj n := (k_seq n).property - have h_up (n : ℕ) : (k_seq (n+1)).val ≫ S.transitionMap n = (k_seq n).val := by - induction n with - | zero => exact (Classical.choose_spec (h_step 0 k0 h_down0)).1 - | succ n ih => - exact (Classical.choose_spec (h_step (n+1) (k_seq (n+1)).val (k_seq (n+1)).property)).1 - let k_cone : Cone S.diagram := - { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ (k_seq n).val) (fun n ↦ (h_up n).symm) } - -- now the induced map Y ⟶ S = lim S.component is the desired map - use S.asLimit.lift k_cone - let g_cone : Cone S.diagram := - { pt := X, π := NatTrans.ofOpSequence (fun n ↦ g ≫ S.proj n) (fun n ↦ by - simpa using congrArg _ (S.proj_comp_transitionMap n).symm) } - have hg : g = S.asLimit.lift g_cone := by - apply S.asLimit.uniq g_cone - intro n - rw [NatTrans.ofOpSequence_app] - rw [hg] - have hlim : S.asLimit.lift (k_cone.extend f) = S.asLimit.lift g_cone := by - dsimp [Cone.extend] - congr - ext n - simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down] - rw [← hlim] - apply S.asLimit.uniq (k_cone.extend f) - intro n - simp - -instance injective_in_profinite_of_light (S : LightProfinite.{u}) [Nonempty S] : - Injective (lightToProfinite.obj S) := sorry - -end LightProfinite diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean index 3c16c9a..4557d73 100644 --- a/LeanCondensed/Projects/LightSolid.lean +++ b/LeanCondensed/Projects/LightSolid.lean @@ -46,7 +46,7 @@ end MonoidalClosed namespace LightProfinite -def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := TopCat.ofHom { +def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := ConcreteCategory.ofHom { toFun | ∞ => ∞ | OnePoint.some n => (n + 1 : ℕ) @@ -89,7 +89,7 @@ variable {R : Type} [CommRing R] /-- A light condensed abelian group `A` is *solid* if the shift map `ℕ∪∞ → ℕ∪∞` induces an isomorphism on internal homs into `A` -/ class IsSolid (A : LightCondAb) : Prop where - oneMinusShift_induces_iso : IsIso ((pre (oneMinusShift ℤ)).app A) + oneMinusShift_induces_iso : IsIso ((MonoidalClosed.pre (oneMinusShift ℤ)).app A) structure Solid where toLightCondAb : LightCondAb @@ -99,8 +99,7 @@ namespace Solid def of (A : LightCondAb) [IsSolid A] : Solid := ⟨A⟩ -instance category : Category Solid := - InducedCategory.category toLightCondAb +instance category : Category Solid := InducedCategory.instCategory (F := toLightCondAb) instance : IsSolid ((discrete (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) := sorry @@ -118,7 +117,7 @@ instance : PreservesLimitsOfSize.{0, 0} solidToCondensed := sorry instance : PreservesColimitsOfSize.{0, 0} solidToCondensed := sorry instance : LocallySmall.{0} Solid where - hom_small X Y := inferInstanceAs (Small (X.1 ⟶ Y.1)) + hom_small X Y := sorry--inferInstanceAs (Small (X.1 ⟶ Y.1)) section @@ -126,40 +125,40 @@ variable {C : Type u} [SmallCategory C] (J : GrothendieckTopology C) end -def solidToCondensed' : ShrinkHoms Solid ⥤ ShrinkHoms LightCondAb := - inducedFunctor _ +-- def solidToCondensed' : ShrinkHoms Solid ⥤ ShrinkHoms LightCondAb := +-- inducedFunctor _ -- TODO: define this property: -- instance : PreservesExtensions (solidToCondensed R) := sorry -instance : solidToCondensed.IsRightAdjoint := by +instance : solidToCondensed.IsRightAdjoint := by sorry -- TODO: use construction of left adjoint for Bousfield localizations instead - let i : solidToCondensed ≅ (ShrinkHoms.equivalence.{0} Solid).functor ⋙ - solidToCondensed' ⋙ - (ShrinkHoms.equivalence.{0} LightCondAb).inverse := by - refine NatIso.ofComponents (fun _ ↦ Iso.refl _) ?_ - intro X Y f - simp only [solidToCondensed_obj, ShrinkHoms.equivalence_functor, ShrinkHoms.equivalence_inverse, - Functor.comp_obj, ShrinkHoms.functor_obj, ShrinkHoms.inverse_obj, - solidToCondensed_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, - ShrinkHoms.functor_map, ShrinkHoms.inverse_map, Category.id_comp] - erw [Equiv.apply_symm_apply] - have : HasLimits (ShrinkHoms Solid) := - Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence _).inverse - have : HasLimits (ShrinkHoms LightCondAb) := - Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence _).inverse - have : PreservesLimits solidToCondensed' := sorry - have : solidToCondensed'.IsRightAdjoint := by - apply isRightAdjoint_of_preservesLimits_of_solutionSetCondition - intro A - sorry - have : ((ShrinkHoms.equivalence.{0} Solid).functor ⋙ - inducedFunctor _ ⋙ - (ShrinkHoms.equivalence.{0} LightCondAb).inverse).IsRightAdjoint := by - apply (config := {allowSynthFailures := true}) Functor.isRightAdjoint_comp - apply (config := {allowSynthFailures := true}) Functor.isRightAdjoint_comp - exact this - apply Functor.isRightAdjoint_of_iso i.symm + -- let i : solidToCondensed ≅ (ShrinkHoms.equivalence.{0} Solid).functor ⋙ + -- solidToCondensed' ⋙ + -- (ShrinkHoms.equivalence.{0} LightCondAb).inverse := by + -- refine NatIso.ofComponents (fun _ ↦ Iso.refl _) ?_ + -- intro X Y f + -- simp only [solidToCondensed_obj, ShrinkHoms.equivalence_functor, ShrinkHoms.equivalence_inverse, + -- Functor.comp_obj, ShrinkHoms.functor_obj, ShrinkHoms.inverse_obj, + -- solidToCondensed_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, + -- ShrinkHoms.functor_map, ShrinkHoms.inverse_map, Category.id_comp] + -- erw [Equiv.apply_symm_apply] + -- have : HasLimits (ShrinkHoms Solid) := + -- Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence _).inverse + -- have : HasLimits (ShrinkHoms LightCondAb) := + -- Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence _).inverse + -- have : PreservesLimits solidToCondensed' := sorry + -- have : solidToCondensed'.IsRightAdjoint := by + -- apply isRightAdjoint_of_preservesLimits_of_solutionSetCondition + -- intro A + -- sorry + -- have : ((ShrinkHoms.equivalence.{0} Solid).functor ⋙ + -- inducedFunctor _ ⋙ + -- (ShrinkHoms.equivalence.{0} LightCondAb).inverse).IsRightAdjoint := by + -- apply (config := {allowSynthFailures := true}) Functor.isRightAdjoint_comp + -- apply (config := {allowSynthFailures := true}) Functor.isRightAdjoint_comp + -- exact this + -- apply Functor.isRightAdjoint_of_iso i.symm def solidification : LightCondAb ⥤ Solid := solidToCondensed.leftAdjoint diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean index f668dd4..b538b80 100644 --- a/LeanCondensed/Projects/Proj.lean +++ b/LeanCondensed/Projects/Proj.lean @@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jonas van der Schaaf -/ import Mathlib.Condensed.Light.InternallyProjective +import Mathlib.Topology.Category.CompHausLike.Cartesian +import Mathlib.Topology.Category.LightProfinite.Injective import Mathlib.Topology.FiberPartition -import LeanCondensed.Projects.LightProfiniteInjective import LeanCondensed.Projects.PreservesCoprod import LeanCondensed.Projects.Epi import LeanCondensed.Mathlib.CategoryTheory.Countable -import LeanCondensed.Mathlib.Topology.Category.CompHausLike.Limits open CategoryTheory Category Functor LightProfinite OnePoint LightCondensed MonoidalCategory CartesianMonoidalCategory CompHausLike @@ -64,7 +64,7 @@ def fibre : LightProfinite := isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact of (f ⁻¹' {y}) -def fibre_incl : fibre y f ⟶ X := ⟨{ toFun := Subtype.val }⟩ +def fibre_incl : fibre y f ⟶ X := ⟨⟨{ toFun := Subtype.val }⟩⟩ variable {Z : LightProfinite} {f : X ⟶ Z} {g : Y ⟶ Z} @@ -166,9 +166,9 @@ lemma smartCoverToFun_surjective {S T X : Type*} (π : T → S × Option X) (σ which is given by this morphism. -/ def smartCoverNew {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : (of _ (T ⊕ (pullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) - (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨{ + (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨⟨{ toFun := smartCoverToFun _ _ - continuous_toFun := by dsimp [smartCoverToFun]; fun_prop }⟩ + continuous_toFun := by dsimp [smartCoverToFun]; fun_prop }⟩⟩ def sectionOfFibreIncl {S T X : Type*} (π : T → S × Option X) (σ : Option X → S → T) (hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x) : S → (Prod.snd ∘ π_r π σ) ⁻¹' {none} := @@ -292,7 +292,7 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : -- `fibresOfOption`. have := S'_compactSpace π (by fun_prop) let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ fibre n (π ≫ snd _ _) := - ⟨{ toFun x := x.val n, continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩ + ⟨⟨{ toFun x := x.val n, continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩⟩ let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩ let π' := pullback.snd π (y' ▷ ℕ∪{∞}) let σ' : ℕ∪{∞} → LightProfinite.of (S' π) → pullback π (y' ▷ ℕ∪{∞}) := fun n ↦ diff --git a/LeanCondensed/Projects/Sequence.lean b/LeanCondensed/Projects/Sequence.lean index 500d434..27a89e7 100644 --- a/LeanCondensed/Projects/Sequence.lean +++ b/LeanCondensed/Projects/Sequence.lean @@ -8,7 +8,12 @@ import Mathlib.Combinatorics.Quiver.ReflQuiver import Mathlib.Condensed.Light.Functors import Mathlib.Condensed.Light.Module import Mathlib.Topology.Category.LightProfinite.Sequence -import Mathlib.Topology.Compactness.PseudometrizableLindelof +import Mathlib.Data.Finset.Attr +import Mathlib.Tactic.Common +import Mathlib.Tactic.Continuity +import Mathlib.Tactic.Finiteness.Attr +import Mathlib.Tactic.SetLike +import Mathlib.Util.CompileInductive import Mathlib.Topology.Connected.Separation import Mathlib.Topology.Spectral.Prespectral @@ -21,10 +26,10 @@ noncomputable section variable (R : Type _) [CommRing R] def ι : LightProfinite.of PUnit.{1} ⟶ ℕ∪{∞} := - (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) + (ConcreteCategory.ofHom ⟨fun _ ↦ ∞, continuous_const⟩) def ι_split : SplitMono ι where - retraction := (TopCat.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩) + retraction := (ConcreteCategory.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩) id := rfl def P_map : diff --git a/lake-manifest.json b/lake-manifest.json index 3f29673..3ffc22f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "07946e860d2f824f658fe62db9a3b010e953cd60", + "rev": "7cccd8a4ca2caff3505b0419559f646e1824769f", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "74835c84b38e4070b8240a063c6417c767e551ae", + "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3", + "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710", + "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.82", + "inputRev": "v0.0.86", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e", + "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3", + "rev": "23324752757bf28124a518ec284044c8db79fee5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0", + "rev": "a7ab123915d17f92587c2b1ec7218db7db7856e1", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9", + "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", + "inputRev": "v4.28.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "LeanCondensed", diff --git a/lean-toolchain b/lean-toolchain index 7035713..3e9b4e1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0-rc2 \ No newline at end of file +leanprover/lean4:v4.28.0-rc1 \ No newline at end of file