Zulip Chat Archive

Stream: maths

Topic: Homeless lemma


view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jan 19 2021 at 21:38):

Absolutely agreed on using mul_action, great point.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Jan 19 2021 at 21:40):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:17):

docs#category_theory.End

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:20):

I'll sketch some code...

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:20):

1 sec

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:32):

Oh, I see....

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:32):

Sorry, I misunderstood the question.

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:32):

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

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:33):

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

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:33):

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

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:37):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 20 2021 at 03:57):

etc.

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:03):

Mathlib does have Lie monoids, although there was some debate

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:05):

Adam Topaz said:

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

So one still has to prove this fact, right?

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Jan 20 2021 at 04:06):

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" :)

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:08):

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

view this post on Zulip Adam Topaz (Jan 20 2021 at 04:09):

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

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:10):

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

view this post on Zulip Adam Topaz (Jan 20 2021 at 04:11):

:expressionless:

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 20 2021 at 04:20):

Yeah, this should be easier.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:26):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 20 2021 at 04:35):

Not optimal, but ey! :smile:

view this post on Zulip Adam Topaz (Jan 20 2021 at 04:35):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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