type class for "`Even`" types?

Stream: maths

[Jireh Loreaux]

Am I correct that we don't have any type class of the following form? The purpose of such a type class would be that for an instance of such a class we could define the function half. Of course, the multiplicativized version of this would give us a generic sqrt function.

class EvenType (α : Type _) [Add α] where
  isEven : ∀ a : α, Even a

noncomputable def half {α : Type _} [AddZeroClass α] [EvenType α] (a : α) :=
  Classical.choose <| EvenType.isEven a

@[simp]
lemma half_add_half {α : Type _} [AddZeroClass α] [EvenType α] (a : α) :
    half a + half a = a :=
  (Classical.choose_spec <| EvenType.isEven a).symm

Why I'm thinking about it: currently, we only have a multiplication on selfAdjoint R when R is a commutative star ring. But selfAdjoint R has a natural non-associative multiplication given by x y ↦ (x * y + y * x)/2 which makes it into a JB-algebra (with appropriate extra structure on R). However, we currently can't really define this multiplication by itself because of the / 2. Of course, one could take an [Module ℚ R] argument and use (1 / 2) • (x * y + y * x), but (a) gross and (b) you'll rarely have a [Module ℚ R] assumption in practice, and you wouldn't get it from things like [Module ℝ R] (nor should you). Possibly we could just use [Module ℝ R], but that seems awfully overly specific.

Another option would be to only define a Mulon selfAdjoint R by bundling it into an Algebra 𝕜 (selfAdjoint R) instance when 𝕜 is a field with trivial star. But this faces it's own major problems: two Algebra 𝕜 (selfAdjoint R) and Algebra 𝕜' (selfAdjoint R) instances now give you non-defeq Mul instances on selfAdjoint R. :face_palm:

I really have no idea how to do this properly. The EvenType idea even suffers from its own problems: any instance of the form instance [Field 𝕜] [Module 𝕜 (selfAdjoint R)] : EvenType (selfAdjoint R) is going to be bad because there will be no reasonable synthesization order. So how would we even arrive at EvenType (selfAdjoint R) instances unless we only used specific fields (like ℝ, ℚ, ℂ) for 𝕜?

[Frédéric Dupuis]

There's also the option to use [Invertible (2 : R)].

[Jireh Loreaux]

That only works if R is unital :sad:

[Frédéric Dupuis]

Oh. Indeed.

[Kyle Miller]

Do we have divisible groups anywhere? It's overkill as an assumption if you just want to divide by 2, but for that there's also the notion of a $p$-divisible group.

[Matthew Ballard]

docs#DivisibleBy

[Eric Wieser]

Don't we already have that multiplication you're talking about? docs#SymAlg

[Eric Wieser]

There we use Invertible 2, but I guess both assume unitality.

[Damiano Testa]

If you introduce a Module ℤ[1/2] α assumption, I do not think that this will require a unit in α.

It is also likely stronger than the instance you proposed, since halves are now constructed, rather than chosen.

Also, fields of characteristic two would likely not be "even types" regardless of the definition of "even type"! :upside_down:

[Jireh Loreaux]

Eric, SymAlg is for when you already have a multiplication, and you want the new one. We don't have any generic Mul instance on selfAdjoint R

[Yury G. Kudryashov]

DivisibleBy (Submonoid.powers (2 : Nat)) M is another option.