Wreath products

Stream: new members

[Bernhard Reinke]

Hi, I am interested in implementing wreath products in lean (currently lean 3). I have a small working definition for unrestricted wreath products reducing it to a semidirect product such as

variables (A : Type*) (B : Type*) (L : Type*) [group A] [group B] [mul_action A L]

[...]

def wreath_product_1 := semidirect_product (L → B) A wreath_product.φ

notation B` ≀[`:35 L:35`] `:0 A :35 := wreath_product_1 A B L

where ẁreath_product.φ : A →* mul_aut (L → B) given by the reindexing action λ (a : A) (f : L → B) (l: L), f (has_smul.smul a⁻¹ l). Most of the file is currently showing that this definition lifts to A →* mul_aut (L → B).

I also want to consider restricted wreath products. But here I am not sure how to deal with the type classes: semidirect products are defined for (multiplicative) groups, but finsupp is defined for has_zero B. I also want to consider groups B that are noncommutative, so I am reluctant to use additive notation for B. I saw that @Sky Wilshaw was thinking of generalizing finsupp. Has there been any progress there? Any good suggestions on how to proceed? I don't really want to reinvent the wheel but I also don't know how to glue the current definitions together.

[Sky Wilshaw]

I stopped working on that PR to give more effort to porting mathlib3 to mathlib4. I don't intend to continue with that PR, I might submit something similar for mathlib4 after the port.

[Eric Wieser]

Could you use docs#free_monoid instead of finsupp?

[Bernhard Reinke]

I decided to side step restricted wreath products for now, one thing I want to work towards to is the description of the p-Sylow group of Sym(p^k) as an k-times iterated wreath product of the cyclic group of order p. See the stub.

At the moment I am still struggling to define iterated wreath products correctly, again because of type class issues. Is it possible to define types inductively together with their instance of a certain type class?

For wreath products, I define a structure

section bare_def

variables (A : Type*) (B : Type*) (L : Type*)

@[ext]
structure wreath_product :=
(left: L → B) (right : A)

end bare_def

and show a group instance

section group

variables (A : Type*) (B : Type*) (L : Type*) [group A] [group B] [mul_action A L]

instance wreath_product_group : group (wreath_product A B L) := [...]

end group

notation B` ≀[`:35 L:35`] `:0 A :35 := wreath_product A B L

I want to define iterated wreath products the following way:

def iterated_wreath_product (G : Type*) : ℕ → Type*
| zero := triv_group
| (succ n) := iterated_wreath_product n ≀[G] G

lemma iterated_wreath_product_zero (G : Type*) : iterated_wreath_product G zero = triv_group := rfl

lemma iterated_wreath_product_succ (G : Type*) (n : ℕ) :
iterated_wreath_product G (succ n) = (iterated_wreath_product G n ≀[G] G) := rfl


instance (G : Type*) [group G] (n : ℕ) : group (iterated_wreath_product G n) :=
begin
  induction n with n ih,
  {
    rw iterated_wreath_product_zero,
    apply_instance
  },
  {
    rw iterated_wreath_product_succ,
    sorry,
  }
end

here triv_group is a unit type with the trivial group structure. I would like to construct the group structure inductively. But in the inductive step,
if I try instead of the sorrythe tactic apply wreath_product_groupI get the error

invalid apply tactic, failed to synthesize type class instance for
  group (iterated_wreath_product G n)
state:
case nat.succ
G : Type,
_inst_1 : group G,
n : ℕ,
ih : group (iterated_wreath_product G n)
⊢ group (iterated_wreath_product G n ≀[G] G)

So it seems I cannot use the type class instance for the induction hypothesis. Is there some nice way around this?

[Bernhard Reinke]

I think I found an OK solution, by the defining the group structure on wreath products like

variables (A : Type*) (B : Type*) (L : Type*) [group A] [mul_action A L]
def wreath_product_group_explicit (h : group B) : group (wreath_product A B L) := [...]

and then add an instance as

variables (A : Type*) (B : Type*) (L : Type*) [group A] [group B] [mul_action A L]

instance : group (wreath_product A B L) := wreath_product_group_explicit A B L infer_instance

then it is possible to use the inductively constructed group structure

[Junyan Xu]

Maybe you can just do

    rw iterated_wreath_product_succ,
    resetI, apply_instance,

or if you make iterated_wreath_product a @[reducible] def then maybe you don't even need the rewrite.

I think something like this comes up in docs#polynomial.splitting_field (where we iteratively adjoin roots), but IIRC there situation is more complicated because we want an algebra instance over the base field.

[Eric Wieser]

I think I asked something similar a long time ago about iteratively defining tensor powers

[Eric Wieser]

It's perhaps worth noting that you can get the trivial group more easily with

-- could use `unit` directly if you're fine with `0 : unit` existing
@[derive [comm_group, unique, fintype, decidable_eq]]
def trivial_group := unit

[Bernhard Reinke]

I didn't know about resetI, thanks! What does @[reducible] defdo exactly?

[Eric Wieser]

It allows typeclass search to see through the definition

[Eric Wieser]

Generally you would use reducible if you're just coming up with a shorthand name, and derive if you want your new name to have differences in behavior (by choosing to not derive certain things)