## Stream: maths

### Topic: Homeless lemma

#### Oliver Nash (Jan 19 2021 at 21:31):

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 (Jan 19 2021 at 21:35):

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 (Jan 19 2021 at 21:36):

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 (Jan 19 2021 at 21:38):

Absolutely agreed on using mul_action, great point.

#### Heather Macbeth (Jan 19 2021 at 21:38):

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 (Jan 19 2021 at 21:39):

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

#### Heather Macbeth (Jan 19 2021 at 21:40):

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

#### Oliver Nash (Jan 19 2021 at 21:41):

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 (Jan 19 2021 at 21:42):

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 (Jan 19 2021 at 21:46):

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 (Jan 20 2021 at 03:16):

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 (Jan 20 2021 at 03:17):

docs#category_theory.End

#### Adam Topaz (Jan 20 2021 at 03:18):

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 (Jan 20 2021 at 03:20):

@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 (Jan 20 2021 at 03:20):

I'll sketch some code...

1 sec

#### Adam Topaz (Jan 20 2021 at 03:28):

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 (Jan 20 2021 at 03:29):

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 (Jan 20 2021 at 03:30):

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 (Jan 20 2021 at 03:31):

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.

Oh, I see....

#### Adam Topaz (Jan 20 2021 at 03:32):

Sorry, I misunderstood the question.

#### Adam Topaz (Jan 20 2021 at 03:32):

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

#### Adam Topaz (Jan 20 2021 at 03:33):

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

#### Adam Topaz (Jan 20 2021 at 03:33):

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

#### Heather Macbeth (Jan 20 2021 at 03:54):

@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 (Jan 20 2021 at 03:57):

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.

etc.

#### Heather Macbeth (Jan 20 2021 at 04:03):

Mathlib does have Lie monoids, although there was some debate

#### Heather Macbeth (Jan 20 2021 at 04:05):

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

So one still has to prove this fact, right?

#### Heather Macbeth (Jan 20 2021 at 04:05):

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

#### Adam Topaz (Jan 20 2021 at 04:06):

Heather Macbeth 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 (Jan 20 2021 at 04:08):

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

#### Adam Topaz (Jan 20 2021 at 04:09):

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

#### Heather Macbeth (Jan 20 2021 at 04:10):

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

:expressionless:

#### Heather Macbeth (Jan 20 2021 at 04:20):

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 (Jan 20 2021 at 04:20):

Yeah, this should be easier.

#### Heather Macbeth (Jan 20 2021 at 04:21):

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

#### Heather Macbeth (Jan 20 2021 at 04:23):

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 (Jan 20 2021 at 04:24):

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

#### Heather Macbeth (Jan 20 2021 at 04:26):

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 (Jan 20 2021 at 04:26):

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

#### Adam Topaz (Jan 20 2021 at 04:31):

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 (Jan 20 2021 at 04:32):

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

#### Johan Commelin (Jan 20 2021 at 04:34):

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 (Jan 20 2021 at 04:34):

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 (Jan 20 2021 at 04:35):

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

#### Johan Commelin (Jan 20 2021 at 04:35):

Not optimal, but ey! :smile:

#### Adam Topaz (Jan 20 2021 at 04:35):

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

#### Kevin Buzzard (Jan 20 2021 at 07:46):

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 (Jan 20 2021 at 07:48):

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 (Jan 20 2021 at 11:13):

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


Last updated: May 09 2021 at 09:11 UTC