# Zulip Chat Archive

## Stream: general

### Topic: invalid 'calc': transitivity rule

#### Kenny Lau (Apr 16 2018 at 01:50):

invalid 'calc' expression, transitivity rule is not defined for current step

#### Kenny Lau (Apr 16 2018 at 01:51):

I am using `≃`

in `calc`

as in here

#### Kenny Lau (Apr 16 2018 at 01:51):

why does it give me this error?

#### Kenny Lau (Apr 16 2018 at 01:51):

mathlib:

lemma group_equiv_left_cosets_times_subgroup {s : set α} (hs : is_subgroup s) : nonempty (α ≃ (left_cosets s × s)) := ⟨calc α ≃ (@set.univ α) : (equiv.set.univ α).symm ... ≃ (⋃t∈left_cosets s, t) : by rw [←hs.Union_left_cosets_eq_univ]; simp ... ≃ (Σt:left_cosets s, t) : equiv.set.bUnion_eq_sigma_of_disjoint hs.pairwise_left_cosets_disjoint ... ≃ (Σt:left_cosets s, s) : equiv.sigma_congr_right $ λ⟨t, ht⟩, classical.choice $ hs.left_cosets_equiv_subgroup ht ... ≃ (left_cosets s × s) : equiv.sigma_equiv_prod _ _⟩

#### Kenny Lau (Apr 16 2018 at 01:51):

why can mathlib use it but gives me error when I use it

#### Kenny Lau (Apr 16 2018 at 02:00):

oh my god

#### Kenny Lau (Apr 16 2018 at 02:01):

it is a totally unrelated error caused by `≃`

having higher priority than `×`

#### Mario Carneiro (Apr 16 2018 at 02:02):

the priority of ≃ is a bit dumb, I know

#### Mario Carneiro (Apr 16 2018 at 02:03):

but it's hard to be both equality like and also lower than most type operators

#### Kenny Lau (Apr 16 2018 at 02:03):

theorem orbit_stab : nonempty ((orbit G X x × stab G X x) ≃ G) := nonempty.elim (orbit_equiv_stab_cosets G X x) $ λ F1, nonempty.elim (is_subgroup.group_equiv_left_cosets_times_subgroup $ stab.is_subgroup G X x) $ λ F2, nonempty.intro $ (equiv.prod_congr F1 (equiv.refl $ stab G X x)).trans F2.symm

#### Kenny Lau (Apr 16 2018 at 02:03):

orbit-stabilizer theorem done :D

#### Mario Carneiro (Apr 16 2018 at 02:04):

does it have to be `nonempty`

? Can't you give the equiv itself?

#### Kenny Lau (Apr 16 2018 at 02:04):

ask `group_equiv_left_cosets_times_subgroup`

#### Kenny Lau (Apr 16 2018 at 02:04):

https://github.com/leanprover/mathlib/blob/master/group_theory/coset.lean#L146

#### Kenny Lau (Apr 16 2018 at 02:05):

hey `group_equiv_left_cosets_times_subgroup`

, why are you nonempty?

#### Mario Carneiro (Apr 16 2018 at 02:05):

probably because of the choice in the middle

#### Mario Carneiro (Apr 16 2018 at 02:06):

you can't constructively pick an element from each coset

#### Kenny Lau (Apr 16 2018 at 02:06):

I see

#### Mario Carneiro (Apr 16 2018 at 02:06):

does that generalize to your theorem?

#### Kenny Lau (Apr 16 2018 at 02:07):

well I used that theorem so it has to be nonempty

#### Mario Carneiro (Apr 16 2018 at 02:09):

Maybe your application is constructive though

#### Kenny Lau (Apr 16 2018 at 02:10):

well then it is `noncomputable def`

at most?

#### Kenny Lau (Apr 16 2018 at 02:10):

don't quite see the difference between that and just `nonempty`

#### Mario Carneiro (Apr 16 2018 at 02:10):

I think `orbit_equiv_stab_cosets`

gives you a way to select an element from each coset

#### Mario Carneiro (Apr 16 2018 at 02:10):

I think it is computable

