elaboration problems for algebra homomorphisms

Stream: mathlib4

[Jireh Loreaux]

Perhaps you've had problems elaborating AlgHoms or StarAlgHoms. If so, I've come across two instances (I think I added them) that are causing the pain. Namely docs#AlgHom.instContinuousLinearMapClassToSemiringToDivisionSemiringToSemifieldToFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNormedSpace and docs#StarAlgHom.instContinuousLinearMapClassComplexInstSemiringComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToModuleInstNormedFieldComplexToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'.

Now, in Lean 3 these instances did not cause the same elaboration pain, but in Lean 4 I get errors when Lean goes looking for certain FunLike instances.

mwe

import Mathlib

variable {R : Type*} [CommSemiring R]

def bar : R →ₐ[R] R := Algebra.ofId R R

-- reenable the instance to break elaboration of `bar_zero`
attribute [-instance] AlgHom.instContinuousLinearMapClassToSemiringToDivisionSemiringToSemifieldToFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNormedSpace

lemma bar_zero : bar (0 : R) = 0 := map_zero bar



variable [StarRing R]

def foo : R →⋆ₐ[R] R := StarAlgHom.ofId R R

-- reenable the instance to break elaboration of `foo_zero`
attribute [-instance] StarAlgHom.instContinuousLinearMapClassComplexInstSemiringComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToModuleInstNormedFieldComplexToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'ToModuleToSeminormedAddCommGroupToNonUnitalSeminormedRingToNonUnitalNormedRingToNormedSpace'

lemma foo_zero : foo (0 : R) = 0 := map_zero foo

This reminds me of elaboration problem we had during porting surround a redundant FunLike instance on Module.Dual that was causing linear maps to fail to elaborate. @Kevin Buzzard and I ran across that independently and we just ended up removing the instance because it was unnecessary. However, I think (?) we actually want both of the instances above. I'd love some help or insight on this.

[Jireh Loreaux]

Here is yet another thread about the Module.Dual issue which may contain some hints as to what is going on here.

[Jireh Loreaux]

@Matthew Ballard I assume that you never made any more progress after the end of that thread?

[Eric Rodriguez]

@Anne Baanen were these the instances you came across that were problematic during the refactor?

[Matthew Ballard]

I’ve mostly got current master building with Anne’s changes at branch#mrb/updates (any help appreciated) but if someone doesn’t beat me to testing the mwe above there I’ll do it in a few hours

[Matthew Ballard]

Yes this is no problem. You can do

set_option maxHeartbeats 500 in
set_option synthInstance.maxHeartbeats 200 in
lemma bar_zero : bar (0 : R) = 0 := map_zero bar

for example.