# Zulip Chat Archive

## Stream: maths

### Topic: separated quotient

#### Patrick Massot (Sep 30 2018 at 20:18):

@Johannes Hölzl why https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L185 is not an instance?

#### Patrick Massot (Sep 30 2018 at 20:19):

Oh! Why this completeness assumption?!

#### Patrick Massot (Sep 30 2018 at 20:20):

I love doing that with Lean: I removed the assumption and the proof still compiles!

#### Johannes Hölzl (Sep 30 2018 at 20:39):

yeah should be instance

#### Kevin Buzzard (Sep 30 2018 at 20:44):

Yeah for removing assumptions. You remove them in real life and then have to understand the proof all over again

#### Patrick Massot (Sep 30 2018 at 20:44):

exactly

#### Patrick Massot (Sep 30 2018 at 20:58):

I just noticed while reviewing my work that this unneeded assumption is simply copy-paste from the previous lemma (where it *is* needed).

#### Patrick Massot (Sep 30 2018 at 21:01):

Anyway, @Johannes Hölzl please have a look at https://github.com/leanprover-community/mathlib/commit/cfb60c52739921a0a9b36bbe2a73400dc2fc372a

#### Patrick Massot (Sep 30 2018 at 21:02):

The nonempty quotient stuff will have to move to its proper place but I don't have courage right now (it means recompiling all mathlib since the proper place is very low in the tree).

#### Patrick Massot (Sep 30 2018 at 21:03):

Kevin: this commit is still work towards ring completions. It's preparation for the isomorphism from `completion (separation_quotient a)`

to `completion a`

.

#### Patrick Massot (Sep 30 2018 at 21:05):

We're getting really close. We may have ring completion tomorrow if I can hide from my secretary and from the head of my department. But first I need to sleep.

#### Patrick Massot (Oct 01 2018 at 07:08):

@Johannes Hölzl I just noticed that some lemmas from my versions of uniform spaces completions didn't make it through your refactoring. In particular https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L266-L267 and https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean#L274 (I realized I forgot the analogue of the last one for the separation quotient yesterday). Is it on purpose? From a categorical point of view they are crucial.

#### Johannes Hölzl (Oct 01 2018 at 07:40):

sorry, both got lost. I will add them

#### Patrick Massot (Oct 01 2018 at 08:36):

It's ok, I can add them back

#### Patrick Massot (Oct 01 2018 at 08:44):

Just to make sure: Johannes, are you working on this?

#### Johannes Hölzl (Oct 01 2018 at 08:47):

Not yet, I wanted to start now. Do you have some changes?

#### Patrick Massot (Oct 01 2018 at 08:48):

No, I was about to start :smile:

#### Patrick Massot (Oct 01 2018 at 08:48):

I'll let you do this, and work on the next steps

#### Johannes Hölzl (Oct 01 2018 at 08:48):

okay

#### Patrick Massot (Oct 01 2018 at 08:49):

Did you pull what I did yesterday?

#### Johannes Hölzl (Oct 01 2018 at 08:49):

One thing I will also change: remove `is_ideal'`

. I don't think it is necessary.

#### Johannes Hölzl (Oct 01 2018 at 08:49):

yes, i just pulled

#### Patrick Massot (Oct 01 2018 at 08:49):

Fine. I was worried that nobody reacted to this `is_ideal'`

#### Patrick Massot (Oct 01 2018 at 08:50):

But I hope the topology proof won't become ugly

#### Johannes Hölzl (Oct 01 2018 at 08:52):

I hope so, too. That's why I plan to remove it again. If it gets ugly I will add a "constructor" function for `is_ideal`

instead of the additional structure

#### Patrick Massot (Oct 01 2018 at 08:52):

Ok, great. I'll stop asking questions and let you work then

#### Johannes Hölzl (Oct 01 2018 at 11:27):

So I restructured a little bit and replaced the proof for `is_ideal (closure _)`

, by adding nicer rules for membership in `closure`

.

#### Patrick Massot (Oct 01 2018 at 11:28):

I see you pushed while I was writing a link to the previous version :)

