Unbundled morphism classes

Stream: mathlib4

[Michael George]

I see that the unbundled classes IsAddHom, IsGroupHom etc are deprecated in Mathlib, and the bundled morphisms are recommended as a replacement. However, I'm not seeing how to use them for what I need.

I'm trying to build a data structure (FilteredReal α) that wraps types that represent subsets of the reals (and wraps them with floating-point intervals to improve performance). My WIP implementation is here.

I can implement various operation typeclasses (e.g. Zero, One, Add, etc) on my wrapped type, but only if the underlying subset supports those operations and they commute with the embedding. (e.g. I can implement One if α has a One and if coe (1 : α) = (1 : ℝ)). It seems sensible to encode this using typeclasses:

instance [One α] [Coe α ℝ] [IsOneHom coe] : One (FilteredReal α) where
  one := ...
    -- dependent value can only be constructed using `IsOneHom` instance

The fact that Mathlib has migrated away from unbundled morphism classes makes me think that this design is not idiomatic. On the other hand, I don't see how to implement this with bundled morphisms, unless I make a separate FilteredReal structure for each combination of operations that I want to support. I wonder what's the "right" approach here? I'm also curious about why mathlib has shifted to favor bundled morphisms.

[Anne Baanen]

You're right that there isn't a good way to express this property. On the other hand I'm worried that using Coe will bring you more trouble. Since Coe.coe doesn't actually appear in the elaborated coercions you're probably going to run into issues trying to simplify. Is it a good idea to parametrize over a function (f : α → ℝ) instead of over an instance [Coe α ℝ). (Also: coercions are hard to parametrize over because coercions are actually elaborated as the transitive closure of docs#Coe, docs#CoeHead, docs#CoeTail etc.)

[Anne Baanen]

Concretely:

structure FilteredReal (α : Type) (f : α → ℝ) where
  value  : Thunk α
  range  : Around (value.get)

@[simps] instance [Zero α] {F} [FunLike F α ℝ] [ZeroHomClass F α ℝ] (f : F) : Zero (FilteredReal α f) where
  zero := {
    value := (0 : α)
    range := ⟨0, by simp [Thunk.get, map_zero]⟩
  }

[Michael George]

Thanks, that makes sense. I think what I was missing is that the Funlike instance allows me to not have to change the argument to FilteredReal.