invalid 'calc': transitivity rule

Stream: general

[Kenny Lau]

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

[Kenny Lau]

I am using ≃ in calc as in here

[Kenny Lau]

why does it give me this error?

[Kenny Lau]

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]

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

[Kenny Lau]

oh my god

[Kenny Lau]

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

[Mario Carneiro]

the priority of ≃ is a bit dumb, I know

[Mario Carneiro]

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

[Kenny Lau]

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]

orbit-stabilizer theorem done :D

[Mario Carneiro]

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

[Kenny Lau]

ask group_equiv_left_cosets_times_subgroup

[Kenny Lau]

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

[Kenny Lau]

hey group_equiv_left_cosets_times_subgroup, why are you nonempty?

[Mario Carneiro]

probably because of the choice in the middle

[Mario Carneiro]

you can't constructively pick an element from each coset

[Kenny Lau]

I see

[Mario Carneiro]

does that generalize to your theorem?

[Kenny Lau]

well I used that theorem so it has to be nonempty

[Mario Carneiro]

Maybe your application is constructive though

[Kenny Lau]

well then it is noncomputable def at most?

[Kenny Lau]

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

[Mario Carneiro]

I think orbit_equiv_stab_cosets gives you a way to select an element from each coset

[Mario Carneiro]

I think it is computable

[Kenny Lau]

that one isn't computable either

[Kenny Lau]

there's no computable inverse

[Kenny Lau]

I am not using quotient

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

then our lives will be easier

[Kenny Lau]

they even have the equivalence relation set up

[Mario Carneiro]

I think you are right...

[Kevin Buzzard]

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]

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]

what is this a response to?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

we three all agree with that

[Mario Carneiro]

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]

we three all agree with that

yes, but I gave a proof ;-)

[Patrick Massot]

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]

well "mathlib" isn't a person

[Kenny Lau]

and the person you seek is @Scott Morrison

[Kenny Lau]

and this thing is just here 5 days ago

[Patrick Massot]

I'm sure it's older

[Patrick Massot]

When Johannes proved Lagrange

[Kenny Lau]

nvm what i said is bs

[Kenny Lau]

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

[Johannes Hölzl]

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]

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

[Kenny Lau]

cardinalities don't interact well with quotients

[Patrick Massot]

(deleted)