Zulip Chat Archive

Stream: maths

Topic: Extending `add_monoid_hom` and `add_monoid_hom_class`

Christopher Hoskin (Mar 09 2022 at 18:13):

Following the pattern in algebra.group.hom I'm trying to extend the add_monoid_hom structure and add_monoid_hom_class class as follows:

import algebra.ring.basic
import algebra.group.hom

variable {A : Type*}
variable {F : Type*}

variable [non_unital_non_assoc_semiring A]

@[ancestor add_monoid_hom]
structure centroid (A : Type*) [non_unital_non_assoc_semiring A] extends A →+ A :=
(lmul_comm': ∀ a b, to_add_monoid_hom (a*b) = a * (to_add_monoid_hom b))
(rmul_comm': ∀ a b, to_add_monoid_hom (a*b) = (to_add_monoid_hom a) * b)


attribute [nolint doc_blame] centroid.to_add_monoid_hom

@[ancestor add_monoid_hom_class]
class centroid_class (F : Type*) (A : out_param $ Type*) [non_unital_non_assoc_semiring A]
  extends add_monoid_hom_class F A A :=
(lmul_comm: ∀ (f : F) (a b : A), f (a*b) = a * (f b))
(rmul_comm: ∀ (f : F) (a b : A), f (a*b) = (f a) * b)

-- c.f. https://github.com/leanprover-community/mathlib/blob/5d405e2a7028f87e962e7cc2133dc0cfc9c55f7d/src/algebra/group/hom.lean#L276
instance centroid.centroid_class : centroid_class (centroid A) A :=
{ lmul_comm := centroid.lmul_comm',
  rmul_comm := centroid.rmul_comm',
  ..add_monoid_hom.add_monoid_hom_class }

I'm getting the following error with instance centroid.centroid_class : centroid_class (centroid A) A:

centroid.lean:24:0
type mismatch at field 'coe'
  add_monoid_hom_class.coe
has type
  (?m_1 →+ ?m_2) → Π (a : ?m_1), (λ (_x : ?m_1), ?m_2) a : Type (max ? ?)
but is expected to have type
  centroid A → Π (a : A), (λ (_x : A), A) a : Type u_1
centroid.lean:24:0
type mismatch at field 'coe_injective''
  add_monoid_hom_class.coe_injective'
has type
  function.injective add_monoid_hom_class.coe
but is expected to have type
  function.injective ?coe
centroid.lean:24:0
type mismatch at field 'map_add'
  add_monoid_hom_class.map_add
has type
  ∀ (f : ?m_1 →+ ?m_2) (x y : ?m_1), ⇑f (x + y) = ⇑f x + ⇑f y
but is expected to have type
  ∀ (f : centroid A) (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y
centroid.lean:24:0
type mismatch at field 'map_zero'
  add_monoid_hom_class.map_zero
has type
  ∀ (f : ?m_1 →+ ?m_2), ⇑f 0 = 0
but is expected to have type
  ∀ (f : centroid A), ⇑f 0 = 0

centroid.lean:25:15
type mismatch at field 'lmul_comm'
  centroid.lmul_comm'
has type
  ∀ (self : centroid ?m_1) (a b : ?m_1), ⇑(self.to_add_monoid_hom) (a * b) = a * ⇑(self.to_add_monoid_hom) b
but is expected to have type
  ∀ (f : centroid A) (a b : A), ⇑f (a * b) = a * ⇑f b

centroid.lean:26:15
type mismatch at field 'rmul_comm'
  centroid.rmul_comm'
has type
  ∀ (self : centroid ?m_1) (a b : ?m_1), ⇑(self.to_add_monoid_hom) (a * b) = ⇑(self.to_add_monoid_hom) a * b
but is expected to have type
  ∀ (f : centroid A) (a b : A), ⇑f (a * b) = ⇑f a * b

I'm afraid I can't quite untangle what I'm supposed to be doing here?

Thanks,

Christopher

Kevin Buzzard (Mar 09 2022 at 18:33):

Your problem is with the last line of code: ..add_monoid_hom.add_monoid_hom_class says "I'll fill in the rest of the fields using add_monoid_hom.add_monoid_hom_class, which is an instance of add_monoid_hom_class (M →+ N) M N so which can (only) be used to make a term of type centroid_class F A if this matches with add_monoid_hom_class F A A. OK let me figure out how all this matches". Solving this we see that M=N=A and F=A →+ A. But your F is centroid A so the matching problem can't be solved.

Kevin Buzzard (Mar 09 2022 at 18:36):

The very first line of your error

type mismatch at field 'coe'
  add_monoid_hom_class.coe
has type
  (?m_1 →+ ?m_2) → Π (a : ?m_1), (λ (_x : ?m_1), ?m_2) a : Type (max ? ?)
but is expected to have type
  centroid A → Π (a : A), (λ (_x : A), A) a : Type u_1

says "OK I have something which eats an additive monoid hom but you're telling me I need to eat a term of type centroid A" so this is unification failing explicitly (and correctly).

Kevin Buzzard (Mar 09 2022 at 18:51):

-- this is what you're missing
instance centroid.add_monoid_hom_class : add_monoid_hom_class (centroid A) A A :=
{ coe := λ c a, c.to_add_monoid_hom a,
  coe_injective' := sorry,
  map_add := sorry,
  map_zero := sorry }

-- c.f. https://github.com/leanprover-community/mathlib/blob/5d405e2a7028f87e962e7cc2133dc0cfc9c55f7d/src/algebra/group/hom.lean#L276
instance centroid.centroid_class : centroid_class (centroid A) A :=
{ lmul_comm := centroid.lmul_comm',
  rmul_comm := centroid.rmul_comm',
  ..centroid.add_monoid_hom_class }

Christopher Hoskin (Mar 09 2022 at 18:52):

This at least doesn't have any errors:

instance centroid.centroid_class : centroid_class (A →+ A) A :=
{ lmul_comm := sorry,
  rmul_comm := sorry,
  ..add_monoid_hom.add_monoid_hom_class }

Although I'm not sure if this is what I need to prove to satisfy the make sure to extend monoid_hom_class. requirement?

Kevin Buzzard (Mar 09 2022 at 18:53):

I don't know how add_monoid_class works but looking at the docstring it seems that you should be extending it when you define centroid.

Kevin Buzzard (Mar 09 2022 at 19:02):

Christopher Hoskin said:

This at least doesn't have any errors:
instance centroid.centroid_class : centroid_class (A →+ A) A :=
{ lmul_comm := sorry,
  rmul_comm := sorry,
  ..add_monoid_hom.add_monoid_hom_class }
Although I'm not sure if this is what I need to prove to satisfy the make sure to extend monoid_hom_class. requirement?

Sure this doesn't have any errors -- but the sorrys are not provable, right?

Christopher Hoskin (Mar 09 2022 at 19:07):

Nearly there?

instance centroid.add_monoid_hom_class : add_monoid_hom_class (centroid A) A A :=
{ coe := λ c a, c.to_add_monoid_hom a,
  coe_injective' := sorry,
  map_add := λ f _ _, f.to_add_monoid_hom.map_add _ _,
  map_zero := λ f, f.to_add_monoid_hom.map_zero, }

-- c.f. https://github.com/leanprover-community/mathlib/blob/5d405e2a7028f87e962e7cc2133dc0cfc9c55f7d/src/algebra/group/hom.lean#L276
instance centroid.centroid_class : centroid_class (centroid A) A :=
{ lmul_comm := λ f a b, by apply f.lmul_comm',
  rmul_comm := λ f a b, by apply f.rmul_comm', }

Christopher Hoskin (Mar 09 2022 at 19:16):

This appears to work:

instance centroid.add_monoid_hom_class : add_monoid_hom_class (centroid A) A A :=
{ coe := λ c a, c.to_add_monoid_hom a,
  coe_injective' := λ f g h,
  begin
    cases f,
    cases g,
    congr',
    exact fun_like.ext f__to_add_monoid_hom g__to_add_monoid_hom (congr_fun h),
  end,
  map_add := λ f _ _, f.to_add_monoid_hom.map_add _ _,
  map_zero := λ f, f.to_add_monoid_hom.map_zero, }

-- c.f. https://github.com/leanprover-community/mathlib/blob/5d405e2a7028f87e962e7cc2133dc0cfc9c55f7d/src/algebra/group/hom.lean#L276
instance centroid.centroid_class : centroid_class (centroid A) A :=
{ lmul_comm := λ f a b, by apply f.lmul_comm',
  rmul_comm := λ f a b, by apply f.rmul_comm', }

Eric Wieser (Mar 09 2022 at 19:42):

Doesn't the type you want already exist as docs#distrib_mul_action_hom?

Eric Wieser (Mar 09 2022 at 19:43):

That is, as R →+[R] R?

Christopher Hoskin (Mar 09 2022 at 20:11):

That seems to be something similar - but is that equivariant with respect to both the right and left action of R on R?

Christopher Hoskin (Mar 09 2022 at 21:20):

I guess I would need to extend R →+[R] R and R →[Rᵐᵒᵖ] R?

Christopher Hoskin (Mar 09 2022 at 21:31):

Trying:

structure centroid (A : Type*) [non_unital_non_assoc_semiring A] extends A →[A] A, A →[Aᵐᵒᵖ] A

but I get field collisions, regardless of whether or not I use set_option old_structure_cmd true.

Yaël Dillies (Mar 09 2022 at 21:31):

GIve me 5Min.

Yaël Dillies (Mar 09 2022 at 22:11):

Here you go! branch#centroid_hom

Yaël Dillies (Mar 09 2022 at 22:11):

Feel free to modify, kick me out of the copyright, or whatever. This is your branch, with the correct design.

Eric Wieser (Mar 09 2022 at 22:53):

You're right, distrib_mul_action_hom only captures one of your requirements, and extending it twice is likely just a headache

Christopher Hoskin (Mar 10 2022 at 09:13):

@Yaël Dillies Wow - thanks! I'll take a look this evening.

Christopher Hoskin (Mar 13 2022 at 11:24):

I've managed to show that centroid_hom is a semiring, and a ring when α is a ring. As a further example of the sort of result one can prove, I'm trying to show that prime associative rings have commutative centroid (using a hypothesis for prime which avoids the use of two sided ideals). Nearly there, but stuck on how to bring all the threads of the argument together:

https://github.com/leanprover-community/mathlib/blob/centroid_hom/src/algebra/group/hom/centroid.lean#L228

The goal is: