Zulip Chat Archive

Stream: condensed mathematics

Topic: soft_truncation'


view this post on Zulip Johan Commelin (Mar 03 2021 at 19:29):

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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 19:42):

Good! I hope this will not take too much

view this post on Zulip 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?

view this post on Zulip 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 []

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Mar 03 2021 at 20:15):

This must be in mathlib right?

view this post on Zulip Heather Macbeth (Mar 03 2021 at 20:23):

For the submodule version, docs#submodule.topological_closure

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 03 2021 at 20:30):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Mar 03 2021 at 20:31):

Adam Topaz said:

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.

view this post on Zulip Adam Topaz (Mar 03 2021 at 20:31):

Oh right, okay.

view this post on Zulip 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⟩,
  ..quotient_add_group.mk' S }

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:12):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:23):

Maybe we should introduce closed_add_subgroup extending add_subgroup?

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 21:25):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:26):

Yes that's right

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:27):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:28):

There is even a Galois insertion between the two!

view this post on Zulip 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 (λ ε , _),
    obtain N, hN := exists_nat_ge ε⁻¹,
    have Npos := lt_of_lt_of_le (inv_pos.mpr ) hN,
    replace hN := (inv_le_inv Npos (inv_pos.mpr )).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,
  simp only [zero_add, add_neg_cancel_comm] at 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

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:34):

Which branch is this in?

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 21:34):

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

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 21:35):

That is now written with [complete_space S]

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 21:36):

OK, I pushed to quotient_closed

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 21:40):

Done

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:40):

Got it! Thanks :)

view this post on Zulip Heather Macbeth (Mar 03 2021 at 21:46):

Adam Topaz said:

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.

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:50):

We can always use fact (is_closed _)

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:55):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Adam Topaz (Mar 03 2021 at 22:54):

Yes, this all sounds very reasonable.

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:00):

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

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 23:03):

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

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:06):

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

view this post on Zulip 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 c0c_0 to itself sending (xi)(x_i) to (i1xi)(i^{-1}x_i).

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:14):

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

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:14):

I just want the image as a normed group

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:14):

no closedness assumptions for now.

view this post on Zulip Heather Macbeth (Mar 03 2021 at 23:14):

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

view this post on Zulip 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 :)

view this post on Zulip Heather Macbeth (Mar 03 2021 at 23:16):

Oh, normed_group vs NormedGroup :)

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:16):

And I want an actual has_images instance for NormedGroup as well

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 03 2021 at 23:30):

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

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:31):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 03 2021 at 23:33):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 23:36):

I have the impression that the kernel and cokernel always exist

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:36):

Which should be correct.

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:37):

This is the more general defn of images:
https://ncatlab.org/nlab/show/image

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:37):

(which agrees with docs#category_theory.limits.has_images )

view this post on Zulip Riccardo Brasca (Mar 03 2021 at 23:38):

normedgroup is probably {pre,semi}abelian, or something like that

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 03 2021 at 23:45):

Yes, I completely agree with that :)

view this post on Zulip 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 $
  quotient_add_group.quotient f.range.topological_closure

@[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,
  ..(quotient_add_group.lift _ g.to_add_monoid_hom begin
    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.

view this post on Zulip Johan Commelin (Mar 04 2021 at 05:17):

Thanks for all the work!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 11:01):

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

view this post on Zulip Johan Commelin (Mar 04 2021 at 11:02):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Mar 04 2021 at 12:32):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 13:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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,
  ..(quotient_add_group.lift _ g.to_add_monoid_hom begin
    intros b hb,
    sorry,
  end ) }

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 14:17):

I've added lift here

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:20):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:20):

give me a few mins

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:34):

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

view this post on Zulip Johan Commelin (Mar 04 2021 at 14:40):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:40):

4sho

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:40):

Oh, I pushed it.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:45):

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

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 14:47):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:47):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:47):

