## Stream: general

### Topic: subgroup of subgroup of...

#### Kenny Lau (Aug 23 2020 at 07:55):

Can I state the theorem "... of the subgroup of the subgroup of ... G" is a subgroup of G?

#### Kevin Buzzard (Aug 23 2020 at 08:18):

import group_theory.subgroup

example (G : Type) [group G] (H : subgroup G) (K : subgroup H) : subgroup G :=
subgroup.map ((by library_search) : H →* G) K


#### Kenny Lau (Aug 23 2020 at 08:38):

yes but I want an infinite chain of subgroups

Oh!

#### Kevin Buzzard (Aug 23 2020 at 08:55):

Of course you can still do it but maybe you want to set things up differently

#### Kyle Miller (Aug 23 2020 at 09:53):

I wanted a similar type of dependent sequences in another context, but I couldn't figure out how to get it to work.

Here's one thing I tried:

/--
A list of groups, where each is a subgroup of the previous
-/
inductive subgroup_chain : Π (G : Type u) [group G], Type (u + 1)
| group (G : Type u) [group G] : subgroup_chain G
| subgroup {G : Type u} [group G] (G' : subgroup G) (tail : subgroup_chain G') : subgroup_chain G

/--
Drop last subgroup off the subgroup_chain.  FAILS: "dependent pattern matching result is not a constructor application"
-/
def sc_init : Π {G : Type u} [h : group G], @subgroup_chain G h → @subgroup_chain G h
| _ _ (@subgroup_chain.group G h) := @subgroup_chain.group G h
| _ _ (@subgroup_chain.subgroup G h G' (@subgroup_chain.group _ _)) := @subgroup_chain.group G h
| _ _ (@subgroup_chain.subgroup G h G' tail) := @subgroup_chain.subgroup G h G' (sc_init tail)

structure subgroup_sequence (G : Type u) [group G] :=
(f : ℕ → subgroup_chain G)
(prop₁ : f 0 = subgroup_chain.group G)
(prop₂ : ∀ n, f n = sc_init (f (n + 1)))


#### Kyle Miller (Aug 23 2020 at 09:55):

I think what I was attempting is to simulate a coinductive definition with inductive types. Ideally this would be a stream of subgroups (a.k.a. an infinite list).

#### Mario Carneiro (Aug 23 2020 at 09:55):

Isn't it possible to just have a chain in the partial order of subgroups?

#### Mario Carneiro (Aug 23 2020 at 09:56):

or a monotone function, if you want an infinite sequence

#### Kyle Miller (Aug 23 2020 at 09:58):

In the other context, I found some type that everything could be a set in, solving the problem like you suggest, but I'm still wondering how to set up this kind of recursive definition.

#### Kevin Buzzard (Aug 23 2020 at 10:05):

In the coq odd order paper some technicalities were solved by making all groups subgroups of an ambient big group. But this trick cannot be used for eg rings

#### Mario Carneiro (Aug 23 2020 at 10:24):

I won't say this is the best implementation, but it fixes all the errors and avoids the universe bump:

import group_theory.subgroup

universe u
/--
A list of groups, where each is a subgroup of the previous
-/
def subgroup_chain' : ℕ → Π (G : Type u) [group G], Type u
| 0 G _ := punit
| (n+1) G _ := by exactI Σ (G' : subgroup G), subgroup_chain' n G'

def subgroup_chain (G : Type u) [group G] : Type u := Σ n, subgroup_chain' n G

def subgroup_chain.nil {G} [group G] : subgroup_chain G := ⟨0, ⟨⟩⟩
def subgroup_chain.cons {G : Type u} [group G]
(G' : subgroup G) : subgroup_chain G' → subgroup_chain G
| ⟨n, C⟩ := ⟨n+1, G', C⟩

def subgroup_chain.init' : ∀ n {G : Type u} [group G], by exactI subgroup_chain' n G → subgroup_chain G
| (n+2) G _ ⟨G', C⟩ := by exactI subgroup_chain.cons G' (subgroup_chain.init' (n+1) C)
| _ _ _ _ := by exactI subgroup_chain.nil

/--
Drop last subgroup off the subgroup_chain.  FAILS: "dependent pattern matching result is not a constructor application"
-/
def subgroup_chain.init {G : Type u} [group G] : subgroup_chain G → subgroup_chain G
| ⟨n, G'⟩ := subgroup_chain.init' n G'

structure subgroup_sequence (G : Type u) [group G] :=
(f : ℕ → subgroup_chain G)
(prop₁ : f 0 = subgroup_chain.nil)
(prop₂ : ∀ n, f n = subgroup_chain.init (f (n + 1)))


#### Kyle Miller (Aug 23 2020 at 23:13):

I tried abstracting out the pattern, which is that these are lists whose elements have types that are constructed from the previous element in some way. There is a type α, a function tcons of that takes terms of α to types that index allowable next terms in the list, and a function mk that takes these index terms back to terms of α.

import group_theory.subgroup
import tactic

universes u v

section chains

def chain_tcons (α : Type (u+1)) := α → Type u
def chain_mk {α : Type (u+1)} (cons : chain_tcons α) := Π ⦃x : α⦄, cons x → α

variables {α : Type (u+1)} (tcons : chain_tcons α) (mk : chain_mk tcons)

def chain' : ℕ → Π (x : α), Type u
| 0 x := punit
| (n+1) x := Σ (x' : tcons x), chain' n (mk x')

def chain (x : α) : Type u := Σ (n : ℕ), chain' tcons mk n x

variables {tcons} {mk}
def chain.nil {x : α} : chain tcons mk x := ⟨0, punit.star⟩
def chain.cons {x : α} (x' : tcons x) : chain tcons mk (mk x') → chain tcons mk x
| ⟨n, C⟩ := ⟨n+1, x', C⟩
def chain.init' : Π (n : ℕ) {x : α}, chain' tcons mk n x → chain tcons mk x
| (n+2) x ⟨x', C⟩ := chain.cons x' (chain.init' (n+1) C)
| _ _ _ := chain.nil
def chain.init {x : α} : chain tcons mk x → chain tcons mk x
| ⟨n, C⟩ := chain.init' n C

variables (tcons) (mk)
structure chain_seq (x : α) :=
(f : ℕ → chain tcons mk x)
(prop₁ : f 0 = chain.nil)
(prop₂ : ∀ (n : ℕ), f n = chain.init (f (n + 1)))

end chains

structure Group :=
(G : Type u)
(s : group G)

@[reducible]
def subgroup_tcons : chain_tcons Group := λ G, @subgroup G.G G.s
def subgroup_mk : chain_mk subgroup_tcons := λ x G', {G := G', s := by apply_instance}


#### Kyle Miller (Aug 23 2020 at 23:14):

I don't feel like I fully understand the pattern yet, but the code certainly type checks :smile:

#### Mario Carneiro (Aug 23 2020 at 23:17):

By the way, the general technique for avoiding universe bumps in inductives is to realize that not all types can be used in the recursion, only those "derived" from the input by some "small" (i.e. in Type u) indexed family

#### Mario Carneiro (Aug 23 2020 at 23:17):

in this case the family is indexed by nat

#### Mario Carneiro (Aug 23 2020 at 23:26):

here's another example:

universe u

inductive rose_tree : Type u → Type (u+1) -- bad
| leaf {α} : α → rose_tree α
| node {α} : rose_tree (α × α) → rose_tree α

def rose_type : ℕ → Type u → Type u
| 0 α := α
| (n+1) α := rose_type n (α × α)

def rose_tree' (α : Type u) : Type u := -- good
Σ n, rose_type n α

def rose_tree'.leaf {α} (a : α) : rose_tree' α := ⟨0, a⟩
def rose_tree'.node {α} (a : α) : rose_tree' (α × α) → rose_tree' α
| ⟨n, a⟩ := ⟨n+1, a⟩


#### Mario Carneiro (Aug 23 2020 at 23:27):

the fact that it is a def after the transformation isn't the important part, it is the fact that rose_tree' only quantifies over nat instead of Type u

#### Mario Carneiro (Aug 23 2020 at 23:30):

The only time this isn't possible is when you really take advantage of that type quantifier, as in src#pSet, and that's when you get the really big inductives that properly require a universe bump

#### Kyle Miller (Aug 23 2020 at 23:33):

Thanks, I was wondering if the nat you introduced was the key here.

The other setup I was looking at was defining a sequence of graphs, each having a vertex set derived from the previous, something like

inductive deriv_verts {α : Type*} [simple_graphs α] (G : α) :
| incl (v : V G)
| join (e : (sym2 (V G)) (h : ¬∃ (w : V G), ∀ (v ∈ e), v ~ w)

def deriv {α : Type*} [simple_graphs α] (G : α) : simple_graph_on (deriv_verts G) :=
sorry

-- then define a function f : ℕ → graphs somehow where f (n + 1) = deriv (f n)


It turns out all the graphs can be thought of as being subgraphs of a complete graph on some other type, so it doesn't really matter, but I thought it was interesting how it wasn't clear how to reign in the universes.

#### Kyle Miller (Aug 24 2020 at 00:12):

I guess this is another way to set it up:

structure Group :=
(G : Type u)
(s : group G)

def subgroups (G : Group) : set Group := {G' : Group | ∃ (g' : @subgroup G.G G.s), G' = ⟨g', by apply_instance⟩}

structure subgroup_chain (G : Group) :=
(f : ℕ → Group)
(prop₁ : f 0 = G)
(prop₂ : ∀ n, f (n + 1) ∈ subgroups (f n))


This simplifies things in that it doesn't need to represent the infinite chain as a limit of finite chains.

#### Mario Carneiro (Aug 24 2020 at 00:18):

you might have some type equalities to wrangle with that definition

Last updated: May 16 2021 at 21:11 UTC