Level of Generality while Contributing

Stream: new members

[Callum Cassidy-Nolan]

Hi there, I had a question relating to contributing to mathlib as a newer mathematician.

The other week I was working with even/odd functions, and I found that the definitions I was familiar with were not in mathlib.

I created some simple definitions that work for what I want to do:

def even_fun (f : ℝ → ℝ) := ∀ (x : ℝ), f x = f (-x)

def odd_fun (f : ℝ → ℝ) := ∀ (x : ℝ), f x = - f (-x)

But when I asked about it on zulip, it looks like if I wanted to contribute to mathlib, I would need the most generalized version of it:

Jireh Loreaux said:

I haven't seen it (which doesn't mean it isn't there!), but if we did have it, then the appropriate level of generality would be something like an involutive linear map on a vector space over a field of characteristic different from 2. Any such map decomposes the vector space into a fixed part, and an anti-fixed part. For even functions (the fixed part) the involution is (lambda x, f x) -> (lambda x, f -x). (Sorry, on mobile)

As of right now, I'm not quite sure how to implement that definition, but I do have this definition that works for my needs.

I am curious about the standpoint of having specialized versions of theorems in mathlib, like my basic ones I've defined

To me it makes sense to have at least one form of the definition (generalized or not) in mathlib at any point in time so that at least some people can use it (rather than none) and then over time work on getting the most generalized version in.

What do you think?

[Kyle Miller]

I think another way to say Jireh's suggestion is that even/odd functions correspond to eigenvectors of the domain-reversing involution associated to the eigenvalues 1 and -1. (Though Jireh is explaining, additionally, the even/odd direct sum decomposition.)

[Kyle Miller]

I'm not sure what the "right" generalization of even/odd should be. One thing that comes to mind is how the fact it's centered at 0 is arbitrary, so that could be generalized as well -- rather than the involution acting on a vector space, it could also be an involution on an affine space.

[Kyle Miller]

One formalization:

import algebra.group.basic
import linear_algebra.eigenspace
import data.real.basic

@[simps]
def act {α : Type*} (f : α → α) : module.End ℝ (α → ℝ) :=
{ to_fun := λ g, g ∘ f,
  map_add' := by { intros, refl, },
  map_smul' := by { intros, refl, } }

def is_even (f : ℝ → ℝ) := f ∈ module.End.eigenspace (act (has_neg.neg : ℝ → ℝ)) 1
def is_odd (f : ℝ → ℝ) := f ∈ module.End.eigenspace (act (has_neg.neg : ℝ → ℝ)) (-1)

lemma is_even_iff {f : ℝ → ℝ} :
  is_even f ↔ ∀ x, f (-x) = f x :=
begin
  simp only [is_even, module.End.mem_eigenspace_iff, one_smul],
  split,
  { intros h x,
    simpa using congr_fun h x, },
  { intro h,
    ext x,
    simpa using h x, },
end

lemma is_odd_iff {f : ℝ → ℝ} :
  is_odd f ↔ ∀ x, f (-x) = -f x :=
begin
  simp only [is_odd, module.End.mem_eigenspace_iff, one_smul],
  split,
  { intros h x,
    simpa using congr_fun h x, },
  { intro h,
    ext x,
    simpa using h x, },
end

[Kyle Miller]

There's probably something somewhere in the library that can replace act

[Kyle Miller]

That said, there's probably no reason to define is_even and is_odd in such a complicated way if you can write lemmas showing a definition is equivalent to the fancy (and "right") definition, so I might go with this (using @Kevin Buzzard's suggestion from the other thread):

import algebra.group.basic
import linear_algebra.eigenspace
import data.real.basic

def function.is_even {α β : Type*} [has_neg α] (f : α → β) : Prop :=
∀ (x : α), f (- x) = f x

def function.is_odd {α β : Type*} [has_neg α] [has_neg β] (f : α → β) : Prop :=
∀ (x : α), f (- x) = -f x

