Zulip Chat Archive

Stream: general

Topic: invalid 'calc': transitivity rule


view this post on Zulip Kenny Lau (Apr 16 2018 at 01:50):

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:51):

I am using in calc as in here

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:51):

why does it give me this error?

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:51):

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:00):

oh my god

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:01):

it is a totally unrelated error caused by having higher priority than ×

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:02):

the priority of ≃ is a bit dumb, I know

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:03):

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

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:03):

orbit-stabilizer theorem done :D

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:04):

does it have to be nonempty? Can't you give the equiv itself?

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:04):

ask group_equiv_left_cosets_times_subgroup

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:04):

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:05):

hey group_equiv_left_cosets_times_subgroup, why are you nonempty?

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:05):

probably because of the choice in the middle

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:06):

you can't constructively pick an element from each coset

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:06):

I see

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:06):

does that generalize to your theorem?

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:07):

well I used that theorem so it has to be nonempty

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:09):

Maybe your application is constructive though

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:10):

well then it is noncomputable def at most?

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:10):

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

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

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:10):

I think it is computable

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:11):

that one isn't computable either

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:11):

there's no computable inverse

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:11):

I am not using quotient

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:11):

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

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:12):

then our lives will be easier

view this post on Zulip Kenny Lau (Apr 16 2018 at 02:12):

they even have the equivalence relation set up

view this post on Zulip Mario Carneiro (Apr 16 2018 at 02:17):

I think you are right...

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

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 06:47):

what is this a response to?

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 06:51):

does it have to be nonempty? Can't you give the equiv itself?

view this post on Zulip Kenny Lau (Apr 16 2018 at 06:52):

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

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 06:57):

we three all agree with that

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

view this post on Zulip Kevin Buzzard (Apr 16 2018 at 07:07):

we three all agree with that

yes, but I gave a proof ;-)

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:28):

well "mathlib" isn't a person

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:29):

and the person you seek is @Scott Morrison

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:29):

and this thing is just here 5 days ago

view this post on Zulip Patrick Massot (Apr 16 2018 at 07:29):

I'm sure it's older

view this post on Zulip Patrick Massot (Apr 16 2018 at 07:29):

When Johannes proved Lagrange

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:30):

nvm what i said is bs

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:30):

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

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

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

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:52):

cardinalities don't interact well with quotients

view this post on Zulip Patrick Massot (Apr 16 2018 at 07:53):

(deleted)


Last updated: May 11 2021 at 14:11 UTC