I can't find it in the branch

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 14:51):

I've added lift_mk

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 14:51):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:52):

Ok, I'll add lift_unique

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:53):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 04 2021 at 14:59):

Allright, I added lift_unque

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:00):

So now we have cokernels

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:04):

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

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 15:04):

No problem for me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:06):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:10):

I think you need the assumption that it's normal

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:11):

docs#quotient_group.quotient.group

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 04 2021 at 15:12):

And probably less work from now.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 15:13):

Sure!

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:38):

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

view this post on Zulip Johan Commelin (Mar 04 2021 at 15:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 04 2021 at 15:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 04 2021 at 15:59):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:10):

Merci!

view this post on Zulip 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 :(

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:15):

I'll have dinner first

view this post on Zulip Adam Topaz (Mar 04 2021 at 16:16):

Want to meet on video later?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:50):

Adam Topaz said:

Want to meet on video later?

I can probably meet around

view this post on Zulip Adam Topaz (Mar 04 2021 at 16:50):

What time zone is that?

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:51):

I'm using <time

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:51):

So Zulip turns it into your timezone

view this post on Zulip Adam Topaz (Mar 04 2021 at 16:51):

Fancy!

view this post on Zulip Adam Topaz (Mar 04 2021 at 16:51):

That works :)

view this post on Zulip Johan Commelin (Mar 04 2021 at 16:51):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Mar 04 2021 at 17:43):

@Adam Topaz I'm ready half an hour early

view this post on Zulip Johan Commelin (Mar 04 2021 at 17:44):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 04 2021 at 22:31):

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

view this post on Zulip Adam Topaz (Mar 04 2021 at 22:32):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 04 2021 at 23:42):

Fine with me!

view this post on Zulip Riccardo Brasca (Mar 04 2021 at 23:46):

Pushed to master

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Mar 04 2021 at 23:56):

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

view this post on Zulip Adam Topaz (Mar 05 2021 at 00:05):

Okay, I'm fixing it.

view this post on Zulip Adam Topaz (Mar 05 2021 at 00:05):

And adding some docstrings to make the linter happy

view this post on Zulip Adam Topaz (Mar 05 2021 at 00:08):

Shhould be okay now

view this post on Zulip Sebastien Gouezel (Mar 05 2021 at 08:53):

Adam Topaz said:

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.

view this post on Zulip Johan Commelin (Mar 05 2021 at 08:54):

of mathlib, or LTE?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 09 2021 at 07:12):

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

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:12):

we are only shifting left

view this post on Zulip Johan Commelin (Mar 09 2021 at 07:13):

and then truncating whatever got moved into negative degrees

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:44):

We need both to be additive, right?

view this post on Zulip Adam Topaz (Mar 09 2021 at 08:44):

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

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:45):

Hmm, makes sense

view this post on Zulip Johan Commelin (Mar 09 2021 at 08:45):

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

view this post on Zulip Adam Topaz (Mar 09 2021 at 08:45):

Yeah.

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip 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

view this post on Zulip Adam Topaz (Mar 09 2021 at 15:08):

I'm adding the preadditive instance now.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:16):

@Adam Topaz one sec!

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:16):

I already did that

view this post on Zulip Adam Topaz (Mar 09 2021 at 15:17):

Oh :)

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:17):

let me push what I have

view this post on Zulip Adam Topaz (Mar 09 2021 at 15:17):

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

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:17):

See jmc-refactor-complex branch

view this post on Zulip Adam Topaz (Mar 09 2021 at 15:17):

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

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:18):

Thinks work a lot smoother now. Even less eq_to_homs

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:20):

@Adam Topaz ok, it builds locally

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 09 2021 at 15:24):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 11 2021 at 16:23):

I think that the API for soft_truncation' is almost done

view this post on Zulip Johan Commelin (Mar 11 2021 at 16:24):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 11 2021 at 16:25):

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

view this post on Zulip 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