Zulip Chat Archive

Stream: maths

Topic: Fixed points of endomorphism form substructure


view this post on Zulip Keefer Rowan (May 27 2020 at 14:08):

I don't think this is anywhere in the library (note this is inspired by the complex inner product issue), but I want to add for a bunch of the algebraic structures (monoid, group, ring, field) that the fixed points of an endomorphism ff, form a sub-x (where x is monoid, group, ring, field resp). Here's the one for monoid:

/-- The set of fixed points of an endomorphism `f` of a monoid `M` is a submonoid of `M`. -/
@[to_additive is_add_submonoid_fixed "The set of fixed points of an endomorphism `f` of an `add_monoid` `M` is a `add_submonoid` of `M`. "]
lemma is_submonoid_fixed (f : M →* M) : is_submonoid (fixed_points f) :=
begin
  split,
    {exact monoid_hom.map_one f},
  intros a b a_def b_def,
  change f (a * b) = a *b,
  rw monoid_hom.map_mul,
  change f a = a at a_def,
  change f b = b at b_def,
  simp *
end

It is in the file group_theory/submonoid.lean and is right under this lemma (on which the formatting was based):

/-- The union of an indexed, directed, nonempty set of submonoids of a monoid `M` is a submonoid
    of `M`. -/
@[to_additive is_add_submonoid_Union_of_directed "The union of an indexed, directed, nonempty set of `add_submonoid`s of an `add_monoid` `M` is an `add_submonoid` of `M`. "]
lemma is_submonoid_Union_of_directed {ι : Type*} [ : nonempty ι]
  (s : ι  set M) [ i, is_submonoid (s i)]
  (directed :  i j,  k, s i  s k  s j  s k) :
  is_submonoid (i, s i) := sorry

Is this all good?

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:10):

I think is_submonoid is deprecated

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:11):

you want to use submonoid

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:13):

import group_theory.submonoid order.fixed_points

open order

def submonoid_fixed {M : Type*} [monoid M] (f : M →* M) :
  submonoid M :=
{ carrier := fixed_points f,
  one_mem' := monoid_hom.map_one f,
  mul_mem' := begin
    intros a b a_def b_def,
    change f (a * b) = a *b,
    rw monoid_hom.map_mul,
    change f a = a at a_def,
    change f b = b at b_def,
    simp *
  end }

Same proof, different implementation

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:17):

Someone better than me at automation will probably be able to make simp do the tactic proof all in one go

view this post on Zulip Keefer Rowan (May 27 2020 at 14:18):

Cool, thanks. I was wondering how to state it in the bundled case.

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:18):

Note that it's a definition, not a theorem, because of the carrier

view this post on Zulip Keefer Rowan (May 27 2020 at 14:20):

Yeah, that's why I couldn't figure out the correct statement at first, but it makes sense when you show it like that.

view this post on Zulip Keefer Rowan (May 27 2020 at 14:20):

For subgroups, subrings, and subfields, it's still all unbundled, right?

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:22):

I think subgroups are bundled now. For the others, if you could bundle them first then that would be great :-) Bundling PR's are really good fun. Both Jason KY and Amelia Livingston (UG Imperial mathematicians) had early PR's which were just bundling unbundled structures and they both learnt a lot.

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:22):

I'll be bundling normal subgroups in June and then attempting to refactor quotient groups based on them

view this post on Zulip Keefer Rowan (May 27 2020 at 14:23):

Looking at the group_theory/subgroups.lean, I don't see any bundled subgroup. Is there anywhere else worth looking? On a different branch?

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:24):

For some reason Jason (aka Kexing Yang) made a new file bundled_subgroup and the PR police let him do it

view this post on Zulip Keefer Rowan (May 27 2020 at 14:25):

I see that. I guess to avoid breaking all the dependencies? How should one go about bundling? Replace the unbundled definition, redo all the theorems, and fix all broken dependencies?

view this post on Zulip Keefer Rowan (May 27 2020 at 14:25):

Is there a good way to find all broken dependencies?

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:25):

Removing the unbundled definition is the hard part

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:26):

I do not encourage learner undergraduates to do that. Basically what is going on is that for months people were saying "uuh, the correct thing to do is to bundle submodules, subgroups, group homs, ring homs etc, all at once, and to remove the unbundled ones, and it will be a monster PR" and of course nobody would do it

view this post on Zulip Keefer Rowan (May 27 2020 at 14:27):

What would you recommend doing?

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:27):

but then I began to need it, so I started encouraging people to do the bundling but leave the unbundling alone, because then there will be a far more inefficient process involving much smaller PR's but at least I'd be able to use bundled group homs for the stuff I wanted to do with them

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:29):

Well, first talk to @Yury G. Kudryashov and @Johan Commelin because they know the state of the art better than me. The question is what is next on the list of unbundled things which should be bundled, and the next question is whether bundling them is a good idea (for which I vote yes, but it would be interesting to have a poll)

view this post on Zulip Kevin Buzzard (May 27 2020 at 14:36):

PS I think you're also running into lean#197 , your goals shouldn't mention set.mem and this is hurting automation I think

view this post on Zulip Keefer Rowan (May 27 2020 at 14:50):

Question 1) What are the advantages of bundling that makes it worthwhile do all the work to change to library?
Question 2) How does one track all the dependencies without opening every file in Mathlib?

view this post on Zulip Johan Commelin (May 27 2020 at 14:54):

Without bundling, you need to find type classes all the time. And this didn't always work as expected.

view this post on Zulip Yury G. Kudryashov (May 27 2020 at 15:50):

We have meq_locus

view this post on Zulip Keefer Rowan (May 27 2020 at 16:11):

So what's the deal with fixing bundling? Is that something worth working on? Right now we have bundled and unbundled for both monoids and subgroups. Is the goal to kill off the unbundled?

view this post on Zulip Yury G. Kudryashov (May 27 2020 at 16:32):

As far as I understand, the goal is to kill unbundled homs and substructures.

view this post on Zulip Yury G. Kudryashov (May 27 2020 at 16:34):

Because in many cases we can construct bundled objects right away instead of relying on classes. At the same time [monoid M] etc are not deprecated because we don't want to write nat.monoid --> M


Last updated: May 18 2021 at 06:15 UTC