Homeless lemma

Stream: maths

[Oliver Nash]

I believe I need to use the following lemma:

import order.lattice

lemma monotone_nat_action_iff {α : Type*} [semilattice_sup α] (f : ℕ → α → α)
  (h_zero : ∀ a, f 0 a = a)
  (h_add : ∀ n₁ n₂ a, f (n₁ + n₂) a = f n₁ (f n₂ a))
  (h_mono : ∀ a, monotone (f a)) :
  (∀ n₁ n₂ a₁ a₂, f (n₁ + n₂) (a₁ ⊔ a₂) ≤ (f n₁ a₁) ⊔ (f n₂ a₂)) ↔
  (∀ a₁ a₂, f 1 (a₁ ⊔ a₂) ≤ (f 1 a₁) ⊔ a₂) :=
begin
  split,
  { intros h a₁ a₂, conv_rhs { rw ← h_zero a₂, }, exact h 1 0 a₁ a₂, },
  { intros h n₁ n₂ a₁ a₂, have h' : ∀ n a₁ a₂, f n (a₁ ⊔ a₂) ≤ (f n a₁) ⊔ a₂,
    { intros n, induction n with n ih; intros a₁ a₂,
      { rw [h_zero, h_zero], },
      { calc f (n + 1) (a₁ ⊔ a₂) = f n (f 1 (a₁ ⊔ a₂)) : h_add n 1 _
                             ... ≤ f n ((f 1 a₁) ⊔ a₂) : h_mono n (h a₁ a₂)
                             ... ≤ (f n (f 1 a₁)) ⊔ a₂ : ih _ _
                             ... = (f (n + 1) a₁) ⊔ a₂ : by rw h_add n 1, }, },
    calc f (n₁ + n₂) (a₁ ⊔ a₂) = f n₁ (f n₂ (a₁ ⊔ a₂)) : h_add _ _ _
                           ... = f n₁ (f n₂ (a₂ ⊔ a₁)) : by rw sup_comm
                           ... ≤ f n₁ ((f n₂ a₂) ⊔ a₁) : h_mono n₁ (h' n₂ _ _)
                           ... = f n₁ (a₁ ⊔ (f n₂ a₂)) : by rw sup_comm
                           ... ≤ (f n₁ a₁) ⊔ (f n₂ a₂) : h' n₁ a₁ _, },
end

but I'm not sure:

• where it should live,
• what it should be called,
• whether I'm stating it in appropriate generality.

I'd be grateful for any comments!

[Heather Macbeth]

Would it make sense to make this literally, rather than just morally, a result about an action of ℕ on α? There is a theory of monoid action, docs#mul_action. Seemingly only in the multiplicative case, should we add the additive case?

[Heather Macbeth]

I have also wondered lately whether we need a fancier theory, to deal with actions which are "category-respecting": actions on orders which are monotone, actions on topological spaces which are continuous, actions on manifolds which are smooth.

[Oliver Nash]

Absolutely agreed on using mul_action, great point.

[Heather Macbeth]

Heather Macbeth said:

I have also wondered lately whether we need a fancier theory, to deal with actions which are "category-respecting": actions on orders which are monotone, actions on topological spaces which are continuous, actions on manifolds which are smooth.

One way to do that here would be to write down the monoid instance on the type of monotone self-maps of α, and phrase your lemma as a result about a homomorphism of ℕ into that monoid.

[Oliver Nash]

Also a nice idea, though I have to pick between this approach and mul_action then I guess.

[Heather Macbeth]

I thought I'd leave the decision to someone else! :)

[Oliver Nash]

I'm pretty much done for the day so I'll mull it for a day or so. Currently leaning toward mul_action.

[Oliver Nash]

I'd also like it if there was a helpful generalisation of ℕ though it's not clear to me that there is (at least a helpful one).

[Oliver Nash]

Incidentally the mysterious f in my case is lie_algebra.derived_series_of_ideal cf https://github.com/leanprover-community/mathlib/pull/5815

[Adam Topaz]

Heather Macbeth said:

I have also wondered lately whether we need a fancier theory, to deal with actions which are "category-respecting": actions on orders which are monotone, actions on topological spaces which are continuous, actions on manifolds which are smooth.

This is possible to do since End X has a monoid instance (where X is a term of some type with a category instance). A monoid action of M on X compatible with the category structure is then a morphism of monoids M \to End X.

[Adam Topaz]

docs#category_theory.End

[Adam Topaz]

I tried to play with this once before ( I was trying to do some Tannakian sort of stuff in lean)... IIRC I found it somewhat cumbersome. But maybe it's worth another shot.

[Heather Macbeth]

@Adam Topaz one can also do this "by hand": construct the group/monoid instance on the monotone self-maps of an order, the self-homeomorphisms of a topological space, the diffeomorphism group of a manifold, and then define an action to be a homomorphism into this group/monoid. Is there any reason to do this construction "by category theory"? (Sorry for the naive question!)

[Adam Topaz]

I'll sketch some code...

[Adam Topaz]

1 sec

[Adam Topaz]

import algebra
import category_theory.endomorphism
import category_theory.concrete_category

open category_theory

variables (M : Type*) [monoid M] {C : Type*} [category C] [concrete_category C] (X : C)

class mul_action' := (act : M →* End X)

instance bar : has_coe_to_sort C := ⟨Type*,λ Y, (forget C).obj Y⟩

variables {M X}

@[simp]
def foo [mul_action' M X] (m : M) (x : X) : X := (forget C).map (mul_action'.act m) x

instance baz [mul_action' M X] : mul_action M X :=
{ smul := foo,
  one_smul := λ x, by simp,
  mul_smul := by tidy }

[Adam Topaz]

So now you can define an action on a monoid on an object in any concrete category (such as Top, Type*, etc.) which is compatible with the underlying structure.

[Adam Topaz]

I don't know if this can be made to be useful enough so that the "standard" actions, like the action on a topological space by continuous maps, a manifold by diffeomorphisms, etc., don't need to be individually written by hand.

[Heather Macbeth]

I think this is more subtle, though. Back in 10 mins, but what about Lie group actions on manifolds? Action needs to be smooth in the "group" co-ordinate too.

[Adam Topaz]

Oh, I see....

[Adam Topaz]

Sorry, I misunderstood the question.

[Adam Topaz]

In this case we need to use monoid objects internal to a cateogry.

[Adam Topaz]

This exists docs#category_theory.monoidal.Mon_ and it should be doable...

[Adam Topaz]

https://leanprover-community.github.io/mathlib_docs/category_theory/monoidal/Mon_.html#Mon_

[Adam Topaz]

One can use this:
https://leanprover-community.github.io/mathlib_docs/category_theory/monoidal/Mod.html#Mod

[Heather Macbeth]

@Adam Topaz I am glad to hear that people have found a suitable theory for this. Can you explain the terminology? Is a Lie group a monoid object in the category of smooth manifolds?

[Adam Topaz]

A Lie monoid (is that a thing?) is a monoid object in the category of manifolds. A Lie group is a group object in the category of manifolds.

[Adam Topaz]

etc.

[Heather Macbeth]

Mathlib does have Lie monoids, although there was some debate

[Heather Macbeth]

Adam Topaz said:

A Lie group is a group object in the category of manifolds.

So one still has to prove this fact, right?

[Heather Macbeth]

And the idea is that then one gets access to a family of general theorems about structure-preserving group actions?

[Adam Topaz]

Heather Macbeth said:

Adam Topaz said:

A Lie group is a group object in the category of manifolds.

So one still has to prove this fact, right?

This is "the definition" :)

[Heather Macbeth]

Well, we have another definition docs#lie_group, and need some glue between them :)

[Adam Topaz]

Do we have "the category of manifolds" in mathlib?

[Heather Macbeth]

https://en.wikipedia.org/wiki/Lord_Kitchener_Wants_You

[Adam Topaz]

:expressionless:

[Heather Macbeth]

If this is a serious proposal, then a good test case would be to redefine docs#topological_group as a group object in the category of topological spaces.

[Adam Topaz]

Yeah, this should be easier.

[Heather Macbeth]

Has anything like this been done in mathlib before? That is, to make a "real-life" definition by invoking category theory?

[Heather Macbeth]

I would be very curious to know whether something "practical" like Floris' construction of Haar measure is unaffected by switching to a category-theoretic definition of topological group.

[Adam Topaz]

I can't think of an example. But it's usually not as good as a "standard" definition, because of universe issues.

[Heather Macbeth]

I see. This is a very naive question, but if it can't be used for such things, then what is the purpose of the category theory library?

[Heather Macbeth]

Is it to provide a sanity check that the definitions (given the concrete way) are correct?

[Adam Topaz]

Oh, it can certainly be used. Here's an example of what I mean.
Suppose I want to define monoids. I can define the objects themselves as a type with extra data, etc., or I can define them as monoid objects in the category Type u for a fixed universe u. Now when I go to define morphisms of monoids, I can define them as functions satsifying assumptions in the first case, or I can define them as morphisms in the category Type u which satisfy some conditions in terms of commuting diagrams. The difference is that with the first example, I can define morphisms of monoids whose underlying type has different universes, while in the second case you can only have the two monoids coming from the same universe since the thing which underlies a morphism of monoids is a morphism in the category Type u itself.

Long story short -- if you don't care about universes, then either approach is fine.

[Heather Macbeth]

But given that mathlib philosophy is to care about universes, we can never use the category theory approach, right?

[Johan Commelin]

I haven't work on the flat module project for a while. But when I was thinking about it recently, I realized that I wanted an induction principle for the category of R-modules, and that would probably simplify my proofs drastically.

[Johan Commelin]

It is true that there would be some universe restrictions, but those can be dealt with in a separate part of the proof.

[Johan Commelin]

Basically, use ulift to put everything in 1 universe, and then apply some machinery from category theory.

[Johan Commelin]

Not optimal, but ey! :smile:

[Adam Topaz]

:) This stuff isn't a problem in Coq right? They have cumulative universes?

[Kevin Buzzard]

When Amelia was working on tensor algebras she observed that the construction using quotients was quite universe-flexible, but when she made a second construction using sigma types she had to put the ring and the module into the same universe. I tried using ulift to get around this but when I found that lean didn't seem to know that if R was a ring then ulift R was too, I told her that I wouldn't be at all bothered if R and M were in the same universe, because I've spent 30 years of my life thinking that there _was_ only one universe and it didn't stop me doing the p-adic Langlands program

[Kevin Buzzard]

Heather asks (and Mario has also raised this issue several times) what the point of the category theory library is if it enables us to do stuff but only under some universe restrictions. One might conversely ask what the point of more than one universe is, given that mathematicians like Heather probably will never need them to do anything she's interested in.

[Oliver Nash]

I'd actually love to find a good excuse to use the category theory library but for what it's worth in the case of the lemma at the top of this thread I think I'm going to go with something like:

import order.preorder_hom
import logic.function.iterate

variables {α : Type*} [semilattice_sup α]

open function

lemma preorder_hom.iterate_sup_le_sup_iff (f : α →ₘ α) (n : ℕ) :
  (∀ n₁ n₂ a₁ a₂, f^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (f^[n₁] a₁) ⊔ (f^[n₂] a₂)) ↔
  (∀ a₁ a₂, f (a₁ ⊔ a₂) ≤ (f a₁) ⊔ a₂) :=
begin
  split; intros h,
  { exact h 1 0, },
  { intros n₁ n₂ a₁ a₂, have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ (f^[n] a₁) ⊔ a₂,
    { intros n, induction n with n ih; intros a₁ a₂,
      { refl, },
      { calc f^[n + 1] (a₁ ⊔ a₂) = (f^[n] (f (a₁ ⊔ a₂))) : iterate_succ_apply f n _
                             ... ≤ (f^[n] ((f a₁) ⊔ a₂)) : f.monotone.iterate n (h a₁ a₂)
                             ... ≤ (f^[n] (f a₁)) ⊔ a₂ : ih _ _
                             ... = (f^[n + 1] a₁) ⊔ a₂ : by rw ← iterate_succ_apply, }, },
    calc f^[n₁ + n₂] (a₁ ⊔ a₂) = (f^[n₁] (f^[n₂] (a₁ ⊔ a₂))) : iterate_add_apply f n₁ n₂ _
                           ... = (f^[n₁] (f^[n₂] (a₂ ⊔ a₁))) : by rw sup_comm
                           ... ≤ (f^[n₁] ((f^[n₂] a₂) ⊔ a₁)) : f.monotone.iterate n₁ (h' n₂ _ _)
                           ... = (f^[n₁] (a₁ ⊔ (f^[n₂] a₂))) : by rw sup_comm
                           ... ≤ (f^[n₁] a₁) ⊔ (f^[n₂] a₂) : h' n₁ a₁ _, },
end