subgroup of subgroup of...

Stream: general

[Kenny Lau]

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

[Kevin Buzzard]

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]

yes but I want an infinite chain of subgroups

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

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

[Kyle Miller]

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]

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]

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

[Mario Carneiro]

or a monotone function, if you want an infinite sequence

[Kyle Miller]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

in this case the family is indexed by nat

[Mario Carneiro]

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]

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]

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]

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]

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]

you might have some type equalities to wrangle with that definition