OAI/GroupTheory/FiniteLattice/PerfectPreimage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteLattice.perfect_le_map_inf line 12

   Source documentation

   Two normal subgroups whose images contain a perfect subgroup retain it in their intersection.

   theorem perfect_le_map_inf (f : M →* H) (P : Subgroup H) [Group.IsPerfect P]
       (B C : Subgroup M) [B.Normal] [C.Normal]
       (hB : P ≤ B.map f) (hC : P ≤ C.map f) : P ≤ (B ⊓ C).map f := by
   …

2. theorem OAI.FiniteLattice.perfect_le_map_iInf line 22

   Source documentation

   A finite nonempty intersection of normal subgroups retains a prescribed perfect image.

   theorem perfect_le_map_iInf {ι : Type*} [Finite ι] [Nonempty ι]
       (f : M →* H) (P : Subgroup H) [Group.IsPerfect P]
       (B : ι → Subgroup M) (hN : ∀ i, (B i).Normal)
       (hP : ∀ i, P ≤ (B i).map f) : P ≤ (⨅ i, B i).map f := by
   …

3. theorem OAI.FiniteLattice.exists_least_normal_perfect_preimage line 43

   Source documentation

   In a finite group, there is a least normal subgroup mapping onto a prescribed perfect normal subgroup.

   theorem exists_least_normal_perfect_preimage [Finite M]
       (f : M →* H) (P : Subgroup H) [Group.IsPerfect P] [P.Normal]
       (hP : P ≤ f.range) :
       ∃ Q : Subgroup M, Q.Normal ∧ Q.map f = P ∧
         ∀ B : Subgroup M, B.Normal → P ≤ B.map f → Q ≤ B := by
   …