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

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

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: May 11 2021 at 14:11 UTC