## Stream: condensed mathematics

### Topic: soft_truncation'

#### Johan Commelin (Mar 03 2021 at 19:29):

I've stubbed out soft_truncation' in src/system_of_complexes/soft_truncation.lean.

#### Johan Commelin (Mar 03 2021 at 19:30):

@Riccardo Brasca once you have the universal property for the quotient, we should also bundle the quotient into a NormedGroup and then most of the sorrys in that file should be "easy" to fill in.

#### Riccardo Brasca (Mar 03 2021 at 19:42):

Good! I hope this will not take too much

#### Riccardo Brasca (Mar 03 2021 at 19:47):

Is this (S : add_subgroup M) [is_closed (↑S : set M)] the correct way of stating that S is closed in M?

#### Johan Commelin (Mar 03 2021 at 19:48):

I don't think that is_closed is a class, so it should be (hS : ...) instead of []

#### Adam Topaz (Mar 03 2021 at 20:13):

Do we know that the closure of a subgroup of a normed group is again a subgroup subNormedGroup?

#### Adam Topaz (Mar 03 2021 at 20:15):

This must be in mathlib right?

#### Heather Macbeth (Mar 03 2021 at 20:23):

For the submodule version, docs#submodule.topological_closure

#### Heather Macbeth (Mar 03 2021 at 20:24):

There is less API for subgroups than submodules, but it shouldn't be hard to adapt the proof.

#### Heather Macbeth (Mar 03 2021 at 20:25):

Note that you just need that it's a subgroup -- the normed structure follows docs#add_subgroup.normed_group

#### Adam Topaz (Mar 03 2021 at 20:30):

But for the "universal property" you need the kernel to be closed, right?

#### Adam Topaz (Mar 03 2021 at 20:31):

Sorry, what I mean is that the quotient is a normed group only when the subgroup is closed.

#### Heather Macbeth (Mar 03 2021 at 20:31):

Do we know that the closure of a subgroup of a normed group is again a subgroup subNormedGroup?

I was responding to this part -- subgroup implies subNormedGroup.

Oh right, okay.

#### Riccardo Brasca (Mar 03 2021 at 20:49):

I modified the proof, and now we have a norm on the quotient by any closed subspace (in particular by the kernel), it the first lemma below. If is_closed is not an instance, what I am supposed to write in normed_group.mk to let Lean know that (quotient S) is a normed group?

