LeastImage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Equivariance of the least normal preimage of a perfect subgroup.

theorem OAI.FiniteLattice.CommonCore.least_image_stable line 12

Source documentation

Leastness forces invariance for a prescribed image, not merely image top.

theorem least_image_stable
    (f : M →* H) (J : Subgroup H) (Q : Subgroup M) [Q.Normal]
    (himage : Q.map f = J)
    (hleast : ∀ B : Subgroup M, B.Normal → J ≤ B.map f → Q ≤ B)
    (a : M ≃* M) (b : H ≃* H)
    (hJ : ∀ y ∈ J, b y ∈ J)
    (hcompat : ∀ x, f (a x) = b (f x)) :
    ∀ x ∈ Q, a x ∈ Q := by
…

theorem OAI.FiniteLattice.CommonCore.least_image_map_eq line 39

Source documentation

A compatible pair of automorphisms preserving the prescribed image also preserves its least normal preimage.

theorem least_image_map_eq
    (f : M →* H) (J : Subgroup H) (Q : Subgroup M) [Q.Normal]
    (himage : Q.map f = J)
    (hleast : ∀ B : Subgroup M, B.Normal → J ≤ B.map f → Q ≤ B)
    (a : M ≃* M) (b : H ≃* H)
    (hJ : J.map b.toMonoidHom = J)
    (hcompat : ∀ x, f (a x) = b (f x)) :
    Q.map a.toMonoidHom = Q := by
…

theorem OAI.FiniteLattice.CommonCore.exists_equivariant_least_preimage line 76

Source documentation

A perfect normal subgroup in the image has a least normal preimage, invariant under every compatible pair of automorphisms preserving the image.

theorem exists_equivariant_least_preimage [Finite M]
    (f : M →* H) (J : Subgroup H) [J.Normal] [Group.IsPerfect J]
    (hJ : J ≤ f.range) :
    ∃ Q : Subgroup M, Q.Normal ∧ Q.map f = J ∧
      (∀ B : Subgroup M, B.Normal → J ≤ B.map f → Q ≤ B) ∧
      (∀ (a : M ≃* M) (b : H ≃* H), J.map b.toMonoidHom = J →
        (∀ x, f (a x) = b (f x)) → Q.map a.toMonoidHom = Q) := by
…