#### Johannes Hölzl (Oct 01 2018 at 11:30):

Hehe good. I guess you want to work now on the ring completion without assuming Hausdorff?

#### Patrick Massot (Oct 01 2018 at 11:31):

Yes, and then you'll have the pleasure to refactor it

#### Johannes Hölzl (Oct 01 2018 at 11:32):

No problem. I'm sure it will be in a good state!

#### Patrick Massot (Oct 01 2018 at 11:33):

I'm a bit sad that the proof of `ideal_closure`

is no unrecognizable for mathematicians

#### Patrick Massot (Oct 01 2018 at 11:33):

I don't know why you and Mario don't like equalities between functions.

#### Patrick Massot (Oct 01 2018 at 11:34):

It's really going against main stream mathematics to replace function equality with elements equality everywhere

#### Johannes Hölzl (Oct 01 2018 at 11:34):

No I'm confused. I think it is much more readable than before. We state what kind of steps we proof (is it the zero, add, or mul case) and we say how we proof the membership in the `closure`

. Before it was just a sequence of tactics, not mentioning which case is proved.

#### Patrick Massot (Oct 01 2018 at 11:35):

Category theory tells us that elements are confusing, only arrows matter

#### Patrick Massot (Oct 01 2018 at 11:36):

I agree that stating which case we are proving is nice. What I'm talking about is hiding that the proof key is `image_closure_subset_closure_image`

#### Patrick Massot (Oct 01 2018 at 11:36):

that you've hidden in `mem_closure`

#### Patrick Massot (Oct 01 2018 at 11:37):

also that name is much harder to find than image_closure_subset_closure_image

#### Johannes Hölzl (Oct 01 2018 at 12:07):

why is it harder to find? You ask, "is there anything to prove membership in `closure`

" then you find it. if you ask: is there anything w.r.t. subset of closure you don't find it. But both are valid. Your proof might be more categorical. But only halfway, you proof something about subsets, not about arrows. You still use `closure_mono`

, instead of arguing about an mono-homomorphism into another type.

#### Johannes Hölzl (Oct 01 2018 at 12:08):

`closure`

is very set based, so for me it doesn't make sense to argue about arrows.

#### Patrick Massot (Oct 01 2018 at 13:37):

No problem. I'm sure it will be in a good state!

@Johannes Hölzl it's your turn: https://github.com/leanprover-community/mathlib/commit/b0592fe97e74ef4e9af8158052d30053914d639b

#### Patrick Massot (Oct 01 2018 at 13:37):

I'm sure you'll find better names :wink:

#### Kevin Buzzard (Oct 01 2018 at 14:45):

I find these conversations very interesting. Patrick is absolutely right from a mathematical point of view. Grothendieck stressed that the arrows were more important than the objects. People talked about geometric objects being smooth but Grothendieck argued that the correct definition was that of a map being smooth, and an object being smooth just meant that the map from this object to the one point set was smooth. On the other hand Johannes thinks about mathematics in a completely different way. Do people properly understand how Grothendieck's ideas should influence type theory?

#### Patrick Massot (Oct 01 2018 at 19:02):

Hum, I built a ring structure on the separation quotient of a topological ring, but forgot to prove that it's a *topological* ring

#### Patrick Massot (Oct 01 2018 at 19:02):

I'll need that projection on a quotient group is open

#### Patrick Massot (Oct 01 2018 at 19:03):

Do we have open maps in mathlib?

#### Reid Barton (Oct 01 2018 at 19:05):

Don't think so, there's `embedding_open`

I think which says that an embedding of an open subspace is an open map, but just spelled out explicitly.

#### Patrick Massot (Oct 01 2018 at 19:06):

I'm not sure how to get back the fact that addition on a group quotient group is defined by `quotient.lift`

. Should I `dunfold`

until I see it or is there a better way?

#### Chris Hughes (Oct 01 2018 at 19:24):

use `show`

#### Johannes Hölzl (Oct 01 2018 at 19:26):

`dsimp`

could also help.

