Zulip Chat Archive

Stream: maths

Topic: new is_group_hom


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:14):

I already complained about this :P

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:14):

I'm not really complaining

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:15):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:18):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:21):

but what is conj_is_mph?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:22):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:24):

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

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:24):

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

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:24):

But trying to move stuff always gets Lean to go crazy

view this post on Zulip Patrick Massot (Apr 16 2018 at 15:25):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:28):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 16 2018 at 15:30):

right, which I demonstrated


Last updated: May 06 2021 at 19:30 UTC