RetainedCore.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A relative normal core retains a nonabelian simple quotient when the adjoining subgroups normalize suitable normal full preimages and centralize their images in the quotient.

theorem OAI.FiniteLattice.RetainedCore.least_full_preimage_stable line 23

Source documentation

Minimality plus full image forces stability under every compatible pair of genuine group automorphisms. No invariance is assumed of Q.

theorem least_full_preimage_stable
    (f : M →* H) (Q : Subgroup M) [Q.Normal]
    (hfull : Q.map f = ⊤)
    (hleast : ∀ B : Subgroup M, B.Normal → B.map f = ⊤ → Q ≤ B)
    (a : M ≃* M) (b : H ≃* H)
    (hcompat : ∀ x, f (a x) = b (f x)) :
    ∀ x ∈ Q, a x ∈ Q := by
…

theorem OAI.FiniteLattice.RetainedCore.least_full_preimage_map_eq line 48
def OAI.FiniteLattice.RetainedCore.Statement line 73
Source documentation
A relative normal core maps onto a nonabelian simple quotient. The subgroups T i lie in R₀; their ambient images are used for normalization and commutators. The normal core inside the generated subgroup W is transported back to R₀. The finite indexing type may be empty.
```
def Statement (D : Type*) [Group D] [Finite D]
    (R₀ : Subgroup D) (C : Subgroup R₀) [C.Normal]
    [IsSimpleGroup (R₀ ⧸ C)]
    (ι : Type*) [Finite ι] (L : ι → Subgroup D)
    (T : ι → Subgroup R₀) : Prop :=
…
```

theorem OAI.FiniteLattice.RetainedCore.exists_least_full_preimage line 90

Source documentation

A least normal full preimage, with equality-shaped minimality.

theorem exists_least_full_preimage [Finite M] [Group.IsPerfect H]
    (f : M →* H) (hf : Function.Surjective f) :
    ∃ Q : Subgroup M, Q.Normal ∧ Q.map f = ⊤ ∧
      ∀ B : Subgroup M, B.Normal → B.map f = ⊤ → Q ≤ B := by
…

def OAI.FiniteLattice.RetainedCore.embeddedConj line 102
Source documentation
Restrict ambient conjugation to an embedded subgroup, without assuming that conjugation preserves the larger group into which that subgroup embeds.
```
noncomputable def embeddedConj {D : Type*} [Group D]
    (K : Subgroup M) (j : M →* D) (hj : Function.Injective j)
    (g : D) (hg : g ∈ Subgroup.normalizer (K.map j : Set D)) : K ≃* K :=
…
```
theorem OAI.FiniteLattice.RetainedCore.embeddedConj_val line 108

theorem OAI.FiniteLattice.RetainedCore.least_inside_normal_eq line 122

Source documentation

The least full preimage inside a normal subgroup equals that inside its ambient group. The quotient may be any perfect group.

theorem least_inside_normal_eq [Finite M] [Group.IsPerfect H]
    (f : M →* H) (Q : Subgroup M) [Q.Normal]
    (hQ : Q.map f = ⊤)
    (hminQ : ∀ B : Subgroup M, B.Normal → B.map f = ⊤ → Q ≤ B)
    (K : Subgroup M) [K.Normal]
    (hK : K.map f = ⊤)
    (B : Subgroup K) [B.Normal]
    (hB : B.map (f.comp K.subtype) = ⊤)
    (hminB : ∀ A : Subgroup K, A.Normal →
      A.map (f.comp K.subtype) = ⊤ → B ≤ A) :
    B.map K.subtype = Q := by
…

theorem OAI.FiniteLattice.RetainedCore.retained_core line 162

Source documentation

The relative normal core retains the entire nonabelian simple quotient.

theorem retained_core (D : Type*) [Group D] [Finite D]
    (R₀ : Subgroup D) (C : Subgroup R₀) [C.Normal]
    [IsSimpleGroup (R₀ ⧸ C)]
    (ι : Type*) [Finite ι] (L : ι → Subgroup D)
    (T : ι → Subgroup R₀) : Statement D R₀ C ι L T := by
…

Mentions: OAI.FiniteLattice.RetainedCore.Statement