/-- If (m : M) has norm equal to 0 in quotient S for a closed subgroup S of M, then
m ∈ S. -/
lemma norm_zero_eq_zero (S : add_subgroup M) (hS : is_closed (↑S : set M)) (m : M)
(h : ∥(quotient_add_group.mk' S) m∥ = 0) : m ∈ S := sorry

/-- The norm on quotient S is actually a norm if S is a complete subgroup of M. -/
lemma quotient.is_normed_group.core (S : add_subgroup M) (hS : is_closed (↑S : set M)) :
normed_group.core (quotient S) := sorry

/-- An instance of normed_group on the quotient by a subgroup. -/
noncomputable
instance quotient_normed_group (S : add_subgroup M) (hS : is_closed (↑S : set M)) :
normed_group (quotient S) :=
normed_group.of_core (quotient S) (quotient.is_normed_group.core S hS)

/-- The canonical morphism M → (quotient S) as morphism of normed groups. -/
noncomputable
def normed_group.mk (S : add_subgroup M) (hS : is_closed (↑S : set M)) :
normed_group_hom M (quotient S) :=
{ bound' := ⟨1, λ m, by simpa [one_mul] using norm_mk_le _ m⟩,


#### Adam Topaz (Mar 03 2021 at 21:12):

I added the has_shift instance that was mentioned as a TODO in this file..

#### Adam Topaz (Mar 03 2021 at 21:16):

@Riccardo Brasca what I envisioned in my ccomments above was to define add_subgroup.closureas a subgroup again, and take the quotient by that.

#### Adam Topaz (Mar 03 2021 at 21:23):

Maybe we should introduce closed_add_subgroup extending add_subgroup?

#### Riccardo Brasca (Mar 03 2021 at 21:25):

Ah you're right, it's probably the best thing to do!

#### Riccardo Brasca (Mar 03 2021 at 21:26):

I have the impression that, categorically, the quotient exist by any subgroup, and it is the quotient by the closure

Yes that's right

#### Adam Topaz (Mar 03 2021 at 21:27):

The quotient by the closure is the largest quotient which is a normed group

#### Adam Topaz (Mar 03 2021 at 21:28):

In any case, making closed_add_subgroup should be straightforward enough, even with a small API. We can then define the closure function as a function from add_subgroup to closed_add_subgroup, etc.

#### Adam Topaz (Mar 03 2021 at 21:28):

There is even a Galois insertion between the two!

#### Riccardo Brasca (Mar 03 2021 at 21:33):

I think I will stop for today, but if you want to continue feel free to use my proof

/-- If (m : M) has norm equal to 0 in quotient S for a closed subgroup S of M, then
m ∈ S. -/
lemma norm_zero_eq_zero (S : add_subgroup M) (hS : is_closed (↑S : set M)) (m : M)
(h : ∥(quotient_add_group.mk' S) m∥ = 0) : m ∈ S :=
begin
choose g hg using λ n, (norm_mk_lt' S m (@nat.one_div_pos_of_nat ℝ _ n)),
simp only [h, one_div, zero_add] at hg,
have hconv : filter.tendsto (λ n, m + g n) filter.at_top (nhds 0),
{ refine metric.tendsto_at_top.2 (λ ε hε, _),
obtain ⟨N, hN⟩ := exists_nat_ge ε⁻¹,
have Npos := lt_of_lt_of_le (inv_pos.mpr hε) hN,
replace hN := (inv_le_inv Npos (inv_pos.mpr hε)).2 hN,
rw [inv_inv'] at hN,
refine ⟨N, λ n hn, _⟩,
rw [dist_eq_norm _ _, sub_zero],
have npos := lt_trans (lt_of_lt_of_le Npos (nat.cast_le.2 (ge.le hn))) (lt_add_one n),
replace hn := lt_of_le_of_lt (ge.le hn) (lt_add_one n),
have hnε := lt_of_lt_of_le ((inv_lt_inv npos Npos).2 (nat.cast_lt.2 hn)) hN,
exact lt_trans (hg n).2 hnε },
replace hconv := tendsto.add_const (-m) hconv,
replace hS := mem_of_is_seq_closed (is_seq_closed_iff_is_closed.2 hS) (λ n, (hg n).1) hconv,
simpa using hS,
end


#### Adam Topaz (Mar 03 2021 at 21:34):

Which branch is this in?

#### Riccardo Brasca (Mar 03 2021 at 21:34):

I didn't pushed it, since it breaks the rest of the (small) API for quotients

#### Adam Topaz (Mar 03 2021 at 21:35):

Oh, why don't you push it into a new branch, and I'll try to play around with it

#### Riccardo Brasca (Mar 03 2021 at 21:35):

That is now written with [complete_space S]

#### Riccardo Brasca (Mar 03 2021 at 21:36):

OK, I pushed to quotient_closed

#### Adam Topaz (Mar 03 2021 at 21:38):

@Riccardo Brasca did you commit before pushing? the last commit in this branch was made by Johan.

Done

#### Adam Topaz (Mar 03 2021 at 21:40):

Got it! Thanks :)

#### Heather Macbeth (Mar 03 2021 at 21:46):

Maybe we should introduce closed_add_subgroup extending add_subgroup?

I wonder if you should instead make is_closed a class, it might be useful more generally, and then it could be used as a mixin rather than defining closed_add_subgroup directly, which might avoid diamonds at some later point.

#### Adam Topaz (Mar 03 2021 at 21:50):

We can always use fact (is_closed _)

#### Adam Topaz (Mar 03 2021 at 21:55):

Okay, fact (is_closed ...) seems to work well enough.

#### Adam Topaz (Mar 03 2021 at 22:15):

Alright! I added the definition of the closure of a subgroup, and added some facts in the branch topaz_quotient_closed

#### Adam Topaz (Mar 03 2021 at 22:26):

@Riccardo Brasca @Johan Commelin feel free to merge this to whereever you want, if you're happy with the code.

#### Riccardo Brasca (Mar 03 2021 at 22:54):

It seems now really easy to do everything in the correct (?) generality: given a normed group M and any subgroup A, define A.normed_group_quotient, that is the quotient of M by the closure of A with the various mk lemmas. Given another normed group N and f : normed_group_hom M N such that f a = 0 for all a ∈ A, then we have f a = 0 a ∈ topological_closure A and so we have lift f : A.normed_group_quotient N (the proof of boundedness is immediate).

#### Adam Topaz (Mar 03 2021 at 22:54):

Yes, this all sounds very reasonable.

#### Adam Topaz (Mar 03 2021 at 23:00):

I guess we're also missing the fact that NormedGroup has images of morphisms?

#### Riccardo Brasca (Mar 03 2021 at 23:03):

There is range, in normed_group_hom.lean. But it is only a subgroup

#### Adam Topaz (Mar 03 2021 at 23:06):

Okay, I'll sketch some code for the image too...

#### Heather Macbeth (Mar 03 2021 at 23:12):

Are you asking that the range of a bounded homomorphism be closed? I believe this is not true in general, consider the map from $c_0$ to itself sending $(x_i)$ to $(i^{-1}x_i)$.

#### Adam Topaz (Mar 03 2021 at 23:14):

No that's not what I'm asking for.

#### Adam Topaz (Mar 03 2021 at 23:14):

I just want the image as a normed group

#### Adam Topaz (Mar 03 2021 at 23:14):

no closedness assumptions for now.

#### Heather Macbeth (Mar 03 2021 at 23:14):

Oh, I see. But a subgroup is a normed group, docs#add_subgroup.normed_group

#### Adam Topaz (Mar 03 2021 at 23:16):

I know, I'm just bundling so that it becomes a NormedGroup where we can do categorical stuff :)

#### Heather Macbeth (Mar 03 2021 at 23:16):

Oh, normed_group vs NormedGroup :)

#### Adam Topaz (Mar 03 2021 at 23:16):

And I want an actual has_images instance for NormedGroup as well

#### Riccardo Brasca (Mar 03 2021 at 23:26):

Note that the correct notion of image seems to be the closure of the group theoretic image (I mean, the kernel of the cokernel), but this is probably not very important

#### Adam Topaz (Mar 03 2021 at 23:28):

Well, NormedGroup is not an abelian category is it? So we don't necessarily have that the image of a morphism is the kernel of the map to its cokernel.

#### Kevin Buzzard (Mar 03 2021 at 23:30):

Right, but I should think that it's the category-theoretic image nonetheless.

#### Adam Topaz (Mar 03 2021 at 23:31):

What is? The closure of the set-theoretic image?

#### Adam Topaz (Mar 03 2021 at 23:32):

I think the category-theoretic image is the usual group-theoretic image with the induced structure of a normed_group.

#### Kevin Buzzard (Mar 03 2021 at 23:33):

Oh sorry, you're right, I was thinking of cokernels

#### Kevin Buzzard (Mar 03 2021 at 23:34):

You have to think carefully about whether the norm is the one coming from the source or the target I guess

#### Riccardo Brasca (Mar 03 2021 at 23:35):

According to the stack project, in any preadditive category, we call image of a morphism the kernel of the cokernel (is these exist)

#### Riccardo Brasca (Mar 03 2021 at 23:36):

I have the impression that the kernel and cokernel always exist

#### Adam Topaz (Mar 03 2021 at 23:36):

Well, in any case, here's a preliminary defn:

-- Note: the next sorry needs a NormedGroup, so we need to bundle.
def X (C : cochain_complex NormedGroup) : ℤ → NormedGroup
| -[1+n]  := 0
| 0       := NormedGroup.of $quotient (C.d (-1)).range.topological_closure | (n+1:ℕ) := C.X (n+1)  #### Adam Topaz (Mar 03 2021 at 23:36): Which should be correct. #### Adam Topaz (Mar 03 2021 at 23:37): This is the more general defn of images: https://ncatlab.org/nlab/show/image #### Adam Topaz (Mar 03 2021 at 23:37): (which agrees with docs#category_theory.limits.has_images ) #### Riccardo Brasca (Mar 03 2021 at 23:38): normedgroup is probably {pre,semi}abelian, or something like that #### Adam Topaz (Mar 03 2021 at 23:39): In any case, I don't have any more time to work on this today. I pushed the defn above to topaz_quotient_closed here https://github.com/leanprover-community/lean-liquid/blob/564878d91e8b0864294bd06be16de17ab982c38f/src/system_of_complexes/soft_truncation.lean#L31 In case anyone wants to build on top of it #### Riccardo Brasca (Mar 03 2021 at 23:44): What I mean is that the closure of the group theoretic image controls the epimorphisms, and similar the closure of the (already closed) kernel controls the monomorphisms, so for the image we should really take the closure. What is missing to be abelian is that mono + epi = iso (for example the inclusion of a dense subspace) #### Adam Topaz (Mar 03 2021 at 23:45): Yes, I completely agree with that :) #### Adam Topaz (Mar 04 2021 at 05:08): I'm thinking about the universal property of quotients of morphisms of NormedGroups. Is it really true that the quotient by the closure of the image provides a "correct" cokernel? I don't see how to prove the first sorry in the following: variables {A B C : NormedGroup.{u}} @[simp] noncomputable def coker (f : A ⟶ B) : NormedGroup := NormedGroup.of$

@[simp]
noncomputable
def coker.π {f : A ⟶ B} : B ⟶ coker f :=
normed_group_hom.normed_group.mk _

lemma coker.π_surjective {f : A ⟶ B} : function.surjective (coker.π : B ⟶ coker f).to_add_monoid_hom :=
surjective_quot_mk _

open normed_group_hom

noncomputable
def lift {f : A ⟶ B} {g : B ⟶ C} (cond : f ≫ g = 0) : coker f ⟶ C :=
{ bound' := begin
-- Is this actually true!?
sorry
end,
intros b hb,
sorry,
end ) }


The code is found here, in case anyone wants to play with it:
https://github.com/leanprover-community/lean-liquid/blob/9090c7846b8fe32f601a69fbef38960696063963/src/normed_group/NormedGroup.lean#L126

I'm a little suspicious as to whether this is actually true. It seems like some completeness is necessary.

#### Johan Commelin (Mar 04 2021 at 05:17):

Thanks for all the work!

#### Adam Topaz (Mar 04 2021 at 06:10):

Okay, I think it's actually true.

I added a sketch of proof, but now I should go to sleep...
https://github.com/leanprover-community/lean-liquid/blob/50b8c497108fae8752b87a9ff57f6a8e0ac8e877/src/normed_group/NormedGroup.lean#L126

A few sorry's there are just me being lazy and not wanting to look through api docs, and some of these sorry's should be very easy.

#### Johan Commelin (Mar 04 2021 at 10:40):

@Riccardo Brasca @Adam Topaz would you mind merging your progress into master as soon as you think it is a sensible approach?

#### Johan Commelin (Mar 04 2021 at 10:40):

There are ~38 sorrys on master now, and it doesn't matter if that number grows a bit (-;

#### Riccardo Brasca (Mar 04 2021 at 11:00):

I think we are pretty close to a reasonable situation for quotients, if you can wait a little bit we can then merge into master.

#### Riccardo Brasca (Mar 04 2021 at 11:01):

@Adam Topaz I have the impression you are making things more complicated than they are

#### Johan Commelin (Mar 04 2021 at 11:02):

@Riccardo Brasca sure! It just would be unfortunate if your two branches diverge

#### Johan Commelin (Mar 04 2021 at 11:03):

Contrary to mathlib, I'm perfectly happy with pushing half-fleshed out ideas to master in LTE. The only "rule" is that everything should compile.

#### Riccardo Brasca (Mar 04 2021 at 11:04):

In https://github.com/leanprover-community/lean-liquid/blob/quotient_closed/src/for_mathlib/normed_group_quotient.lean I put an instance of a normed group on quotient S.topological_closure, for any subgroup S (the structure of instances is bad, but the idea is the correct one I think). I have to teach soon, but using norm_mk_le proving that the lifting is bounded is immediate

#### Riccardo Brasca (Mar 04 2021 at 11:05):

We only need to prove that if f is 0 on S then it is 0 on S.topological_closureand we got the lifting

#### Riccardo Brasca (Mar 04 2021 at 12:22):

What is the correct way of doing the following (if it is a reasonable strategy at all...)? I want something like

/-- The quotient in the category of normed groups. -/
noncomputable
def normed_group_quotient (S : add_subgroup M) : normed_group (quotient S.topological_closure) :=
normed_group.of_core (quotient S.topological_closure) (quotient.is_normed_group.core S)


But now normed_group_quotient S is of type normed_group (quotient S.topological_closure) and I guess that what I really want is to be of type Type* with an instance of normed group. Should I do this by hand? In particular I am worried to lose all the API for quotient groups...

#### Johan Commelin (Mar 04 2021 at 12:32):

@Riccardo Brasca I think that (quotient S.topological_closure) is automatically coerced to Type*

#### Johan Commelin (Mar 04 2021 at 12:33):

So you could afterwards define something like

def NormedGroup.quotient (V : NormedGroup) (S : add_subgroup V) : NormedGroup :=
NormedGroup.of (quotient S.topological_closure)


#### Johan Commelin (Mar 04 2021 at 12:34):

This will work if your def above is an instance, so that NormedGroup.of can pick up that instance and bundle it.

#### Adam Topaz (Mar 04 2021 at 13:42):

@Riccardo Brasca The way this currently works in my branch is that you have a normed group instance on the quotient by a closed subgroup, where the is_closed assumption is under a fact. Then I have an instance of fact (is_closed ...) for the topological closure of a subgroup, hence the typeclass system automatically gives you the normed group instance for the quotient by the topological closure of a subgroup.

#### Riccardo Brasca (Mar 04 2021 at 13:42):

@Adam Topaz sorry, norm_mk_le is the wrong inequality... I am writing the good one

#### Adam Topaz (Mar 04 2021 at 13:43):

Riccardo Brasca said:

We only need to prove that if f is 0 on S then it is 0 on S.topological_closureand we got the lifting

:up: yes, this is exactly the key point in the proofs involved in coker.lift.

#### Adam Topaz (Mar 04 2021 at 13:45):

I think it's a bit silly to do

lemma quotient.is_normed_group.core (S : add_subgroup M) :
normed_group.core (quotient S.topological_closure) :=


since then it will be a pain to get an instance of a normed group on a quotient when you happen to know that your subgroup is alreaedy closed.

#### Adam Topaz (Mar 04 2021 at 13:45):

For example we may want to take the quotient by the kernel of a morphism, without having to manually prove that the kernel of a morphism equals its own topological closure

#### Adam Topaz (Mar 04 2021 at 13:46):

Here's the skeleton of the argument for lift I had last night:

def lift {f : A ⟶ B} {g : B ⟶ C} (cond : f ≫ g = 0) : coker f ⟶ C :=
{ bound' := begin
rcases g.bound with ⟨c,hcpos,hc⟩,
use c,
intros v,
rcases coker.π_surjective v with ⟨v,rfl⟩,
change ∥ g v ∥ ≤ c * Inf {r : ℝ | ∃ y : B, coker.π _ = coker.π _ ∧ _ },
-- Should be in mathlib in some form?
have : (c : ℝ) * Inf {r : ℝ | ∃ (y : B), (coker.π y : coker f) = (coker.π v : coker f) ∧ r = ∥y∥} =
Inf {r : ℝ | ∃ (y : B), (coker.π y : coker f) = (coker.π v : coker f) ∧ r = c * ∥ y ∥ }, sorry,
rw this,
rw real.le_Inf,
{ rintros x ⟨b,hx,rfl⟩,
have : g v = g b,
{ have : b - v ∈ f.range.topological_closure, sorry, -- from hx
have : (range f).topological_closure ≤ g.ker,
{ change (closure (f.range : set B)) ⊆ (ker g : set B),
have : is_closed (g.ker : set B), sorry, -- should be separate lemma.
-- there should now be a lemma saying that, given is_closed Y,
-- closure X ⊆ Y ↔ X ⊆ Y
-- Then conclude using cond.
sorry },
suffices : g (b - v) = 0, sorry, -- This must be in mathlib somewhere...
apply this,
assumption,
},
rw this,
apply hc },
{ refine ⟨c * ∥ v ∥,v,rfl, rfl⟩ },
{ use 0,
intros y hy,
rcases hy with ⟨y,hy,rfl⟩,
apply mul_nonneg (le_of_lt _) (norm_nonneg _),
simpa },
end,
intros b hb,
sorry,
end ) }


#### Riccardo Brasca (Mar 04 2021 at 13:48):

I think I will have proof in one hour max (not literally of this statement, but something that is mathematically the same), and then I will think about the Lean design of things

#### Riccardo Brasca (Mar 04 2021 at 14:17):

I've added lift here

#### Riccardo Brasca (Mar 04 2021 at 14:17):

https://github.com/leanprover-community/lean-liquid/blob/quotient_closed/src/for_mathlib/normed_group_quotient.lean

#### Riccardo Brasca (Mar 04 2021 at 14:18):

lemma zero_of_closure {M N : Type*} [normed_group M] [normed_group N] (A : add_subgroup M)
(f : normed_group_hom M N) (hf : ∀ a ∈ A, f a = 0) : ∀ m ∈ A.topological_closure, f m = 0 :=


is still sorry, but it shouldn't be hard

#### Adam Topaz (Mar 04 2021 at 14:20):

Oh I have a proof of that already. Ill fill in the sorry

#### Adam Topaz (Mar 04 2021 at 14:20):

give me a few mins

#### Adam Topaz (Mar 04 2021 at 14:34):

Bah, I filled in the sorry, but my git tree is f-ed up

#### Johan Commelin (Mar 04 2021 at 14:40):

I'm inclined to say: git gud :wink:

4sho

Oh, I pushed it.

#### Adam Topaz (Mar 04 2021 at 14:42):

Again, I have to reiterate that I think ddefining

instance normed_group_quotient (S : add_subgroup M) : normed_group (quotient S.topological_closure) :=


is not the right approach

#### Adam Topaz (Mar 04 2021 at 14:43):

Because then the typeclass system wont get the normed_group instance on things like quotient (f.ker)

#### Riccardo Brasca (Mar 04 2021 at 14:43):

Thank you! Now the mathematics is there, the quotient by S.topological_closure has the required universal property. I don't have any strong opinion about the right approach to this kind of problems

#### Adam Topaz (Mar 04 2021 at 14:45):

We're still missing the uniqueness of lift, but that's not too bad

#### Riccardo Brasca (Mar 04 2021 at 14:47):

Ah, sure, lift is not a lift of anything written like that :D

#### Adam Topaz (Mar 04 2021 at 14:47):

Did you get rid of the instance that I wrote yesterday for quotients by closed subgroups?

#### Adam Topaz (Mar 04 2021 at 14:47):

I can't find it in the branch

#### Adam Topaz (Mar 04 2021 at 14:48):

Well, you wrote it, but I fudged around with fact in the hypotheses to make it work with the typeclass system

#### Riccardo Brasca (Mar 04 2021 at 14:51):

I've added lift_mk

#### Riccardo Brasca (Mar 04 2021 at 14:51):

I didn't touch your branch, but I erased the fact in the branch quotient_closed

#### Adam Topaz (Mar 04 2021 at 14:52):

Ok, I'll add lift_unique

#### Johan Commelin (Mar 04 2021 at 14:53):

I think I like the fact approach, at least until there is enough evidence that we need 400 lines of API around closed_(add)_subgroup

#### Adam Topaz (Mar 04 2021 at 14:53):

I'll add this last lemma, then I'll change back to fact's

#### Riccardo Brasca (Mar 04 2021 at 14:53):

BTW I agree that we should now think about how setting up all the instances and so on. Changing everything now should be quite easy, but the sooner we do it the better

#### Johan Commelin (Mar 04 2021 at 14:53):

Note that we can't have global instances for fact in mathlib. (But in LTE it's fine, yolo, living on the edge)

#### Johan Commelin (Mar 04 2021 at 14:54):

So

instance : fact (is_closed f.ker)


is mathlib-evil.
But of course it can be made an instance locally in some files.

#### Adam Topaz (Mar 04 2021 at 14:56):

The change back is going to be a bit annoying since now we have a bunch of S.topological_closures which will need to be changed back to S.

#### Riccardo Brasca (Mar 04 2021 at 14:57):

I have no problem in doing annoying stuff, I just prefer to not take any decision about what is a def what is an instance...

#### Johan Commelin (Mar 04 2021 at 14:59):

If you have doubts, just go with def. It's usually not too hard to change things to instance later on.

#### Adam Topaz (Mar 04 2021 at 15:00):

So now we have cokernels

#### Adam Topaz (Mar 04 2021 at 15:04):

@Johan Commelin @Riccardo Brasca Are you both okay with me changing back to fact (is_closed ...)?

#### Riccardo Brasca (Mar 04 2021 at 15:04):

No problem for me

#### Adam Topaz (Mar 04 2021 at 15:04):

I'm inclined to just delete my branch with this stuff, it doesn't make sense to have two branches on the same topic

#### Adam Topaz (Mar 04 2021 at 15:05):

If we don't want to use facts then we can always go back to the idea of defining closed_add_subgroup

#### Adam Topaz (Mar 04 2021 at 15:06):

This may be a good option anyway since we will never work with non-closed subgroups.

#### Riccardo Brasca (Mar 04 2021 at 15:09):

What is the policy in mathlib for the quotient by a (not necessarily normal) subgroup? I mean the quotient group (by the normal closure), not the quotient set by the relation, that is not a group. It seems a very similar situation, the quotient exist, but it does not commute with the forgetful functor

#### Adam Topaz (Mar 04 2021 at 15:10):

I think you need the assumption that it's normal

#### Adam Topaz (Mar 04 2021 at 15:11):

docs#quotient_group.quotient.group

#### Adam Topaz (Mar 04 2021 at 15:11):

And normal is a class in this case, so you need the instance. That's what I was trying to simulate with fact

#### Johan Commelin (Mar 04 2021 at 15:12):

@Adam Topaz If you want to set up the API for closed_add_subgroup that's fine with me. But I think fact is also fine.

#### Johan Commelin (Mar 04 2021 at 15:12):

And probably less work from now.

#### Johan Commelin (Mar 04 2021 at 15:12):

My guess is that moving from fact to closed_subgroup later on shouldn't create a lot of trouble.

#### Adam Topaz (Mar 04 2021 at 15:12):

Yeah, I'll go with fact for now. It will be easy to change to closed_add_subgroup later if we want

#### Adam Topaz (Mar 04 2021 at 15:13):

@Riccardo Brasca are you okay with me pushing to your branch? with this fact stuff, I mean?

Sure!

#### Adam Topaz (Mar 04 2021 at 15:25):

Okay, that's done. I'll now add a small wrapper to get cokernels in the category NormedGroup

#### Riccardo Brasca (Mar 04 2021 at 15:36):

Do we want to PR this quotient stuff to mathlib at some point? In that case I can improve the API a little bit (for example adding that the norm of the projection to the quotient is 1)

#### Adam Topaz (Mar 04 2021 at 15:38):

I think the appropriate thing for mathlib is the closed_add_subgroup approach (and it should be done in general for an arbitrary topological group presumably)

#### Adam Topaz (Mar 04 2021 at 15:38):

E.g. we will want quotients by closed subgroups of profinite groups eventuially.

#### Johan Commelin (Mar 04 2021 at 15:39):

I think this is natural stuff to move to mathlib at some point

#### Johan Commelin (Mar 04 2021 at 15:39):

But I imagine that @Heather Macbeth @Sebastien Gouezel will have better ideas about how exactly it should be designed

#### Johan Commelin (Mar 04 2021 at 15:40):

I do agree that closed_subgroup will be a good thing for mathlib. Think infinite Galois theory, and such.

#### Heather Macbeth (Mar 04 2021 at 15:41):

As I was saying yesterday, my first idea was that it would be better for is_closed to be a mixin -- are there reasons not to in this case?

#### Johan Commelin (Mar 04 2021 at 15:46):

For infinite Galois theory, I imagine we want a Galois correspondence between intermediate_subfield and closed_subgroup

#### Johan Commelin (Mar 04 2021 at 15:46):

So then it's actually valuable to have a dedicated type, on which we consider an order structure, etc...

#### Adam Topaz (Mar 04 2021 at 15:49):

Plus in general we will want a galois_insertion between subgroup and closed_subgroup

#### Heather Macbeth (Mar 04 2021 at 15:55):

It would be nice if the solution simultaneously applies to normed spaces and subspaces. For example in normed_space.inner_product we have

lemma submodule.is_closed_orthogonal [inner_product_space 𝕜 E] (K : submodule 𝕜 E) : is_closed ↑Kᗮ


#### Johan Commelin (Mar 04 2021 at 15:59):

I fear that we'll need both closed_(add_)subgroup and closed_sub{module/space?}.

#### Riccardo Brasca (Mar 04 2021 at 16:05):

In any case I will improve a little the API for normed_group_hom. Putting a normed_group instance seems not that far

Merci!

#### Adam Topaz (Mar 04 2021 at 16:14):

@Johan Commelin I'm playing with the soft_truncation stuff, and we still seem to have DTT hell issues :(

#### Johan Commelin (Mar 04 2021 at 16:15):

I'll have dinner first

#### Adam Topaz (Mar 04 2021 at 16:16):

Want to meet on video later?

#### Sebastien Gouezel (Mar 04 2021 at 16:41):

If you see a situation where the set of closed subspaces is in canonically in bijection with something else, then we should go for the bundling. (Personnally, I don't have such a situation in mind for now). Otherwise, the mixin approach seems more lightweight and as efficient. I'd probably avoid fact, though, and turn is_closed into a class instead. Most uses of is_closed would remain as usual assumptions, but one would additionally register just a few instances to make sure that you get instances on the things you need (namely f.ker when f is continuous, and so on)

#### Sebastien Gouezel (Mar 04 2021 at 16:43):

The big advantage of the mixin is that you don't need to define two quotients, one by an add_subgroup and the other one by a closed_add_subgroup and repeat all the API. So I'd probably go for the mixin approach for now, and refactor later if/when needed.

#### Johan Commelin (Mar 04 2021 at 16:50):

Want to meet on video later?

I can probably meet around

#### Adam Topaz (Mar 04 2021 at 16:50):

What time zone is that?

#### Johan Commelin (Mar 04 2021 at 16:51):

I'm using <time

#### Johan Commelin (Mar 04 2021 at 16:51):

So Zulip turns it into your timezone

Fancy!

That works :)

#### Johan Commelin (Mar 04 2021 at 16:51):

I see Thu, Mar 4 2021, 19:15 which is CET

#### Adam Topaz (Mar 04 2021 at 17:14):

@Sebastien Gouezel just to clarify, we only have fact (is_closed ...) in LTE, and we don't expect anything like that to be put in mathlib.

#### Mario Carneiro (Mar 04 2021 at 17:24):

By the way, you can also mouse over the time to see the time in the poster's time zone (i.e. I see 1:15 PM but it says 19:15+0100 in the hover)

#### Johan Commelin (Mar 04 2021 at 17:44):

You want to meet now? meet.jit.si/soft-trunction-dtt

#### Johan Commelin (Mar 04 2021 at 19:13):

Adam convinced me that we need to fix complexes and d before filling in the sorrys in the soft_truncation.lean file

#### Kevin Buzzard (Mar 04 2021 at 22:30):

I still like the idea of d {i} {j} (h : j = i + 1) : C i -> C j. Do we have any arguments against this? I'd like to think it solves a lot of problems

#### Adam Topaz (Mar 04 2021 at 22:31):

Johan and I were discussing the idea of using functors $\mathbb{Z} \to \mathrm{NormedGroup}$ and so far it seems to work fairly well

#### Adam Topaz (Mar 04 2021 at 22:32):

(here $\mathbb{Z}$ is given the category obtained from the ordered structure)

#### Scott Morrison (Mar 04 2021 at 23:13):

regarding the mixin / bundled question, can't one have both? start with the mixin, use that as much as possible, and if there are special cases where the bundled thing is helpful, you just use the mixin as a structure field.

#### Adam Topaz (Mar 04 2021 at 23:17):

So this begs the obvious question: should is_closed (for a general subset of a topological space) be made a class in mathlib? What about is_open?

#### Riccardo Brasca (Mar 04 2021 at 23:42):

BTW, can we merge quotient_closed into master now? If it compiles it is probably better to do it...

Fine with me!

Pushed to master

#### Riccardo Brasca (Mar 04 2021 at 23:56):

Lean says

/github/workspace/src/normed_group/NormedGroup.lean:147:24: error: failed to synthesize type class instance for
A B C : NormedGroup,
f : A ⟶ B,
g : B ⟶ C,
cond : f ≫ g = 0,
h : coker f ⟶ C,
ᾰ : coker.π ≫ h = g
⊢ has_lift (f ≫ g = 0) (coker f ⟶ C)


@Adam Topaz Can you have a look at it? Time to sleep for me...

#### Adam Topaz (Mar 04 2021 at 23:56):

I'll try, but I'm a bit busy now.

#### Adam Topaz (Mar 05 2021 at 00:05):

Okay, I'm fixing it.

#### Adam Topaz (Mar 05 2021 at 00:05):

And adding some docstrings to make the linter happy

#### Adam Topaz (Mar 05 2021 at 00:08):

Shhould be okay now

#### Sebastien Gouezel (Mar 05 2021 at 08:53):

So this begs the obvious question: should is_closed (for a general subset of a topological space) be made a class in mathlib? What about is_open?

I'm working on this, in the branch is_closed_class.

#### Johan Commelin (Mar 05 2021 at 08:54):

of mathlib, or LTE?

#### Kevin Buzzard (Mar 05 2021 at 14:19):

I just pushed a couple more coker lemmas to master in normed_group.NormedGroup. They should be enough to show that (coker C-1 -> C0) -> C2 is zero.

#### Johan Commelin (Mar 09 2021 at 07:10):

We now have the following sorry-free definition:

def shift_and_trunctate : system_of_complexes ⥤ system_of_complexes :=
(shift _).functor ⋙ soft_truncation'


and we need to extend this to

def shift_and_truncate : system_of_double_complexes ⥤ system_of_double_complexes :=
sorry


by applying system_of_complexes.shift_and_truncate to all the rows.

#### Johan Commelin (Mar 09 2021 at 07:11):

@Adam Topaz you did a similar thing for completions, using old-skool complexes. How hard do you think it would be to port this to the new complexes?

#### Kevin Buzzard (Mar 09 2021 at 07:12):

Are we shifting left, up, or up-and-left? (using the orientation conventions in analytic.pdf)

#### Johan Commelin (Mar 09 2021 at 07:12):

we are only shifting left

#### Johan Commelin (Mar 09 2021 at 07:13):

and then truncating whatever got moved into negative degrees

#### Adam Topaz (Mar 09 2021 at 08:41):

This shouldn't be too bad... Just make a functional version of truncation, and prove an additive functor instance for it. So then you can push forward a complex with respect to that functor, then apply the shift. As long as everything is functorial, you can just compose some functors and get the definition you want. I don't know if the order really matters, but you can alternatively do something similar by proving that shifting is additive.

#### Johan Commelin (Mar 09 2021 at 08:44):

We need both to be additive, right?

#### Adam Topaz (Mar 09 2021 at 08:44):

Oh I guess all this requires a preadditive instanc for the category of complexes itself

Hmm, makes sense

#### Johan Commelin (Mar 09 2021 at 08:45):

So there is still a little bit of work to do.

Yeah.

#### Johan Commelin (Mar 09 2021 at 08:45):

And I guess it's better to do that work than to brute force our way through the definition.

#### Adam Topaz (Mar 09 2021 at 08:46):

I can take a look tomorrow (well, today, it's 1:45 am here, and I can't sleep )

#### Adam Topaz (Mar 09 2021 at 08:47):

But I'm also attending a workshop "at MFO" this week, so I don't know if I'll have much time for coding

Oh :)

#### Johan Commelin (Mar 09 2021 at 15:17):

let me push what I have

#### Adam Topaz (Mar 09 2021 at 15:17):

I'm getting stuck at zero_add for some reason anyway! :rofl:

#### Johan Commelin (Mar 09 2021 at 15:17):

See jmc-refactor-complex branch

#### Adam Topaz (Mar 09 2021 at 15:17):

I cant get the ext lemma to behave for some reason.

#### Johan Commelin (Mar 09 2021 at 15:18):

Thinks work a lot smoother now. Even less eq_to_homs

#### Johan Commelin (Mar 09 2021 at 15:18):

But the branch doesn't build yet. I'm in the final stages of fixing the build

#### Johan Commelin (Mar 09 2021 at 15:20):

@Adam Topaz ok, it builds locally

#### Johan Commelin (Mar 09 2021 at 15:21):

I'm really quite happy with the shape that this is now getting in

#### Johan Commelin (Mar 09 2021 at 15:22):

There are dedicated constructors for (co)chain_complex which will introduce some eq_to_homs under the hood. But otherwise you don't see them anywhere.

#### Johan Commelin (Mar 09 2021 at 15:23):

One thing I didn't do yet, is lifting has_shift from differential_object to cochain_complex.

#### Johan Commelin (Mar 09 2021 at 15:24):

So the code about shifts of cochain complexes is currently commented out

#### Johan Commelin (Mar 09 2021 at 15:25):

We might want to build a generic constructor for functors to complex_like by taking a functor to differential_object, + a proof that all objects in the image are is_complex_like.

#### Johan Commelin (Mar 11 2021 at 16:23):

I think that the API for soft_truncation' is almost done

#### Johan Commelin (Mar 11 2021 at 16:24):

To prove that it is well-behaved wrt weak bounded exactness, there is 1 sorry left.

#### Johan Commelin (Mar 11 2021 at 16:25):

We need to do a computation with a cokernel, and it's a bit nasty because the range of d is maybe not closed, so we have to work with norm estimates.

#### Johan Commelin (Mar 11 2021 at 16:25):

If someone wants to take a look, please feel free to fix that sorry

#### Johan Commelin (Mar 11 2021 at 17:15):

I changed the sorry into something that I'm convinced is provable.

Last updated: May 09 2021 at 15:11 UTC