#### Kenny Lau (Apr 16 2018 at 02:11):

that one isn't computable either

#### Kenny Lau (Apr 16 2018 at 02:11):

there's no computable inverse

#### Kenny Lau (Apr 16 2018 at 02:11):

I am not using quotient

#### Mario Carneiro (Apr 16 2018 at 02:11):

Maybe the problem is that you have to deal with cosets then

#### Kenny Lau (Apr 16 2018 at 02:12):

well maybe https://github.com/leanprover/mathlib/blob/master/group_theory/coset.lean could use quotients instead of sets

#### Kenny Lau (Apr 16 2018 at 02:12):

then our lives will be easier

#### Kenny Lau (Apr 16 2018 at 02:12):

they even have the equivalence relation set up

#### Mario Carneiro (Apr 16 2018 at 02:17):

I think you are right...

#### Kevin Buzzard (Apr 16 2018 at 06:44):

You need the axiom of choice to pick coset representatives, i.e. if G is a group (even an abelian group) and H is a subgroup then you need the axiom of choice to choose a subset S of G containing precisely one element of each coset. One perhaps rather convoluted way of seeing this is that if G is the reals and H the rationals then if you can choose S then you can build a non-measurable subset of the reals; however there is a model of ZF (no C) in which every set is measurable.

#### Kevin Buzzard (Apr 16 2018 at 06:46):

Apply this to the action of G on the cosets of H and you see that an explicit bijection would give you S, you look at the image of (orbit x {1})

#### Kenny Lau (Apr 16 2018 at 06:47):

what is this a response to?

#### Mario Carneiro (Apr 16 2018 at 06:50):

I think he is arguing that the orbit stabilizer theorem is also necessarily nonconstructive (in the infinite case)

#### Kevin Buzzard (Apr 16 2018 at 06:51):

does it have to be

`nonempty`

? Can't you give the equiv itself?

#### Kenny Lau (Apr 16 2018 at 06:52):

it's nonconstructive, but can't we use noncomputable def instead of nonempty

#### Kevin Buzzard (Apr 16 2018 at 06:55):

I'm not sure I understand the question yet. I think that out of everyone in this conversation I'm the least well placed to answer it anyway. I just wanted to tell you (Kenny) the argument I came up with yesterday which convinced me that some form of nonconstructive maths was provably needed to choose coset reps.

#### Kenny Lau (Apr 16 2018 at 06:57):

we three all agree with that

#### Mario Carneiro (Apr 16 2018 at 07:06):

You can always extract an equiv from a nonempty equiv using `choice`

, which makes it a noncomputable def. Doing this before or after makes little difference

#### Kevin Buzzard (Apr 16 2018 at 07:07):

we three all agree with that

yes, but I gave a proof ;-)

#### Patrick Massot (Apr 16 2018 at 07:28):

It's a complete mystery to me: why mathlib doesn't use a quotient to talk about quotient of a group by a (non-normal) subgroup?

#### Kenny Lau (Apr 16 2018 at 07:28):

well "mathlib" isn't a person

#### Kenny Lau (Apr 16 2018 at 07:29):

and the person you seek is @Scott Morrison

#### Kenny Lau (Apr 16 2018 at 07:29):

and this thing is just here 5 days ago

#### Patrick Massot (Apr 16 2018 at 07:29):

I'm sure it's older

#### Patrick Massot (Apr 16 2018 at 07:29):

When Johannes proved Lagrange

#### Kenny Lau (Apr 16 2018 at 07:30):

nvm what i said is bs

#### Kenny Lau (Apr 16 2018 at 07:30):

right, @Johannes Hölzl proved it in March 6

#### Johannes Hölzl (Apr 16 2018 at 07:35):

The answer is simple: I didn't think about quotients of a group to prove Lagrange. I just wanted to show a property about the orbit of a group.

#### Patrick Massot (Apr 16 2018 at 07:52):

But the orbit of a point is canonically the quotient of the group by the stabilizer of the point

#### Kenny Lau (Apr 16 2018 at 07:52):

cardinalities don't interact well with quotients

#### Patrick Massot (Apr 16 2018 at 07:53):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC