## Stream: maths

### Topic: new is_group_hom

#### Patrick Massot (Apr 16 2018 at 15:14):

Recently is_group_hom became a class. Previously we had

def is_group_anti_hom (f : α → β) : Prop := ∀ a b : α, f (a * b) = f b * f a

namespace is_group_anti_hom
variables {f : α → β} (H : is_group_anti_hom f)
include H

theorem inv (a : α) : (f a)⁻¹ = f a⁻¹ := ...


and I could then write

variables {α : Type} [group α]
def conj (a b : α) := a*b*a⁻¹

lemma inv_conj : (conj b a)⁻¹ = conj b (a⁻¹) :=
conj_is_mph.inv a


Is there such a compact way to write the proof of inv_conj with the new is_group_hom? I'm not talking about the LHS/RHS switch. I'm talking about the ability to use projection notation instead of writing (is_group_hom.inv (conj b) a).symm

#### Kenny Lau (Apr 16 2018 at 15:14):

I already complained about this :P

#### Patrick Massot (Apr 16 2018 at 15:14):

I'm not really complaining

#### Kenny Lau (Apr 16 2018 at 15:15):

right, but the answer is still you can't use projection

#### Patrick Massot (Apr 16 2018 at 15:15):

I slightly prefer the old way in this case but I'm open to learning about advantages of the new way

#### Kenny Lau (Apr 16 2018 at 15:18):

Now you do is_group_hom.one f I think

#### Mario Carneiro (Apr 16 2018 at 15:20):

You should be using inv_conj in your proofs anyways, so this is a one-time cost

#### Kenny Lau (Apr 16 2018 at 15:21):

but what is conj_is_mph?

#### Patrick Massot (Apr 16 2018 at 15:21):

Hm, I didn't realize it was almost exactly the same question (I was vaguely aware of Kenny asking something about this change but didn't check)

#### Mario Carneiro (Apr 16 2018 at 15:21):

also you should probably swap inv_conj for the same reason is_group_hom.inv was swapped

#### Patrick Massot (Apr 16 2018 at 15:22):

Indeed my only use of this lemma was a rw [<-invconj]

#### Patrick Massot (Apr 16 2018 at 15:23):

I'm trying (once more...) to get back to old stuff because I hope I'll have time to resume

#### Patrick Massot (Apr 16 2018 at 15:24):

I tried to work on the pi instance PR. But I failed in the preparatory work

#### Patrick Massot (Apr 16 2018 at 15:24):

I wanted to properly dispatch the content of Johannes' prod_module.lean

#### Patrick Massot (Apr 16 2018 at 15:24):

But trying to move stuff always gets Lean to go crazy

#### Patrick Massot (Apr 16 2018 at 15:25):

everything gets frozen in VSCode and I only end up with a broken mathlib

#### Patrick Massot (Apr 16 2018 at 15:26):

Maybe I should PR everything into the prod_module black-hole and then let you or Johannes decide when this becomes a problem

#### Kenny Lau (Apr 16 2018 at 15:27):

import algebra.group

variables {α : Type} [group α] (a b : α)

def conj := a * b * a⁻¹

instance conj.is_group_hom : is_group_hom (conj a) :=
λ x y, by simp [conj, mul_assoc]

lemma inv_conj : conj a (b⁻¹) = (conj a b)⁻¹ :=
is_group_hom.inv (conj a) b


#### Kenny Lau (Apr 16 2018 at 15:28):

@Patrick Massot c'est c'que tu veux?

#### Patrick Massot (Apr 16 2018 at 15:29):

I know how to do this (except I went with by finish [is_group_hom, conj] in the instance proof. I was only asking how to properly use the new interface

#### Kenny Lau (Apr 16 2018 at 15:30):

right, which I demonstrated

Last updated: May 06 2021 at 19:30 UTC