!4#4857 Magma.ofHom

Stream: mathlib4

[Jon Eugster]

In !4#4857 I got problems getting Magma.of to work, which is just defined as Bundled.of. In particularly I fail to insert an element (x : X) into a function that takes of X → of Y. Here is a minimised example:

Nvm, typo in the MWE, need to fix that first

[Jon Eugster]

ok second try :sweat_smile: in !4#4857 Magma.ofHom has type of X → of Y but somehow it cannot be applied to an element (x : X) even though (↑x : of X) seems to work fine. In this #mwe the last line fails with function expected at `ofHom f` term has type `of X ⟶ of Y` :

import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.CategoryTheory.ConcreteCategory.BundledHom
-- import Mathlib.Algebra.PEmptyInstances
-- import Mathlib.CategoryTheory.Functor.ReflectsIso
-- import Mathlib.CategoryTheory.Elementwise

universe u v

open CategoryTheory

def Magma : Type (u + 1) :=
  Bundled Mul

namespace Magma

instance bundledHom : BundledHom @MulHom :=
  ⟨@MulHom.toFun, @MulHom.id, @MulHom.comp,
    --Porting note : was `@MulHom.coe_inj` which is deprecated
    by intros; apply @FunLike.coe_injective, by aesop_cat, by aesop_cat⟩

deriving instance LargeCategory for Magma
instance concreteCategory : ConcreteCategory Magma := BundledHom.concreteCategory MulHom

instance : CoeSort Magma (Type _) :=
  Bundled.coeSort

def of (M : Type u) [Mul M] : Magma :=
  Bundled.of M

def ofHom {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) : of X ⟶ of Y :=
  f

variable {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) (x : X)
#check (x : of X)
#check (ofHom f) (x : of X) -- fails!

demonstration which worked in lean3:

import algebra.hom.equiv.basic
import category_theory.concrete_category.bundled_hom
-- import algebra.pempty_instances
-- import category_theory.functor.reflects_isomorphisms
-- import category_theory.elementwise

universes u v

open category_theory

def Magma : Type (u+1) := bundled has_mul

namespace Magma

instance bundled_hom : bundled_hom @mul_hom :=
⟨@mul_hom.to_fun, @mul_hom.id, @mul_hom.comp, @mul_hom.coe_inj⟩

attribute [derive [large_category, concrete_category]] Magma

instance : has_coe_to_sort Magma Type* := bundled.has_coe_to_sort

def of (M : Type u) [has_mul M] : Magma := bundled.of M

def of_hom {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) :
  of X ⟶ of Y := f

variables {X Y : Type u} [has_mul X] [has_mul Y] (f : X →ₙ* Y) (x : X)
#check (x : of X)
#check (of_hom f) (x : of X) -- works

end Magma

Does anybody have an idea?

[Jon Eugster]

(I also just realised that of X → of Y and of X ⟶ of Y are not the same thing... the latter is a quiver. so the problem might have to do with quivers, but Im out of time to debug for now)