@[simps]
def act {α : Type*} (f : α → α) : module.End ℝ (α → ℝ) :=
{ to_fun := λ g, g ∘ f,
  map_add' := by { intros, refl, },
  map_smul' := by { intros, refl, } }

lemma is_even_iff {f : ℝ → ℝ} :
  function.is_even f ↔ f ∈ module.End.eigenspace (act (has_neg.neg : ℝ → ℝ)) 1 :=
begin
  simp only [module.End.mem_eigenspace_iff, one_smul],
  split,
  { intro h,
    ext x,
    simpa using h x, },
  { intros h x,
    simpa using congr_fun h x, },
end

lemma is_odd_iff {f : ℝ → ℝ} :
  function.is_odd f ↔ f ∈ module.End.eigenspace (act (has_neg.neg : ℝ → ℝ)) (-1) :=
begin
  simp only [module.End.mem_eigenspace_iff, neg_smul, one_smul],
  split,
  { intro h,
    ext x,
    simpa using h x, },
  { intros h x,
    simpa using congr_fun h x, },
end

[Callum Cassidy-Nolan]

So as a beginner if I find something not included in mathlib, but I'm not aware of the most general definition, would you recommend me to try to PR with that definition?

[Jireh Loreaux]

Others can overrule me, but I would do the following: ask on Zulip, "I'm considering implementing concept X using method Y, is this a good approach, or should I attempt it a different way?" Then people can provide input before you PR. That way, when you do PR, you likely won't have to rewrite everything from scratch.

Note: in mathlib, we are at least sometimes willing to wait a long time to have things done the "right" way. Other times, we decide it's important enough to have a given thing that we forgo such considerations.

As for the specific even/odd discussion above, I'll write something up tonight or tomorrow showing the kind of thing I was thinking.

@Kyle Miller zero isn't quite as arbitrary when you think of the involution on the vector space of functions as additive group inversion on the domain (of course, yes, you can have other involutions of the domain)

[Kyle Miller]

@Callum Cassidy-Nolan I don't think I can give a blanket recommendation. You can try asking #Is there code for X? whether something is already in mathlib or if it's close to something already in mathlib, and there's also #maths to discuss how you might formalize something and to draw up a plan. A problem with just doing a PR is that not everyone is reviewing everything, so it might not get so much attention.

There can also be many ways to generalize something, so it takes gaining some kind of consensus to know if something is "most" general. This is a matter of thinking through the sorts of theorems you're wanting to prove, what sorts of math we're each personally interested in formalizing, what resources (e.g. time) we have to do the formalization, and so on. We don't want to generalize just for the sake of generalization -- if we think no one is going to prove theorems about generalized even/odd functions (or, if they do, it's going to be a long long time from now), then it can be a waste of effort. If you're not careful, you might do the wrong generalization due to lack of foresight (this is a common software engineering problem...)

[Kyle Miller]

@Jireh Loreaux I get that the domain is a vector space and that even/odd corresponds to the isotypic components of representation of the group generated by has_neg.neg acting on the domain (and I do like this generalization). My question is whether this is the "right" generalization, given the theory what might be in the theory of even/odd functions.

[Kyle Miller]

Like if you're considering power series representations of functions centered at different points, you probably want to generalize even/odd to this situation.

[Kyle Miller]

(But that would also be more complicated, since I guess you want more of a pseudogroup acting on the domain to deal with the radius of convergence.)

[Jireh Loreaux]

By the way, the reason I was thinking about this generalization is that it occurs all over:

1. Complex numbers with conjugation as real-linear involution -> real and imaginary parts.
2. Square matrices with transpose -> symmetric and skew-symmetric parts.
3. Yes, power series
4. Adjoint operation in *-Algebras
5. Even and odd functions

[Jireh Loreaux]

I never required objects to be functions in my original proposal.

[Jireh Loreaux]

For power series you could just work with formal multilinear series and ignore convergence

[Kyle Miller]

Oh, I misread part of your proposal: I thought you were talking about, essentially, taking a representation V of a group then considering Hom(V, W) for some reason.

[Jireh Loreaux]

This generality is why I considered it to be the right generalization, but of course I'm open to other ideas.

