Zulip Chat Archive

Stream: condensed mathematics

Topics:

Writing the LTE paper (1 message, latest: Apr 19 2024 at 15:15)
Light condensed sets (3 messages, latest: Dec 02 2023 at 00:25)
blueprint (58 messages, latest: Sep 04 2023 at 09:38)
Formalisation of condensed maths in Copenhagen (1 message, latest: Apr 27 2023 at 07:34)
Condensed mathematics at CIRM (1 message, latest: Oct 07 2022 at 15:42)
LTE is in mathlib (4 messages, latest: Sep 29 2022 at 16:24)
The elephant in the room (475 messages, latest: Sep 27 2022 at 09:43)
how much mathlib in LTE? (109 messages, latest: Sep 20 2022 at 07:51)
Condensed.pdf Thm 3.3 (24 messages, latest: Sep 16 2022 at 22:49)
leancrawler bug (37 messages, latest: Sep 14 2022 at 08:42)
MO question (9 messages, latest: Sep 05 2022 at 15:08)
README (12 messages, latest: Aug 30 2022 at 15:34)
Real measures (144 messages, latest: Aug 30 2022 at 07:42)
homology refactor (34 messages, latest: Jul 27 2022 at 17:31)
commsq (4 messages, latest: Jul 27 2022 at 10:45)
ℓᵖ(ℕ, ℝ) (42 messages, latest: Jul 25 2022 at 08:45)
citing (4 messages, latest: Jul 24 2022 at 14:44)
CI status (7 messages, latest: Jul 22 2022 at 14:35)
celebration party (9 messages, latest: Jul 22 2022 at 05:02)
Ext (31 messages, latest: Jul 21 2022 at 17:20)
move me (9 messages, latest: Jul 21 2022 at 10:13)
Actual graph (178 messages, latest: Jul 20 2022 at 22:44)
master/dev (16 messages, latest: Jul 20 2022 at 12:42)
treeshaking (50 messages, latest: Jul 20 2022 at 11:05)
examples (13 messages, latest: Jul 19 2022 at 08:11)
Generating web docs (3 messages, latest: Jul 18 2022 at 15:08)
blogpost (44 messages, latest: Jul 16 2022 at 17:38)
sorry count (405 messages, latest: Jul 15 2022 at 16:10)
axioms (15 messages, latest: Jul 14 2022 at 20:17)
admit (5 messages, latest: Jul 13 2022 at 18:33)
linting (6 messages, latest: Jul 13 2022 at 10:11)
Q' SES (9 messages, latest: Jul 11 2022 at 19:51)
Lbar.ext (42 messages, latest: Jul 10 2022 at 18:00)
breen deligne lemma (34 messages, latest: Jul 10 2022 at 13:02)
endomorphisms (64 messages, latest: Jul 10 2022 at 11:12)
homology_functor_iso (12 messages, latest: Jul 09 2022 at 13:14)
Filtered colimits commute with finite limits (17 messages, latest: Jul 08 2022 at 23:04)
Tensor Products (93 messages, latest: Jul 07 2022 at 12:08)
free abelian group norm (29 messages, latest: Jul 07 2022 at 09:39)
AB4 (10 messages, latest: Jul 06 2022 at 11:43)
Isomorphisms with the homology (76 messages, latest: Jul 02 2022 at 15:38)
BD lemma: last line (31 messages, latest: Jun 30 2022 at 17:34)
single coproducts (14 messages, latest: Jun 28 2022 at 15:11)
for_mathlib/endomorphisms/Ext (1 message, latest: Jun 26 2022 at 16:52)
preserves_finite_colimits_of_exact (7 messages, latest: Jun 26 2022 at 16:30)
sigma bounded above (5 messages, latest: Jun 24 2022 at 06:47)
for_mathlib/truncation.lean (21 messages, latest: Jun 18 2022 at 12:37)
homology of Q' (10 messages, latest: Jun 11 2022 at 23:51)
AB5 (8 messages, latest: Jun 08 2022 at 23:46)
for_mathlib/imker (37 messages, latest: Jun 08 2022 at 11:50)
condensed/acyclic (60 messages, latest: Jun 08 2022 at 08:01)
explicit homology in Ab (1 message, latest: Jun 07 2022 at 10:18)
naturality (4 messages, latest: Jun 04 2022 at 10:18)
overview of what's left (132 messages, latest: Jun 03 2022 at 18:48)
for_mathlib/chain_complex_exact (23 messages, latest: Jun 02 2022 at 15:07)
build fail (13 messages, latest: Jun 01 2022 at 13:07)
for_mathlib/acyclic (101 messages, latest: May 31 2022 at 13:26)
bicartesian squares (14 messages, latest: May 21 2022 at 22:40)
Ext commutes with coproducts (40 messages, latest: May 20 2022 at 06:07)
computing Ext with acyclics (7 messages, latest: May 19 2022 at 14:56)
universe strikes back (28 messages, latest: May 19 2022 at 13:34)
invpoly.ses sorry (7 messages, latest: May 18 2022 at 04:20)
master broken (18 messages, latest: May 17 2022 at 19:34)
δ is functorial (16 messages, latest: May 17 2022 at 16:54)
bicomplex glue (20 messages, latest: May 16 2022 at 19:27)
mathlib bump (422 messages, latest: May 12 2022 at 11:35)
Exact functors (37 messages, latest: May 11 2022 at 22:57)
ses2 sorry-free (3 messages, latest: May 09 2022 at 21:27)
salamander/ab cat stuff (21 messages, latest: May 09 2022 at 21:27)
limits in Ab (11 messages, latest: May 09 2022 at 00:05)
split_exact (8 messages, latest: May 07 2022 at 11:01)
homology in Ab (4 messages, latest: May 07 2022 at 04:02)
ingredients (10 messages, latest: May 06 2022 at 00:11)
laurent measures (111 messages, latest: May 03 2022 at 18:42)
fintype_functor (47 messages, latest: May 02 2022 at 17:19)
acyclics (3 messages, latest: May 02 2022 at 13:41)
1/2 is not canonical (14 messages, latest: Apr 30 2022 at 13:11)
Prop 2.1 (102 messages, latest: Apr 28 2022 at 14:54)
free_pfpng.epi (5 messages, latest: Apr 27 2022 at 12:42)
profinite trivialities (27 messages, latest: Apr 22 2022 at 15:59)
spaces of measures / R (127 messages, latest: Apr 20 2022 at 11:38)
blueprint ci (42 messages, latest: Apr 19 2022 at 20:16)
0 \ne 0 (13 messages, latest: Apr 19 2022 at 14:28)
completion of locally constant functions (10 messages, latest: Apr 19 2022 at 08:37)
is_zero sorries (5 messages, latest: Apr 19 2022 at 08:03)
thm69 (4 messages, latest: Apr 18 2022 at 08:23)
unicode in defs (4 messages, latest: Apr 16 2022 at 21:29)
Filtered colimits of condensed sets (16 messages, latest: Apr 15 2022 at 16:14)
exact functor (23 messages, latest: Apr 13 2022 at 14:44)
condensed/exact.lean (65 messages, latest: Apr 12 2022 at 12:54)
blueprint / dependency graph (107 messages, latest: Apr 12 2022 at 05:37)
derived_cat (25 messages, latest: Apr 11 2022 at 21:37)
homology op (6 messages, latest: Apr 11 2022 at 19:24)
rescale_preserves_limits_of_shape_discrete_quotient (16 messages, latest: Apr 10 2022 at 13:15)
bounding mapping cone (9 messages, latest: Apr 05 2022 at 19:22)
Section 5 (11 messages, latest: Apr 05 2022 at 11:48)
r<1 (13 messages, latest: Apr 02 2022 at 16:52)
CI failing (9 messages, latest: Apr 02 2022 at 11:47)
def of comphaus_filtered_pseudo_normed_group_hom (5 messages, latest: Mar 31 2022 at 13:21)
short exact skeleton (5 messages, latest: Mar 28 2022 at 13:07)
homological todos (47 messages, latest: Mar 28 2022 at 11:31)
blueprint software (2 messages, latest: Mar 25 2022 at 10:40)
exact_with_constant (2 messages, latest: Mar 23 2022 at 13:46)
asyncI (23 messages, latest: Mar 23 2022 at 13:45)
normed group todo (1 message, latest: Mar 22 2022 at 13:28)
colimits commute with colimits (32 messages, latest: Mar 21 2022 at 18:10)
shifting triangles (149 messages, latest: Mar 21 2022 at 15:58)
abstract nonsense about pseudo-normed groups (43 messages, latest: Mar 17 2022 at 15:13)
nontrivial Ext group (3 messages, latest: Mar 14 2022 at 21:54)
for_mathlib (184 messages, latest: Mar 12 2022 at 07:49)
extending complexes (12 messages, latest: Mar 11 2022 at 14:56)
empty and binary imply finary (5 messages, latest: Mar 05 2022 at 20:18)
long exact sequence (51 messages, latest: Mar 02 2022 at 14:41)
two step resolutions (2 messages, latest: Mar 02 2022 at 13:22)
AddCommGroup vs Z Modules (3 messages, latest: Feb 28 2022 at 04:56)
[module.free 0] (23 messages, latest: Feb 27 2022 at 23:12)
OPS (2 messages, latest: Feb 27 2022 at 22:43)
✔ 2-step proj resolution (PID) (2 messages, latest: Feb 26 2022 at 17:23)
2-step proj resolution (PID) (11 messages, latest: Feb 26 2022 at 14:27)
holiday (1 message, latest: Feb 26 2022 at 06:40)
submodule of free module over PID is free (8 messages, latest: Feb 24 2022 at 21:23)
exact_seq (1 message, latest: Feb 24 2022 at 21:09)
./scripts/fetch_olean_cache.sh (7 messages, latest: Feb 24 2022 at 17:32)
Projective replacements (2 messages, latest: Feb 23 2022 at 17:33)
Priestley spaces (34 messages, latest: Feb 22 2022 at 21:13)
p-Banach spaces (25 messages, latest: Feb 22 2022 at 17:22)
LES for Ext (217 messages, latest: Feb 19 2022 at 05:02)
Stonean spaces (19 messages, latest: Feb 18 2022 at 13:44)
nnrat (8 messages, latest: Feb 17 2022 at 21:02)
extr disc projective in CompHaus (21 messages, latest: Feb 17 2022 at 20:36)
exactness in Cond(Ab) (1 message, latest: Feb 16 2022 at 20:22)
CI (14 messages, latest: Feb 16 2022 at 17:55)
Topological spaces (14 messages, latest: Feb 11 2022 at 19:06)
Ext^i(Mbar(S), V) = 0 (69 messages, latest: Feb 11 2022 at 09:04)
Mbar → Lbar (9 messages, latest: Feb 10 2022 at 09:37)
Potential Refactor (119 messages, latest: Feb 09 2022 at 18:53)
LTE on MathOverflow (7 messages, latest: Feb 08 2022 at 04:03)
Lemma 9.8 (25 messages, latest: Feb 02 2022 at 12:02)
Sheaves on ExtrDisc (27 messages, latest: Jan 24 2022 at 20:06)
SES of thm 6.9 (21 messages, latest: Jan 20 2022 at 15:48)
Abelian sheaves (56 messages, latest: Jan 10 2022 at 15:48)
9.8 for profinite S (2 messages, latest: Jan 10 2022 at 13:31)
snake lemma (158 messages, latest: Jan 08 2022 at 20:09)
gordan's lemma (52 messages, latest: Jan 06 2022 at 17:43)
thm 69 (125 messages, latest: Dec 23 2021 at 09:25)
distinguished triangles (9 messages, latest: Dec 13 2021 at 16:10)
Cauchy-Hadamard (3 messages, latest: Dec 10 2021 at 19:05)
github project (4 messages, latest: Nov 30 2021 at 14:57)
tensor product of sheaves (17 messages, latest: Nov 29 2021 at 22:22)
some pointset topology (11 messages, latest: Nov 27 2021 at 07:01)
breen deligne update (2 messages, latest: Nov 16 2021 at 13:33)
Locally compact groups (2 messages, latest: Nov 16 2021 at 11:00)
Sheafification (36 messages, latest: Nov 15 2021 at 15:58)
finite powers (biproducts) (33 messages, latest: Nov 08 2021 at 18:37)
exact sequences in concrete abelian categories (9 messages, latest: Nov 08 2021 at 12:21)
blueprint update (28 messages, latest: Nov 08 2021 at 05:22)
condensed abelian groups (150 messages, latest: Nov 08 2021 at 01:49)
project build workflow (1 message, latest: Nov 06 2021 at 14:34)
status update (402 messages, latest: Oct 30 2021 at 17:42)
README.md (2 messages, latest: Oct 30 2021 at 06:06)
triangles and shifts (33 messages, latest: Oct 25 2021 at 19:01)
SemiNormedGroup_Completion.lean (10 messages, latest: Oct 18 2021 at 14:27)
Floor semiring (4 messages, latest: Oct 17 2021 at 17:12)
Sheaf conditions (41 messages, latest: Oct 16 2021 at 19:56)
Explicit cokernel (18 messages, latest: Oct 14 2021 at 14:47)
universes (1 message, latest: Oct 12 2021 at 15:27)
Condensed R-modules (10 messages, latest: Oct 08 2021 at 13:12)
main statement (106 messages, latest: Oct 06 2021 at 04:55)
finite exact sequences (29 messages, latest: Sep 29 2021 at 20:18)
import clash? (11 messages, latest: Sep 29 2021 at 19:45)
short exact sequences (10 messages, latest: Sep 29 2021 at 14:19)
salamander tactic (10 messages, latest: Sep 27 2021 at 12:41)
thm69_bad (4 messages, latest: Sep 23 2021 at 17:59)
delta functors (12 messages, latest: Sep 22 2021 at 16:39)
9.4 for profinite S (2 messages, latest: Sep 16 2021 at 20:29)
✔ Basic questions on the formalization of maths exercises (3 messages, latest: Sep 10 2021 at 09:50)
Limits in CompHaus…_1 (21 messages, latest: Sep 09 2021 at 03:22)
Project status (7 messages, latest: Sep 07 2021 at 14:56)
linter (8 messages, latest: Sep 04 2021 at 05:57)
spaces of measure / Z((T))_r (315 messages, latest: Sep 03 2021 at 06:44)
condensed sets (94 messages, latest: Sep 03 2021 at 03:16)
abelian sheaves (2 messages, latest: Sep 02 2021 at 15:15)
condensed rings of laurent series (6 messages, latest: Aug 26 2021 at 22:02)
laurent series (100 messages, latest: Aug 26 2021 at 19:14)
Kronecker product (94 messages, latest: Aug 20 2021 at 09:59)
col_exact (159 messages, latest: Aug 20 2021 at 05:20)
extremally disconnected sets (129 messages, latest: Aug 11 2021 at 09:56)
github issues (12 messages, latest: Aug 10 2021 at 15:36)
Gromov (2 messages, latest: Aug 02 2021 at 21:41)
attribution (28 messages, latest: Jul 28 2021 at 20:18)
Mbar functor (66 messages, latest: Jul 27 2021 at 12:50)
pseudonormed hierarchy (79 messages, latest: Jul 17 2021 at 01:23)
summary of proof (5 messages, latest: Jul 16 2021 at 09:10)
lessons learned (33 messages, latest: Jul 07 2021 at 17:02)
for_mathlib/wide_pullback (15 messages, latest: Jul 01 2021 at 18:23)
unused arguments (2 messages, latest: Jun 28 2021 at 06:35)
clean up / documentation (4 messages, latest: Jun 25 2021 at 13:46)
constants and parameters (5 messages, latest: Jun 25 2021 at 09:17)
universal map refactor (12 messages, latest: Jun 24 2021 at 03:21)
solid resolution theory (5 messages, latest: Jun 22 2021 at 13:14)
free module (16 messages, latest: Jun 22 2021 at 12:26)
Nature news story (27 messages, latest: Jun 22 2021 at 00:49)
bound_by (28 messages, latest: Jun 18 2021 at 11:55)
meta (10 messages, latest: Jun 18 2021 at 08:39)
explicit computation (287 messages, latest: Jun 17 2021 at 23:05)
online party (20 messages, latest: Jun 10 2021 at 17:32)
SemiNormedGroup completion (10 messages, latest: Jun 09 2021 at 13:45)
constants (147 messages, latest: Jun 09 2021 at 10:45)
notation (10 messages, latest: Jun 09 2021 at 07:36)
TODOs (16 messages, latest: Jun 07 2021 at 11:59)
bumping mathlib (94 messages, latest: Jun 07 2021 at 10:55)
FLC_iso (28 messages, latest: Jun 05 2021 at 04:25)
statement (5 messages, latest: May 31 2021 at 14:53)
pow rescale pow (28 messages, latest: May 28 2021 at 18:14)
congr' 5 (3 messages, latest: May 26 2021 at 11:34)
Project statistics (17 messages, latest: May 26 2021 at 08:13)
isometry (8 messages, latest: May 25 2021 at 16:11)
More on profinite sets (10 messages, latest: May 24 2021 at 15:28)
alternating face map deduplication (1 message, latest: May 24 2021 at 11:01)
rescaling norms and weak exactness (6 messages, latest: May 23 2021 at 12:45)
Dual snake lemma (90 messages, latest: May 21 2021 at 15:08)
strict isomorphism (3 messages, latest: May 20 2021 at 23:56)
complexes, d, dtt (329 messages, latest: May 19 2021 at 20:09)
SemiNormedGroup (6 messages, latest: May 19 2021 at 19:24)
lemma 9.2 (117 messages, latest: May 18 2021 at 23:19)
nonneg (19 messages, latest: May 18 2021 at 03:22)
finite_free wishlist (4 messages, latest: May 17 2021 at 14:55)
finite_free (8 messages, latest: May 17 2021 at 10:24)
breen_deligne.suitable (7 messages, latest: May 16 2021 at 18:55)
mathlib sprint (288 messages, latest: May 15 2021 at 13:45)
cokernels in normed_group/NormedGroup (29 messages, latest: May 15 2021 at 10:16)
toric (523 messages, latest: May 14 2021 at 11:05)
liquid tensor experiment (50 messages, latest: May 14 2021 at 09:36)
cech_stuff (135 messages, latest: May 11 2021 at 08:20)
proetale site on profinite (33 messages, latest: May 03 2021 at 15:20)
progress (23 messages, latest: May 03 2021 at 08:41)
nsmul and Lean 4 (23 messages, latest: May 02 2021 at 08:58)
thm95.homotopy (154 messages, latest: May 01 2021 at 20:04)
LocallyConstant preserves colimits (92 messages, latest: Apr 30 2021 at 20:32)
Profinite PR(s) (1 message, latest: Apr 30 2021 at 16:55)
reasonably easy sorries (5 messages, latest: Apr 28 2021 at 14:44)
Merge profinite branch to master (41 messages, latest: Apr 27 2021 at 21:49)
toric branch issues (65 messages, latest: Apr 27 2021 at 07:47)
Exactness for Cech complex (8 messages, latest: Apr 25 2021 at 19:33)
Hom(Lambda, M) (3 messages, latest: Apr 22 2021 at 07:25)
polyhedral isos (2 messages, latest: Apr 21 2021 at 08:53)
cech predicate (17 messages, latest: Apr 21 2021 at 05:39)
gitpod (12 messages, latest: Apr 17 2021 at 15:56)
projective objects in profinite sets (7 messages, latest: Apr 15 2021 at 08:44)
breen_deligne refactor (4 messages, latest: Apr 13 2021 at 15:10)
docstrings (6 messages, latest: Apr 09 2021 at 06:55)
normed snake lemma (804 messages, latest: Apr 07 2021 at 18:40)
normed group quotient (9 messages, latest: Apr 06 2021 at 07:45)
polyhedral lattice (239 messages, latest: Apr 05 2021 at 13:39)
pseudo normed abelian groups (2 messages, latest: Apr 04 2021 at 19:57)
freestyle (61 messages, latest: Apr 01 2021 at 16:03)
torsion free (125 messages, latest: Apr 01 2021 at 11:57)
lemma 9.7 (319 messages, latest: Apr 01 2021 at 08:22)
homotopies (25 messages, latest: Mar 28 2021 at 14:21)
Simplicial stuff (345 messages, latest: Mar 27 2021 at 05:10)
Can r be 0? (3 messages, latest: Mar 26 2021 at 17:22)
PFPNGWT? (3 messages, latest: Mar 25 2021 at 17:18)
controlled exactness (56 messages, latest: Mar 22 2021 at 22:15)
thm95.double_complex (27 messages, latest: Mar 20 2021 at 21:12)
identity functor is additive (3 messages, latest: Mar 19 2021 at 14:49)
simplex category variant (17 messages, latest: Mar 19 2021 at 13:26)
spectral 9.6 (309 messages, latest: Mar 15 2021 at 21:12)
The system of Mbar r' S is not (yet) admissible (32 messages, latest: Mar 15 2021 at 16:41)
truncation (72 messages, latest: Mar 14 2021 at 17:39)
topology is fun (15 messages, latest: Mar 13 2021 at 22:30)
lean is slow (9 messages, latest: Mar 13 2021 at 19:44)
complexes indexed by N (22 messages, latest: Mar 12 2021 at 13:12)
soft_truncation' (218 messages, latest: Mar 11 2021 at 17:15)
Use of snake lemma vs long exact sequence (6 messages, latest: Mar 11 2021 at 09:45)
possible targets for this week (105 messages, latest: Mar 11 2021 at 04:47)
9.5 => 9.4 pain (19 messages, latest: Mar 10 2021 at 20:25)
combinatorial lemma 9.8 (95 messages, latest: Mar 10 2021 at 09:26)
shift of complexes (42 messages, latest: Mar 09 2021 at 07:05)
condensed terminology (17 messages, latest: Mar 03 2021 at 06:06)
hausdorff school (18 messages, latest: Mar 02 2021 at 17:37)
finitely generated (14 messages, latest: Feb 26 2021 at 05:58)
bounded exactness (183 messages, latest: Feb 24 2021 at 15:21)
completion (10 messages, latest: Feb 22 2021 at 16:04)
homological headache (118 messages, latest: Feb 20 2021 at 18:16)
profinite sets are limits of discrete finite sets (3 messages, latest: Feb 17 2021 at 18:42)
universal maps (67 messages, latest: Feb 12 2021 at 09:29)
repo, sorry, admit (7 messages, latest: Feb 10 2021 at 12:38)
theorem 9.5 (statement) (13 messages, latest: Feb 10 2021 at 08:44)
profinitely filtered pseudo normed topological groups (268 messages, latest: Feb 06 2021 at 08:55)
by exactI (5 messages, latest: Feb 06 2021 at 08:24)
Analytic Prop 6.8 (41 messages, latest: Feb 02 2021 at 21:31)
admissible (5 messages, latest: Jan 26 2021 at 16:10)
extremely disconnected sets (16 messages, latest: Dec 23 2020 at 10:56)
finite jointly surjective map (33 messages, latest: Dec 13 2020 at 22:02)
stream events (17 messages, latest: Dec 09 2020 at 18:13)
analytic theorem 9.4 (42 messages, latest: Dec 08 2020 at 21:07)
topology on a valued ring (1 message, latest: Dec 08 2020 at 18:04)

Last updated: May 02 2025 at 03:31 UTC