#### Patrick Massot (Oct 01 2018 at 19:31):

I'm completely lost in our maze of quotient structures. Do we have the quotient of a commutative additive group by a subgroup? Is it related in anyway with quotient rings? Or should I be doing topological modules?

#### Johannes Hölzl (Oct 01 2018 at 19:35):

`quotient_add_group.add_group`

(https://github.com/leanprover/mathlib/blob/master/group_theory/quotient_group.lean#L46)

is for normal subgroups, but as far as I understand a normal subgroup is just a subgroup in the commutative case?

#### Patrick Massot (Oct 01 2018 at 19:35):

yes, every group is normal in this case

#### Johannes Hölzl (Oct 01 2018 at 19:38):

so you can use `quotient_add_group`

?

#### Johannes Hölzl (Oct 01 2018 at 19:39):

Ah there is also `quotient_add_group.add_comm_group`

it is just not setup as an `instance`

#### Patrick Massot (Oct 01 2018 at 19:40):

What about https://github.com/leanprover/mathlib/blob/master/group_theory/quotient_group.lean#L53?

#### Patrick Massot (Oct 01 2018 at 19:41):

It looks good but I haven't managed to use it yet

#### Johannes Hölzl (Oct 01 2018 at 19:46):

Yes, that's it, but the multiplicative version. Afterwards the additive version is derived (line 63). But for the additive version the instance attribute is missing

#### Patrick Massot (Oct 01 2018 at 19:46):

Oh

#### Patrick Massot (Oct 01 2018 at 19:52):

Now it seems to work without the attribute, strange...

#### Johannes Hölzl (Oct 01 2018 at 19:57):

maybe its somewhere else?

#### Patrick Massot (Oct 01 2018 at 20:00):

I need to stop for today, but at least I have some statement:

import analysis.topology.topological_structures variables {α : Type*} [add_comm_group α] [topological_space α] instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_space (quotient_add_group.quotient N) := by dunfold quotient_add_group.quotient ; apply_instance instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_add_group (quotient_add_group.quotient N) := { continuous_add := sorry, continuous_neg := sorry}

#### Patrick Massot (Oct 01 2018 at 20:01):

I wasn't able to get to the point where I can simply use continuity of lifts of continuous functions

#### Johannes Hölzl (Oct 02 2018 at 07:53):

@Patrick Massot fyi, I rebased the branch. So pull the new branch before continuing on it.

#### Patrick Massot (Oct 03 2018 at 16:08):

I tried to return to this topological quotient group, but I still have no idea how to unfold the definition of addition on the quotient. It uses a mysterious `quotient.lift_on2'`

that I can't reach, even using change. The MWE is:

import analysis.topology.topological_structures import group_theory.quotient_group variables {α : Type*} [add_comm_group α] [topological_space α] [topological_add_group α] (N : set α) [is_add_subgroup N] instance [topological_add_group α] (N : set α) [is_add_subgroup N]: topological_space (quotient_add_group.quotient N) := by dunfold quotient_add_group.quotient ; apply_instance instance : topological_add_group (quotient_add_group.quotient N) := { continuous_add := sorry, continuous_neg := sorry}

#### Johan Commelin (Oct 03 2018 at 16:23):

@Patrick Massot Do you have a strategy in mind?

#### Johan Commelin (Oct 03 2018 at 16:23):

Which ingredients would you want to apply?

#### Johan Commelin (Oct 03 2018 at 16:25):

My guess would be that you first need to turn the addition into a map `quot × quot → quot`

, then identify `quot × quot`

with an appropriate quotient. And then apply some lemma about the universal property of quotients and continuous maps

#### Johan Commelin (Oct 03 2018 at 16:25):

Of course this is very vague...

#### Johannes Hölzl (Oct 03 2018 at 16:36):

So, `quotient.lift_on2'`

is just `quotient.lift_on2`

using a implicit parameter instead of a type class parameter. If this helps...

#### Reid Barton (Oct 03 2018 at 17:22):

I think the math strategy is to start with a commutative square involving the multiplication $G \times G \to G$ and the multiplication $G/H \times G/H \to G/H$. Right?

#### Reid Barton (Oct 03 2018 at 17:24):

Where the vertical maps are $q \times q$ and $q$ where $q : G \to G/H$ is the quotient map. I think the fact that that square commutes is a definitional equality (for each pair $(g_1, g_2) \in G \times G$). So you should not have to unfold the definition of the product in $G/H$ if that is correct.

#### Chris Hughes (Oct 03 2018 at 17:27):

@Patrick Massot the fact that `quotient_group.mk`

is a `group_hom`

should mean that you don't need to unfold mul. The proof that it is a `group_hom`

is just `rfl`

anyway, so everything's definitionally equal to what you want it to be.

#### Reid Barton (Oct 03 2018 at 17:31):

The point is that the multiplication on the quotient is ultimately defined in terms of `quot.lift`

, and `quot.lift`

applied to something made from `quot.mk`

reduces.

#### Johan Commelin (Oct 03 2018 at 17:36):

Ok, so first of all we need to know that the quotient map is ctu. Is this already there?

#### Reid Barton (Oct 03 2018 at 17:43):

Assuming "ctu" = continuous then `continuous_quot_mk`

#### Reid Barton (Oct 03 2018 at 17:46):

By the way, this one is not simply a formal consequence of the universal property of the quotient, because the product of two quotient maps is not in general a quotient map (although in this case I guess it probably is)

#### Reid Barton (Oct 03 2018 at 17:46):

For `continuous_neg`

, you can argue along those lines.

#### Patrick Massot (Oct 03 2018 at 18:41):

Sorry, I was away. Indeed the quotient projection is continuous, and addition is continuous, so I want to use https://github.com/leanprover/mathlib/blob/c1f9f2e2977c0f6cb1cfd949bee8c3817cce0489/analysis/topology/continuity.lean#L811 applied to quotient.mk \circ addition. My problem is to get Lean to swallow that

#### Patrick Massot (Oct 03 2018 at 18:47):

oh maybe I misunderstood. Do you mean I could use https://github.com/leanprover/mathlib/blob/c1f9f2e2977c0f6cb1cfd949bee8c3817cce0489/analysis/topology/continuity.lean#L383?

#### Patrick Massot (Oct 03 2018 at 18:48):

lemma quotient_map.continuous_iff {f : α → β} {g : β → γ} (hf : quotient_map f) : continuous g ↔ continuous (g ∘ f)

#### Patrick Massot (Oct 03 2018 at 18:50):

I'm waiting for mathlib to compile...

#### Chris Hughes (Oct 03 2018 at 18:55):

Is `continuous_quot_mk`

the right `quot_mk`

? I see no mention of groups anywhere around it

#### Patrick Massot (Oct 03 2018 at 18:55):

The topology on the quotient group is the quotient topology (I hope)

#### Reid Barton (Oct 03 2018 at 19:21):

You can't use `continuous_quotient_lift`

or `quotient_map.continuous_iff`

because $G/H \times G/H$ is not (obviously) a quotient of $G \times G$

#### Reid Barton (Oct 03 2018 at 19:23):

I thought you were doing the proof which goes like: $q$ is an open map (because $q^{-1}(q(U))$ is a union of translates of $U$, hence open), so $q \times q$ is an open map, and then you can check that the preimage of an open subset of $G/H$ under multiplication is again open by chasing around the square

#### Patrick Massot (Oct 03 2018 at 19:25):

Indeed this is what I wanted to do the other day (I even asked whether we have a definition of open maps in mathlib) and then I forgot what I was doing...

#### Patrick Massot (Oct 03 2018 at 19:26):

But I guess the map from $G \times G$ to $G/H \times G/H$ should still be a quotient map

#### Patrick Massot (Oct 03 2018 at 19:27):

I need to think on paper

#### Patrick Massot (Oct 03 2018 at 19:53):

I decided that every proof will need to first prove that $G \to G/H$ is open anyway.

#### Kenny Lau (Oct 03 2018 at 19:55):

why do I feel like I've proved that

#### Patrick Massot (Oct 03 2018 at 19:55):

I'd be very interested

#### Patrick Massot (Oct 03 2018 at 19:55):

Do you remember if this is in mathlib?

#### Kenny Lau (Oct 03 2018 at 19:59):

def topological_group.coinduced {α : Type u} {β : Type v} [t : topological_group α] [group β] (f : α → β) [is_group_hom f] (hf1 : function.surjective f) (hf2 : ∀ S, is_open S → is_open (f ⁻¹' (f '' S))) : topological_group β :=

`hf2`

seems to say that it is an open map

#### Kenny Lau (Oct 03 2018 at 19:59):

instance quotient_group.topological_group (G : Type u) [topological_group G] (N : set G) [normal_subgroup N] : topological_group (left_cosets N) := by letI := left_rel N; from topological_group.coinduced quotient.mk quotient.exists_rep (λ S hs, have (⋃ x : {x // ⟦x⟧ = 1}, (λ y, x.1 * y) ⁻¹' S) = quotient.mk ⁻¹' (quotient.mk '' S), from set.ext $ λ z, ⟨λ ⟨S, ⟨⟨g, h1⟩, rfl⟩, h2⟩, ⟨g * z, h2, by rw [is_group_hom.mul quotient.mk, h1, one_mul]; from quotient_group.is_group_hom _⟩, λ ⟨g, h1, h2⟩, ⟨_, ⟨⟨g * z⁻¹, by rw [is_group_hom.mul quotient.mk, h2, is_group_hom.inv quotient.mk, mul_inv_self]; repeat { from quotient_group.is_group_hom _ }⟩, rfl⟩, by simp [h1]⟩⟩, this ▸ is_open_Union $ λ x : {x // ⟦x⟧ = 1}, continuous_mul continuous_const continuous_id _ hs)

so this consistutes a proof

#### Kenny Lau (Oct 03 2018 at 20:00):

#### Kenny Lau (Oct 03 2018 at 20:01):

@Patrick Massot is this what you want?

#### Patrick Massot (Oct 03 2018 at 20:01):

it looks very much like what I want

#### Kenny Lau (Oct 03 2018 at 20:02):

nice

#### Patrick Massot (Oct 03 2018 at 20:02):

I mean the statement of course

#### Kenny Lau (Oct 03 2018 at 20:02):

I mean, it's not hard to prove

#### Patrick Massot (Oct 03 2018 at 20:02):

the proof...

#### Kenny Lau (Oct 03 2018 at 20:03):

a first year could learn that

#### Patrick Massot (Oct 03 2018 at 20:03):

the math proof is easy yes

#### Patrick Massot (Oct 03 2018 at 20:04):

reading a term mode proof is hard (for me)

#### Kenny Lau (Oct 03 2018 at 20:04):

this proof is 3 months old btw

#### Patrick Massot (Oct 03 2018 at 20:06):

I will need to redo it in my context and state intermediate lemmas for reuse anyway

#### Patrick Massot (Oct 03 2018 at 20:06):

but it's still helpful to have one full proof

#### Kenny Lau (Oct 03 2018 at 20:07):

ok

#### Patrick Massot (Oct 03 2018 at 20:08):

thanks!

#### Patrick Massot (Oct 03 2018 at 20:11):

Did you think about PRing stuff from this repo?

#### Kenny Lau (Oct 03 2018 at 20:11):

maybe

#### Patrick Massot (Oct 03 2018 at 20:20):

Remember your work is lost if you don't PR it

#### Kevin Buzzard (Oct 04 2018 at 06:40):

The first key thing we need from Kenny's repo is algebraic closure, and it's not in there yet. Kenny is waiting for module refactoring because the argument needs loads of ideals over loads of rings.

#### Kevin Buzzard (Oct 04 2018 at 06:41):

After that we need to take a level-headed look at how much is appropriate for mathlib and how much really just a wacky independent project

#### Kevin Buzzard (Oct 04 2018 at 06:41):

(and I don't know what the conclusion will be)

Last updated: May 12 2021 at 08:14 UTC