Letting simp know about hom_inv_id'

Stream: new members

[Ken Lee]

I made an equiv, and I want simp to know about hom_inv_id' and inv_hom_id'. How do I do that?

def punit_UP {A : Type u} : (punit ⟶ A) ≅ A :=
{ hom := λ a, a punit.star,
  inv := λ a, λ _ , a,
  hom_inv_id' := by tidy,
  inv_hom_id' := by tidy }

[Anne Baanen]

There should probably already be simp lemmas called docs#category_theory.iso.hom_inv_id and docs#category_theory.iso.inv_hom_id.

[Mario Carneiro]

@[simps] on the definition will automatically generate lemmas about the projections and mark them as @[simp]

[Mario Carneiro]

oh but anne is right - the lemmas you want are not actually about your definition, they are true for all isos

[Mario Carneiro]

@[simps] will generate theorems like punit_UP.hom a = a punit.star

[Anne Baanen]

What do you want to do with the map? If you're planning on applying this to actual elements, it might be neater to work with docs#equiv instead of docs#category_theory.iso.

[Ken Lee]

I have a monoid instance on punit -> A, and used tactic.transport to get a monoid instance on A, and now I want to upgrade the punit_UP to an equiv between monoids.

[Adam Topaz]

@Ken Lee can you provide a #mwe with what you're actually trying to do?

[Ken Lee]

This should work.

import tactic.transport
import algebra.category.Mon.basic

universes u

def transp_monoid {A : Type u} [s : monoid A] {B : Type u} (e : A ≃ B): monoid B :=
by transport using e

/-
Maths proof.

multiplication on B is...
b * b1 = e.to_fun (e.inv_fun b * e.inv_fun b1)
So we have,

e.to_fun (a * a1)
= e.to_fun ((e.inv_fun (e.to_fun a)) * (e.inv_fun (e.to_fun a1)))
= (e.to_fun a) * (e.to_fun a1)
-/
def upgrade {A : Type u} [monoid A] {B : Type u} (e : A ≃ B) :
Mon.of A ≅ @Mon.of B (transp_monoid e) :=
(@mul_equiv_iso_Mon_iso _ _ _ (transp_monoid e)).hom
{ map_mul' := λ x y, sorry
  .. e}

[Ken Lee]

my specific case was between punit -> A and A

[Adam Topaz]

The issue is not a missing simp lemma (or lemmas), it's the fact that you need to somehow unfold the multiplication on B. E.g. this works:

import tactic.transport
import algebra.category.Mon.basic

universes u

def transp_monoid {A : Type u} [s : monoid A] {B : Type u} (e : A ≃ B) : monoid B :=
by transport using e

def upgrade {A : Type u} [monoid A] {B : Type u} (e : A ≃ B) :
Mon.of A ≅ @Mon.of B (transp_monoid e) :=
(@mul_equiv_iso_Mon_iso _ _ _ (transp_monoid e)).hom
{ map_mul' := λ x y, by { change _ = e (e.symm (e x) * e.symm (e y)), simp },
  .. e}

[Ken Lee]

I see! thanks so much