[Kyle Miller]

Regarding the generalization you're talking about, would you want to do anything other than studying module.End.eigenspace T 1 and module.End.eigenspace T (-1) for some involution T?

[Jireh Loreaux]

I hadn't thought about it that much (other than this is one of my pet problems to give to linear algebra students and then show them how to occurs everywhere).

Basically all I was thinking is that if we are going to do this at all, then it probably makes sense to have a uniform definition and API. Just plug in a linear involution, get out the relevant fixed and anti-fixed submodules and the decomposition.

[Jireh Loreaux]

That being said, if we think it's not worth the effort that's fine too.

[Kyle Miller]

I think it's worth the effort to flesh all that out. I just think that, except for all the surrounding theory and the decomposition in char-not-2 (including projections), we sort of already have it.

[Jireh Loreaux]

This is basically the kind of thing I was thinking. The names might be improved, and of course for fields with characteristic different from 2 we could prove more specialized stuff.

/-
Copyright (c) 2022 Jireh Loreaux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jireh Loreaux
-/
import linear_algebra.eigenspace
import algebra.direct_sum.module

/-! # Linear involution decomposition

Throughout mathematics a certain phenomenon can be observed which amounts to the decomoposition of
some module into two pieces, one of which is fixed by a given operation and the other of which is
anti-fixed. As examples:

1. The decomposition of `z : ℂ` into `z = z.re + I * z.im` with the operation of `conj`.
2. The decomposition of a matrix into its symmetric and skew-symmetric parts with the transpose
  operation.
3. The decomposition of an operator into its selfadjoint and skew-selfadjoint parts, with the
  adjoint operation.
4. The decomposition of a real-valued function into its even and odd parts, with the operation
  given by `λ f : ℝ → ℝ, λ x, f (-x)`.
5. The decomposition of a polynomial into its even and odd parts.begin
6. The decomposition of complex-valued measures into their real and imaginary parts.

All of these are unified by a common thread. There is a linear involution acting on the module.
Here we ellucidate that role.
-/

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
  (lin_inv : module.End R M)

namespace linear_involution

open function

local postfix `†`:std.prec.max_plus := lin_inv

def fixed : submodule R M := lin_inv.eigenspace (1 : R)

def anti_fixed : submodule R M := lin_inv.eigenspace (-1 : R)

variables {lin_inv}

lemma mem_fixed_def {m : M} : m ∈ fixed lin_inv ↔ m† = (1 : R) • m :=
module.End.mem_eigenspace_iff

@[simp]
lemma mem_fixed_iff {m : M} : m ∈ fixed lin_inv ↔ m† = m :=
by { convert mem_fixed_def, exact (one_smul R m).symm }

lemma mem_anti_fixed_def {m : M} : m ∈ anti_fixed lin_inv ↔ m† = (-1 : R) • m :=
module.End.mem_eigenspace_iff

@[simp]
lemma mem_anti_fixed_iff {m : M} : m ∈ anti_fixed lin_inv ↔ m† = -m :=
by { convert mem_anti_fixed_def, rw [neg_smul, one_smul] }

lemma add_lin_inv_self_fixed (h : involutive lin_inv) (m : M) :
  m + m† ∈ fixed lin_inv :=
by simp [h.right_inverse m, add_comm m]

lemma sub_lin_inv_self_anti_fixed (h : involutive lin_inv) (m : M) :
  m - m† ∈ anti_fixed lin_inv :=
by simp [h.right_inverse m, add_comm m]

variable (lin_inv)
def fixed_anti_fixed_pair : bool → submodule R M
| tt := fixed lin_inv
| ff := anti_fixed lin_inv

open submodule

lemma fixed_anti_fixed_sum (h₂ : is_unit (2 : R)) (m : M) :
  h₂.unit⁻¹ • m + (h₂.unit⁻¹ • m)† + (h₂.unit⁻¹ • m - (h₂.unit⁻¹ • m)†) = m :=
