Why does NonUnitalStarAlgHom require map_zero'?

Stream: mathlib4

[Gregory Wickham]

Why does proving the NonUnitalStarAlgHom structure require me to prove map_zero', when it is a direct consequence of map_smul'? Is there some case where it isn't? Is there some way to make it so that map_zero' doesn't have to be proven explicitly?

I am asking this because I've been making some improvements to my code for the GNS construction, and I was able to refactor my code to create a lemma that is exactly the statement of map_smul' and then prove map_zero' by by simpa using that lemma with the scalar 0 and vector 0, like so

@[simp]
private lemma gnsNonUnitalStarAlgHom_map_smul (m : ℂ) (x : A) :
    (f.leftMulMapPreGNS (m • x)).completion =
    (MonoidHom.id ℂ) m • (f.leftMulMapPreGNS x).completion := by
  ext x
  induction x using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih x => simp [smul_mul_assoc]

noncomputable def gnsNonUnitalStarAlgHom : A →⋆ₙₐ[ℂ] f.GNS →L[ℂ] f.GNS where
  toFun a := (f.leftMulMapPreGNS a).completion
  map_smul' := by simp
  map_zero' := by simpa using f.gnsNonUnitalStarAlgHom_map_smul 0 0

@Jireh Loreaux

[Jireh Loreaux]

It's because of the chain of extends clauses: docs#NonUnitalStarAlgHom extends docs#NonUnitalAlgHom extends docs#DistribMulActionHom extends docs#AddMonoidHom. In AddMonoidHom, the condition map_zero' is truly necessary, but starting with DistribMulActionHom it's not strictly necessary. So, if you wanted to change this, that would be the place to do it. You would need to create a new def for docs#DistributMulActionHom.toAddMonoidHom since that will no longer be a structure projection created from extends. And then of course you'll need to fix all the places downstream that require the proof of the map_zero' field and remove them.

The reason no one has bothered to do it until now: it's generally minimal effort to supply map_zero'.

[Ruben Van de Velde]

Is it that obvious? It doesn't seem like R necessarily has a zero

[Yaël Dillies]

Jireh, this isn't quite true. You can avoid changing the extends structure completely by instead repeating the field name along with a default value

[Yaël Dillies]

Not at a computer, but can explain tomorrow id you haven't figured it out yet

[Jireh Loreaux]

Ruben Van de Velde said:

Is it that obvious? It doesn't seem like R necessarily has a zero

Oh right, sorry, it's just a monoid, not a ring.

[Jireh Loreaux]

Yaël Dillies said:

Jireh, this isn't quite true. You can avoid changing the extends structure completely by instead repeating the field name along with a default value

Sure, but is that actually better for some reason? If these were instances, then I would agree it would be better to have the structure projection onto the parent so that nothing needs unfolding, but for structures I think it would be better to simply omit the field entirely.

[Jireh Loreaux]

Gregory, if you really want, you can add a so-called convenience constructor. This is def which produces a NonUnitalStarAlgHom (or NonUnitalAlgHom) which uses your argument for the map_zero' field when the scalars form a ring. However, like I said before, there's not too much reason to do this, because the map_zero' field is almost always trivial.

[Yaël Dillies]

Your suggestion brings us back to (nearly) flat structures, and my understanding was that nested structures were much more performant

[Jireh Loreaux]

But again: structures, not instances, so is the payoff really that large?

[Jireh Loreaux]

Also, see docs#LinearMap which extends AddHom instead of AddMonoidHom.

[Jireh Loreaux]

So if it's really that much better, presumably we should change that?

[Gregory Wickham]

Jireh Loreaux said:

Gregory, if you really want, you can add a so-called convenience constructor. This is def which produces a NonUnitalStarAlgHom (or NonUnitalAlgHom) which uses your argument for the map_zero' field when the scalars form a ring. However, like I said before, there's not too much reason to do this, because the map_zero' field is almost always trivial.

Once you are declaring a NonUnitalStarAlgHom, doesn't it require [DistribMulAction R A], which requires that R is an AddMonoid, which does have to have a 0? So then we wouldn't strictly need a Ring, right?

[Gregory Wickham]

Ruben Van de Velde said:

Is it that obvious? It doesn't seem like R necessarily has a zero

The scalars must always have a 0 because R must be an AddMonoid in order to define a NonUnitalStarAlgHom, so being able to get map_zero' from map_smul' isn't a special case, right?

[Jireh Loreaux]

There are two things in play, the algebra A, and the scalars R which are only required to be a Monoid. You know that f 0 = f (r • 0) = r • f 0 for any r : R, but this doesn't allow you to conclude that f 0 = 0 since you can't take r = 0. All you know is that f 0 is an absorbing element under the R-action.

[Gregory Wickham]

Oh, I see. Thank you!

[Eric Wieser]

Yaël Dillies said:

Your suggestion brings us back to (nearly) flat structures, and my understanding was that nested structures were much more performant

I've argued in the past that we should be using flat structures for morphisms anyway, as it makes the story around simp lemmas for mk simpler

[Aaron Liu]

Jireh Loreaux said:

Sure, but is that actually better for some reason? If these were instances, then I would agree it would be better to have the structure projection onto the parent so that nothing needs unfolding, but for structures I think it would be better to simply omit the field entirely.

If you define an AddMonoidHom.foo and you have a f : NonUnitalStarAlgHom .. then you can write f.foo if NonUnitalStarAlgHom transitively extends AddMonoidHom

[Eric Wieser]

Though I also think that RingHom extends MonoidHom, AddMonoidHom only inherits such behavior from the first parent and not the second?

[Aaron Liu]

It checks all the parents in some specified order

[Aaron Liu]

you can find out what order with #print