Coercion brackets

Stream: new members

[Jason KY.]

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]

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]

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

gives you the behaviour you want.

[Jason KY.]

Ah! That makes a lot of sense, thanks!