begin
  simp only [units.smul_def, add_add_sub_cancel],
  rw [←smul_add, ←two_smul R m, smul_smul, h₂.coe_inv_mul, one_smul],
end

variable {lin_inv}
lemma sup_fixed_anti_fixed (h : involutive lin_inv) (h₂ : is_unit (2 : R)) :
  (fixed lin_inv) ⊔ (anti_fixed lin_inv) = ⊤ :=
eq_top_iff'.mpr (λ m, mem_sup.mpr
  ⟨_, add_lin_inv_self_fixed h _,
   _, sub_lin_inv_self_anti_fixed h _,
   fixed_anti_fixed_sum lin_inv h₂ m⟩)

lemma zero_of_fixed_of_anti_fixed (h₂ : is_unit (2 : R)) {m : M}
  (hm₁ : m ∈ fixed lin_inv) (hm₂ : m ∈ anti_fixed lin_inv) : m = 0 :=
begin
  simp only [mem_fixed_iff, mem_anti_fixed_iff] at hm₁ hm₂,
  have hm₃ : (2 : R) • m = 0, by { rw [two_smul], nth_rewrite 1 ←hm₁, rw [hm₂, add_neg_self] },
  have : (↑h₂.unit⁻¹ : R) • ((2 : R) • m) = (↑h₂.unit⁻¹ : R) • (0 : M) := congr_arg2 _ rfl hm₃,
  simpa [smul_smul, h₂.coe_inv_mul] using this,
end

lemma inf_fixed_anti_fixed (h : involutive lin_inv) (h₂ : is_unit (2 : R)) :
  (fixed lin_inv) ⊓ (anti_fixed lin_inv) = ⊥ :=
(submodule.eq_bot_iff _).mpr
  (λ m hm, zero_of_fixed_of_anti_fixed h₂ (mem_inf.mp hm).1 (mem_inf.mp hm).2)

end linear_involution

[Jireh Loreaux]

@Kyle Miller, see above.

[Eric Wieser]

This generalization seems to mean the wrong thing in characteristic two to me; docs#clifford_algebra.graded_algebra performs the same decomposition (using the involution as docs#clifford_algebta.involute), but in a way that still works even when the involution is degenerate

[Jireh Loreaux]

@Eric Wieser can you expand on this? I'm not particularly familiar with the graded algebra structure on Clifford algebras. And what do you think is the right generalization in characteristic two?

[Eric Wieser]

The graded structure is built in the way you could build one for the free algebra; even-length monomials are even and odd-length are odd

[Eric Wieser]

If you define an involution that sends $abc$ to $(-a)(-b)(-c)$ then you can indeed use it as you suggest above to count whether the length is even or odd

[Eric Wieser]

But this doesn't work at all in char 2 when -a = a, because now all your elements are both even and odd

[Eric Wieser]

So the definition via the involution doesn't seem to accurately capture the intuitive notion of even and odd-ness that arises by counting terms in monomials

[Eric Wieser]

I think the right generalization is just "is a zmod 2-graded ring under some choice of submodules"?

[Eric Wieser]

That gives you x ∈ odd →y ∈ even → x*y ∈ odd etc

[Jireh Loreaux]

Yes, but note the linear involution approach doesn't require a multiplication.

[Jireh Loreaux]

So i guess a graded module?

[Eric Wieser]

Did any of your examples above not have a multiplication?

[Eric Wieser]

The multiplication is the thing enforcing the structure, so a graded module (in the "graded additive group with a single action" sense of the word) wouldn't give you anything about how even and odd interact

[Jireh Loreaux]

Hmmm..., I suppose not. But here's one: consider an R-module V and a group G. Then G → V has a natural linear involution given by λ f, λ g, f g⁻¹. But yes, other than given a direct sum decomposition (when R doesn't have characteristic 2) this tells you nothing about the interaction.

[Jireh Loreaux]

I think your graded ring structure is probably the right generalization.

[Eric Wieser]

I think I remember seeing a trick somewhere that conjured a larger space to work in that allowed something resembling your approach to be used even in char 2; but it was mostly over my head. I'll try to find it tomorrow.