10. Proof of the boundary-framed theorem🔗

Lemma10.1

groupuses 0used by 1✓L∃∀N

Lemma 9.1 of the paper (Coprime-kernel subdirect products).

Let A\twoheadrightarrow C and B\twoheadrightarrow C be finite epimorphisms whose kernels have coprime orders. If a subgroup J\le A\times_C B projects onto both A and B, then J=A\times_C B.

Lean code for Lemma10.1●1 theorem

theoremdefined in GQ2/FiniteGroupLemmas.lean

complete

theorem GQ2.FiniteGroup.coprime_fiber_product.{u_1, u_2, u_3} {A : Type u_1}
  {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [Finite A]
  [Finite B] (f : A →* C) (g : B →* C) (hf : Function.Surjective ⇑f)
  (hg : Function.Surjective ⇑g)
  (hcop : (Nat.card ↥f.ker).Coprime (Nat.card ↥g.ker))
  (J : Subgroup (A × B)) (hJsub : ∀ p ∈ J, f p.1 = g p.2)
  (hJA : Function.Surjective fun p => (↑p).1)
  (hJB : Function.Surjective fun p => (↑p).2) (p : A × B) :
  f p.1 = g p.2 → p ∈ J

theorem GQ2.FiniteGroup.coprime_fiber_product.{u_1,
    u_2, u_3}
  {A : Type u_1} {B : Type u_2}
  {C : Type u_3} [Group A] [Group B]
  [Group C] [Finite A] [Finite B]
  (f : A →* C) (g : B →* C)
  (hf : Function.Surjective ⇑f)
  (hg : Function.Surjective ⇑g)
  (hcop :
    (Nat.card ↥f.ker).Coprime
      (Nat.card ↥g.ker))
  (J : Subgroup (A × B))
  (hJsub : ∀ p ∈ J, f p.1 = g p.2)
  (hJA :
    Function.Surjective fun p => (↑p).1)
  (hJB :
    Function.Surjective fun p => (↑p).2)
  (p : A × B) : f p.1 = g p.2 → p ∈ J

**Lemma 9.1 (coprime-kernel subdirect product).** Let `f : A ↠ C` and `g : B ↠ C` be finite
epimorphisms whose kernels have coprime orders. A subgroup `J` of `A × B` that lies in the fibre
product `{(a,b) | f a = g b}` and projects onto both factors is the *entire* fibre product.

Proof via Goursat: `J.goursatFst ≤ ker f` and `J.goursatSnd ≤ ker g`, and Goursat's isomorphism
`A/goursatFst ≃ B/goursatSnd` gives `|goursatFst|·|ker g| = |goursatSnd|·|ker f|`.  Coprimality of
`|ker f|`, `|ker g|` then forces `ker g ≤ J.goursatSnd`, which is exactly the missing wild direction
needed to hit every fibre-product element.

Lemma10.2

groupuses 0used by 1✓L∃∀N

Lemma 9.2 of the paper (Targets with only trivial module factors).

Suppose every chief factor of L_Y is a trivial H-module. Let H_2 be the maximal 2-quotient of H and let N=\ker(H\to H_2). Then N has odd order, has a unique normal lift \widetilde N\triangleleft Y centralizing L_Y, and

Y\cong H\times_{H_2}Q, \qquad Q=Y/\widetilde N\text{ a finite $2$-group}.

Projection to Q identifies exact-image subgroups of Y projecting onto H with subgroups Q'\le Q that map onto H_2.

Lean code for Lemma10.2●1 theorem

theoremdefined in GQ2/SectionNine/Terminal.lean

complete

theorem GQ2.SectionNine.lemma_9_2_core {H Y : Type} [Group H] [Group Y]
  [Finite Y] (piY : Y →* H) (hpi : Function.Surjective ⇑piY)
  (L : Subgroup Y) (hkerL : piY.ker = L) (hL2 : IsPGroup 2 ↥L)
  (hstack : GQ2.SectionSeven.IsScalarStack L) (M : Subgroup H)
  [M.Normal] (hModd : Odd (Nat.card ↥M)) (hMtwo : IsPGroup 2 (H ⧸ M)) :
  ∃ Ntil,
    ∃ (x : Ntil.Normal),
      Odd (Nat.card ↥Ntil) ∧
        IsPGroup 2 (Y ⧸ Ntil) ∧
          Ntil ⊓ L = ⊥ ∧
            ⁅Ntil, L⁆ = ⊥ ∧
              Subgroup.map piY Ntil = M ∧
                Ntil ⊔ L = Subgroup.comap piY M

theorem GQ2.SectionNine.lemma_9_2_core
  {H Y : Type} [Group H] [Group Y]
  [Finite Y] (piY : Y →* H)
  (hpi : Function.Surjective ⇑piY)
  (L : Subgroup Y) (hkerL : piY.ker = L)
  (hL2 : IsPGroup 2 ↥L)
  (hstack :
    GQ2.SectionSeven.IsScalarStack L)
  (M : Subgroup H) [M.Normal]
  (hModd : Odd (Nat.card ↥M))
  (hMtwo : IsPGroup 2 (H ⧸ M)) :
  ∃ Ntil,
    ∃ (x : Ntil.Normal),
      Odd (Nat.card ↥Ntil) ∧
        IsPGroup 2 (Y ⧸ Ntil) ∧
          Ntil ⊓ L = ⊥ ∧
            ⁅Ntil, L⁆ = ⊥ ∧
              Subgroup.map piY Ntil = M ∧
                Ntil ⊔ L =
                  Subgroup.comap piY M

**Lemma 9.2 (structure).** For a marked target `1 → L → Y → H → 1` with `L = ker π` a
2-group *scalar stack* and `H` 2-nilpotent (`M = O²H` odd, `H/M` a 2-group), there is a unique
odd normal complement `Ñ ◁ Y` to `L` over `M`: `Ñ` is odd, `Y/Ñ` is a 2-group, `Ñ ∩ L = ⊥`,
`Ñ` centralizes `L`, `π(Ñ) = M`, and `Ñ · L = π⁻¹(M)`.  These are the fibre-product pieces
feeding `coprime_fiber_product` in the §9 induction.

Proof for Lemma 10.2

Proof uses 2

Proof dependency previews

Preview

Lemma 4.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §9 of the paper. Ingredients: Lemma 10.1 Lemma 4.1.