Invariant subMonoid/AddMonoid/Module

Stream: Is there code for X?

[Kevin Buzzard]

import Mathlib

variable {G : Type*} [Group G] {A : Type*} [AddCommMonoid A]
    [DistribMulAction G A] {g : G} {V : Subgroup G}

#synth AddCommMonoid {a : A // ∀ γ ∈ V, γ • a = a} -- fails

Do we have the type of invariants of a group action, as a monoid or submonoid? Similarly if [Ring R] [Module R A] [SMulCommClass R G A] do we have Module R {a : A // ∀ γ ∈ V, γ • a = a} in some form? I know we have docs#groupCohomology.H0 but honestly I am reluctant to drag category theory into this.

[Edward van de Meent]

afaict, no

[Edward van de Meent]

or actually, FixedPoints.subgroup?

[Edward van de Meent]

specifically, the incantation seems to be FixedPoints.addSubmonoid V A

[Edward van de Meent]

import Mathlib

variable {G : Type*} [Group G] {A : Type*} [AddCommMonoid A]
    [DistribMulAction G A] {g : G} {V : Subgroup G}

#synth AddCommMonoid (FixedPoints.addSubmonoid V A) -- success

example (a:A) : a ∈ FixedPoints.addSubmonoid V A ↔ ∀ v ∈ V, v • a = a := by
  simp? says simp only [FixedPoints.mem_addSubmonoid, Subtype.forall, Subgroup.mk_smul]

[Jireh Loreaux]

When I read the title, I thought you meant docs#Module.End.invtSubmodule. FixedPoints definitely seems like the appropriate name for your object.

[Yury G. Kudryashov]

We have docs#LinearMap.eqLocus which you can use with id as one of the arguments.

[Yury G. Kudryashov]

Sorry, this is for 1 map, not for a group action.

[Kevin Buzzard]

docs#FixedPoints.addSubmonoid

[Michał Mrugała]

Do we have a proof that this is the 0th cohomology group?

[Kevin Buzzard]

No but it would be a nice exercise to add. You'd have to choose whether to make it an isomorphism in the category or an apppropriate equiv.

[Kevin Buzzard]

I realise that I am in a situation where I really don't want the fixed points as a submonoid, I want them as a monoid. Do you think that this sort of code would be appropriate for mathlib:

import Mathlib.Algebra.Ring.Action.Submonoid

variable (M α : Type*) [Monoid M] [AddMonoid α] [DistribMulAction M α]

def FixedPoints.AddMonoid : Type _ := FixedPoints.addSubmonoid M α

instance : AddMonoid (FixedPoints.AddMonoid M α) :=
  inferInstanceAs <| AddMonoid (FixedPoints.addSubmonoid M α)

and similar definitions for AddGroup, Module etc. Or should I keep it in FLT? I have had bad experiences with typeclass inference when treating terms as types via ↥ (for example the refactor of docs#NumberField.RingOfIntegers to be a type rather than a term, even though it's defined as a the coercion-to-sort of a term, solved a lot of timeouts). I know that I want my invariants to be types; it's like docs#DedekindDomain.FiniteAdeleRing where the main object (the finite adele ring) is defined as a subobject of an auxiliary object K_hat R K, but the main object has all the structure. Here I am defining spaces of modular forms which should really be types as they will need a lot of API, but they're fixed points of a group action in my context so they are subobjects of an auxiliary thing which we don't care about once we've made the API.

[Eric Wieser]

I think that would be reasonable if the type was just FixedPoints

[Eric Wieser]

(docs#FixedPoints just in case)

[Kevin Buzzard]

So something like this?

import Mathlib

-- or def?
abbrev FixedPoints (M A : Type*) [SMul M A] : Type _ :=
  {a : A // ∀ m : M, m • a = a}

namespace FixedPoints

variable {M A : Type*}

@[ext]
lemma ext [SMul M A] (a b : FixedPoints M A) (h : a.1 = b.1) : a = b := by
  cases a; cases b; subst h; rfl

instance addZeroClass [AddZeroClass A] [DistribSMul M A] : AddZeroClass (FixedPoints M A) where
  zero := ⟨0, smul_zero⟩
  add a b := ⟨a.1 + b.1, by
    intro m
    rw [smul_add m a.1 b.1, a.2 m, b.2 m]⟩
  zero_add a := by
    ext
    exact zero_add a.1
  add_zero a := by
    ext
    exact add_zero a.1

lemma zero_def [AddZeroClass A] [DistribSMul M A] : (0 : FixedPoints M A) = ⟨0, smul_zero⟩ := rfl

lemma coe_add [AddZeroClass A] [DistribSMul M A] (a b : FixedPoints M A) :
    (a + b : FixedPoints M A).1 = a.1 + b.1 := rfl

instance addMonoid [AddMonoid A] [DistribSMul M A] : AddMonoid (FixedPoints M A) where
  __ := addZeroClass
  add_assoc a b c := by
    ext
    exact add_assoc a.1 b.1 c.1
  nsmul n a := ⟨AddMonoid.nsmul n a.1, by
    intro m
    induction n with
    | zero =>
      rw [AddMonoid.nsmul_zero]
      exact smul_zero m
    | succ n IH =>
      rw [AddMonoid.nsmul_succ, smul_add, IH, a.2]
  ⟩
  nsmul_zero a := by
    simp [zero_def]
  nsmul_succ n a := by
    ext
    simp [succ_nsmul, coe_add]

instance addCommMonoid [AddCommMonoid A] [DistribSMul M A] : AddCommMonoid (FixedPoints M A) where
  __ := addMonoid
  add_comm a b := by
    ext
    exact add_comm a.1 b.1

instance subNegMonoid [SubNegMonoid A] [DistribSMul M A] : SubNegMonoid (FixedPoints M A) where
  __ := addMonoid
  neg a := ⟨-a.1, sorry⟩
  zsmul n a := ⟨SubNegMonoid.zsmul n a.1, sorry⟩
  zsmul_zero' a := sorry
  zsmul_succ' n a := sorry
  zsmul_neg' n a := sorry

-- ...

instance module {R : Type*} [Semiring R] [AddCommMonoid A] [Module R A] [Monoid M]
  [DistribMulAction M A] [SMulCommClass M R A] [Module R A] : Module R (FixedPoints M A) := sorry

-- ...

[Yury G. Kudryashov]

A few suggestions:

• please use def, not abbrev;
• please put it in the MulAction namespace, because
  • we will need an additive version
  • it makes sense to study fixed points of a single map.

[Yury G. Kudryashov]

If you use a Subtype, then you can get AddMonoid etc instances "for free" by forcing defeq to docs#FixedPoints.addSubmonoid etc

[Eric Wieser]

I think it might need to be abbrev unless you also promise to never write .1

[Eric Wieser]

Otherwise the .1 is ill-typed

[Kevin Buzzard]

I changed abbrev to def and nothing broke?

[Eric Wieser]

Here's another approach:

import Mathlib

structure FixedPointsType (M A : Type*)

def fixedPoints (M A : Type*) [SMul M A] : FixedPointsType M A := ⟨⟩

instance (M A : Type*) [SMul M A] : SetLike (FixedPointsType M A) A where
  coe _ := {a : A | ∀ m : M, m • a = a}
  coe_injective' x y _ := by cases x; cases y; rfl

variable {A M}

instance [Zero A] [SMulZeroClass M A] : ZeroMemClass (FixedPointsType M A) A where
  zero_mem _ := smul_zero

instance [AddMonoid A] [DistribSMul M A] : AddSubmonoidClass (FixedPointsType M A) A where
  add_mem _ {a b} ha hb := fun m => (smul_add m a b).trans congr($(ha m) + $(hb m))

instance [Monoid M] [AddMonoid A] [DistribMulAction M A] : AddSubmonoidClass (FixedPointsType M A) A where

instance [Monoid M] [AddGroup A] [DistribMulAction M A] : AddSubgroupClass (FixedPointsType M A) A where
  neg_mem _ {_} hx := (FixedPoints.addSubgroup M A).neg_mem hx

instance [Monoid M] [Monoid A] [MulDistribMulAction M A] : SubmonoidClass (FixedPointsType M A) A where
  mul_mem _ {a b} ha hb := fun m => (smul_mul' m a b).trans congr($(ha m) * $(hb m))
  one_mem _ := smul_one

instance [Monoid M] [Semiring A] [MulSemiringAction M A] : SubsemiringClass (FixedPointsType M A) A where
instance [Monoid M] [Ring A] [MulSemiringAction M A] : SubringClass (FixedPointsType M A) A where

-- test it works: we get all the `Comm` instance for free because of the `*Class` machinery above
variable [Monoid M] [AddCommMonoid A] [DistribMulAction M A] in
#synth AddCommMonoid (fixedPoints M A)
variable [Monoid M] [CommRing A] [MulSemiringAction M A] in
#synth CommRing (fixedPoints M A)

[Eric Wieser]

This one has the nice benefit that (fixedPoints M A) can be cast to a AddSubmonoid or an AddSubgroup

[Eric Wieser]

Though it breaks being able to write fixedPoints M A = fixedPoints N A without inserting coercions

[Yury G. Kudryashov]

Eric Wieser said:

I think it might need to be abbrev unless you also promise to never write .1

Or you can use a 2-field structure (but you can't use lemmas about Subtype in this case).

[Eric Wieser]

Edited above to include all the instances up to CommRing

[Kevin Buzzard]

Eric Wieser said:

Here's another approach:

I am not clear about whether this solves the problem which I'm worried about, and I'm also not clear about whether I should be worrying about this problem.

With your approach:

variable [Monoid M] [CommRing A] [MulSemiringAction M A] in
#check Module (fixedPoints M A) (fixedPoints M A)
-- Module ↥(fixedPoints M A) ↥(fixedPoints M A) : Type u_1

#count_heartbeats in -- 6629 heartbeats
variable [Monoid M] [CommRing A] [MulSemiringAction M A] in
#synth Module (fixedPoints M A) (fixedPoints M A)

Here we still see the ↥. The ↥ is exactly what I want to get rid of, because of the awful experience we had with rings of integers of number fields, where Lean would constantly be trying to solve SMul (↥A) B with A : Subring X by searching for SMul X B (which often didn't exist, leading to very slow code and timeouts).

With my approach:

#count_heartbeats in -- 1812 heartbeats
variable [Monoid M] [CommRing A] [MulSemiringAction M A] in
#synth Module (FixedPoints M A) (FixedPoints M A)

My code is far more verbose than yours though, e.g.

instance commRing [Monoid M] [CommRing A] [MulSemiringAction M A] : CommRing (FixedPoints M A) where
  __ := subNegMonoid
  add_comm a b := by ext; push_cast; simp [add_comm]
  left_distrib a b c := by ext; push_cast; simp [left_distrib]
  right_distrib a b c := by ext; push_cast; simp [right_distrib]
  zero_mul a := by ext; push_cast; simp
  mul_zero a := by ext; push_cast; simp
  mul_assoc a b c := by ext; push_cast; simp [mul_assoc]
  neg_add_cancel a := by ext; push_cast; simp
  one_mul a := by ext; push_cast; simp
  mul_one a := by ext; push_cast; simp
  mul_comm a b := by ext; push_cast; simp [mul_comm]

I would like to go ahead with this in FLT because this construction is on the critical path to my next short-term goal, but ideally I'd like to choose the implentation which is mathlib-suitable. Any comments?

[Eric Wieser]

The verbosity is independently fixable by using Function.Injective.commRing etc

[Jireh Loreaux]

But doesn't that also run into performance issues? Or did that get fixed with the %fast_instance hack?

[Eric Wieser]

fast_instance% makes those go away

[Eric Wieser]

(and may also make lesser versions of those issues do so if used with Kevin's manual approach)

[Kevin Buzzard]

The other thing worth saying is that in my application the fixed points are modules, not monoids, so they are unlikely to be acting on something via SMul. But I could envisage people using this construction in e.g. Galois theory, where there is a constant tension between using IntermediateFields and Types in complex mathematical arguments.

[Eric Wieser]

(deleted)

[Eric Wieser]

In the galois theory case we already have docs#FixedPoints.intermediateField

[Kevin Buzzard]

Yes and this is a term, not a type, so we run into slowdowns because of the "ring of integers phenomenon"

[Eric Wieser]

My inclination would be to ignore the ↥ until you've actually written half of the code that works with the fixedpoints in the way you care about, and then see whether switching to what you've discussed in this thread makes thing faster

[Kevin Buzzard]

I don't quite understand "the way you care about" but I'm interpreting your message as "stick to coerced terms for now, and see what happens" (sorry, on a Eurostar with crappy WiFi for the next 3 hours)

[Kevin Buzzard]

(it's the perfect time for writing some Hecke algebra code without being told off for working on holiday though!)

[Junyan Xu]

Notice that we already have docs#Representation.invariants (the name was decided here).

[Edison Xie]

Michał Mrugała said:

Do we have a proof that this is the 0th cohomology group?

I need it :smiling_face_with_tear: if anyone has done it will be much appreciated... if no one else then I guess I'll have to make this one