soft_truncation'

Stream: condensed mathematics

[Johan Commelin]

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

[Johan Commelin]

@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]

Good! I hope this will not take too much

[Riccardo Brasca]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

This must be in mathlib right?

[Heather Macbeth]

For the submodule version, docs#submodule.topological_closure

[Heather Macbeth]

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

[Heather Macbeth]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Heather Macbeth]

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.

[Adam Topaz]

Oh right, okay.

[Riccardo Brasca]

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 }

[Adam Topaz]

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

[Adam Topaz]

@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]

Maybe we should introduce closed_add_subgroup extending add_subgroup?

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Adam Topaz]

Yes that's right

[Adam Topaz]

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

[Adam Topaz]

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]

There is even a Galois insertion between the two!

[Riccardo Brasca]

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,
  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

[Adam Topaz]

Which branch is this in?

[Riccardo Brasca]

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

[Adam Topaz]

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

[Riccardo Brasca]

That is now written with [complete_space S]

[Riccardo Brasca]

OK, I pushed to quotient_closed

[Adam Topaz]

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

[Riccardo Brasca]

Done

[Adam Topaz]

Got it! Thanks :)

[Heather Macbeth]

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.

[Adam Topaz]

We can always use fact (is_closed _)

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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]

Yes, this all sounds very reasonable.

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Heather Macbeth]

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]

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

[Adam Topaz]

I just want the image as a normed group

[Adam Topaz]

no closedness assumptions for now.

[Heather Macbeth]

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

[Adam Topaz]

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

[Heather Macbeth]

Oh, normed_group vs NormedGroup :)

[Adam Topaz]

And I want an actual has_images instance for NormedGroup as well

[Riccardo Brasca]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Riccardo Brasca]

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]

I have the impression that the kernel and cokernel always exist

[Adam Topaz]

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]

Which should be correct.

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Adam Topaz]

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]

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]

Yes, I completely agree with that :)

[Adam Topaz]

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.

[Johan Commelin]

Thanks for all the work!

[Adam Topaz]

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]

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

[Johan Commelin]

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

[Riccardo Brasca]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

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]

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

[Adam Topaz]

@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]

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

[Adam Topaz]

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]

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]

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]

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 ) }

[Riccardo Brasca]

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]

I've added lift here

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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

[Adam Topaz]

give me a few mins

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

4sho

[Adam Topaz]

Oh, I pushed it.

[Adam Topaz]

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]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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

[Adam Topaz]

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

[Adam Topaz]

I can't find it in the branch

[Adam Topaz]

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

[Riccardo Brasca]

I've added lift_mk

[Riccardo Brasca]

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

[Adam Topaz]

Ok, I'll add lift_unique

[Johan Commelin]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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...

[Adam Topaz]

Allright, I added lift_unque

[Johan Commelin]

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

[Adam Topaz]

So now we have cokernels

[Adam Topaz]

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

[Riccardo Brasca]

No problem for me

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Riccardo Brasca]

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]

I think you need the assumption that it's normal

[Adam Topaz]

docs#quotient_group.quotient.group

[Adam Topaz]

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]

@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]

And probably less work from now.

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Riccardo Brasca]

Sure!

[Adam Topaz]

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

[Riccardo Brasca]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Heather Macbeth]

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]

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

[Johan Commelin]

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

[Adam Topaz]

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

[Heather Macbeth]

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]

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

[Riccardo Brasca]

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

[Johan Commelin]

Merci!

[Adam Topaz]

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

[Johan Commelin]

I'll have dinner first

[Adam Topaz]

Want to meet on video later?

[Sebastien Gouezel]

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]

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]

Adam Topaz said:

Want to meet on video later?

I can probably meet around 2021-03-04T19:15:00+01:00

[Adam Topaz]

What time zone is that?

[Johan Commelin]

I'm using <time

[Johan Commelin]

So Zulip turns it into your timezone

[Adam Topaz]

Fancy!

[Adam Topaz]

That works :)

[Johan Commelin]

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

[Adam Topaz]

@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]

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]

@Adam Topaz I'm ready half an hour early

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Scott Morrison]

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]

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]

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

[Adam Topaz]

Fine with me!

[Riccardo Brasca]

Pushed to master

[Riccardo Brasca]

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]

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

[Adam Topaz]

Okay, I'm fixing it.

[Adam Topaz]

And adding some docstrings to make the linter happy

[Adam Topaz]

Shhould be okay now

[Sebastien Gouezel]

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.

[Johan Commelin]

of mathlib, or LTE?

[Kevin Buzzard]

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]

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]

@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]

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

[Johan Commelin]

we are only shifting left

[Johan Commelin]

and then truncating whatever got moved into negative degrees

[Adam Topaz]

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]

We need both to be additive, right?

[Adam Topaz]

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

[Johan Commelin]

Hmm, makes sense

[Johan Commelin]

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

[Adam Topaz]

Yeah.

[Johan Commelin]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

I'm adding the preadditive instance now.

[Johan Commelin]

@Adam Topaz one sec!

[Johan Commelin]

I already did that

[Adam Topaz]

Oh :)

[Johan Commelin]

let me push what I have

[Adam Topaz]

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

[Johan Commelin]

See jmc-refactor-complex branch

[Adam Topaz]

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

[Johan Commelin]

Thinks work a lot smoother now. Even less eq_to_homs

[Johan Commelin]

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

[Johan Commelin]

@Adam Topaz ok, it builds locally

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

I think that the API for soft_truncation' is almost done

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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