## Stream: new members

### Topic: Coercion brackets

#### 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!

#### 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.

#### Kevin Buzzard (Jul 21 2020 at 18:15):

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


gives you the behaviour you want.

#### 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