new is_group_hom

Stream: maths

[Patrick Massot]

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]

I already complained about this :P

[Patrick Massot]

I'm not really complaining

[Kenny Lau]

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

[Patrick Massot]

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

[Kenny Lau]

Now you do is_group_hom.one f I think

:point_up: https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/is_group_hom.2Emul/near/124970169

[Mario Carneiro]

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

[Kenny Lau]

but what is conj_is_mph?

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

But trying to move stuff always gets Lean to go crazy

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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]

right, which I demonstrated