extending structures

Stream: general

[Jireh Loreaux]

I'm looking to define ⋆-preserving maps (star_homs), of various flavors. So, I naturally tried the following:

structure star_hom (E F : Type*) [has_involutive_star E] [has_involutive_star F] :=
(to_fun : E → F)
(map_star' : ∀ x y : E, to_fun (star x) = star (to_fun x))

@[ancestor monoid_hom star_hom]
structure star_monoid_hom (E F : Type*) [monoid E] [monoid F] [star_monoid E] [star_monoid F]
  extends star_hom E F, monoid_hom E F

/- invalid 'structure' header, field 'to_fun' from 'monoid_hom' has already been declared -/

I don't understand why the above doesn't work, but in algebra/group/hom, the following (particularly monoid_hom) works just fine:

/-- Homomorphism that preserves one -/
@[to_additive]
structure one_hom (M : Type*) (N : Type*) [has_one M] [has_one N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)

/-- Homomorphism that preserves multiplication -/
@[to_additive]
structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

/-- Bundled monoid homomorphisms; use this for bundled group homomorphisms too. -/
@[ancestor one_hom mul_hom, to_additive]
structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]
  extends one_hom M N, mul_hom M N

[Eric Wieser]

You need set_option old_structure_cmd true

[Frédéric Dupuis]

BTW, you might want to check out #9888 (being merged right now) which will change the way the API for morphisms is structured. It'll probably save you a lot of time!

[Jireh Loreaux]

Thanks! Yes, I just saw this. Seems like a fantastic improvement to the API.