Zulip Chat Archive

Stream: new members

Topic: Coercion brackets


view this post on Zulip Jason KY. (Jul 21 2020 at 18:03):

I'm trying to define quotient groups through congruence and I'm a bit stuck on the following

import group_theory.congruence

variables {G : Type} [group G]

namespace group_con

structure group_con (G : Type) [group G] extends con G :=
(inv' :  {x y}, r x y  r x⁻¹ y⁻¹)

instance has_coe_to_setoid : has_coe (group_con G) (setoid G) :=
  ⟨λ R, R.to_con.to_setoid

instance : has_coe_to_fun (group_con G) := ⟨_, λ R, λ x y, R.r x y

lemma mul {R : group_con G} {x₀ x₁ y₀ y₁ : G} :
  R x₀ x₁  R y₀ y₁  R (x₀ * y₀) (x₁ * y₁) := by apply R.mul'

lemma inv {R : group_con G} {x y : G} : R x y  R x⁻¹ y⁻¹ := by apply R.inv'

def quotient (R : group_con G) := quotient (R : setoid G)

variables {R : group_con G}

instance : has_coe_t G (quotient R) := quotient.mk'

lemma eq {x y : G} : (x  : quotient R) = y  R x y := quotient.eq'

def lift_on {β} {R : group_con G} (x : quotient R) (f : G  β)
  (h :  x y, R x y  f x = f y) : β := quotient.lift_on' x f h

def lift_on₂ {β} {R : group_con G} (x y : quotient R) (f : G  G  β)
  (h :  a₁ a₂ b₁ b₂, R a₁ b₁  R a₂ b₂  f a₁ a₂ = f b₁ b₂) : β :=
quotient.lift_on₂' x y f h

instance : has_mul (quotient R) :=
{ mul := λ x y, lift_on₂ x y (λ x y , ((x * y : G) : quotient R))
    $ λ _ _ _ _ h₁ h₂, eq.2 (mul h₁ h₂) }

instance : has_inv (quotient R) :=
  ⟨λ x, lift_on x (λ x, ((x⁻¹ : G) : quotient R)) $ λ _ _ h, eq.2 (inv h)

instance : has_one (quotient R) := ((1 : G) : quotient R)

lemma coe     (x : G)   : quotient.mk' x = (x : quotient R) := rfl
lemma coe_mul (x y : G) : (x : quotient R) * y = ((x * y : G) : quotient R) := rfl
lemma coe_inv (x : G)   : (x : quotient R)⁻¹ = (x⁻¹ : quotient R) := rfl
lemma coe_one           : 1 = ((1 : G) : quotient R) := rfl

lemma mul_left_inv' {a : quotient R} : a⁻¹ * a = 1 :=
begin
  apply quotient.induction_on' a,
  intro x, rw [coe],
  show ((x⁻¹) : quotient R) * x = 1,
  -- why does it show (↑x)⁻¹ * ↑x = 1 and not ↑(x⁻¹) * ↑x = 1 ?
  sorry
end

end group_con

As the comment indicates, why is the lean goal (↑x)⁻¹ * ↑x = 1 and not ↑(x⁻¹) * ↑x = 1. My original intention was to rw coe_inv but that doesn't work either.

Sorry for such a long mwe, any help appreciated!

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 18:15):

This sort of thing used to confuse me too. Someone will say "lean reads from left to right" or "lean expands from the outside in" or some such buzz phrase which helps some people but never helps me. But I do know the answer. When Lean sees ((x⁻¹) : quotient R) it unfolds it to has_inv.inv x : quotient R and then it decides which has_inv.inv to use. Because the answer is supposed to be in quotient R it decides to use the inverse on quotient R. And then it looks at which element of quotient R it's supposed to be inversing, and it finds something which isn't in quotient R, so it coerces it there.

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 18:15):

  show ((x⁻¹ : G) : quotient R) * x = 1,

gives you the behaviour you want.

view this post on Zulip Jason KY. (Jul 21 2020 at 18:21):

Ah! That makes a lot of sense, thanks!


Last updated: May 11 2021 at 12:15 UTC