CorePreimage.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Normality of least preimages under compatible local extensions.

theorem OAI.FiniteLattice.CommonCore.least_image_inside_normal_eq line 13

Source documentation

A least preimage computed inside a normal covering subgroup agrees with that computed in its ambient group, for the prescribed normal image J.

theorem least_image_inside_normal_eq
    (f : M →* H) (J : Subgroup H) [J.Normal]
    (Q : Subgroup M) [Q.Normal] (hQ : Q.map f = J)
    (hminQ : ∀ B : Subgroup M, B.Normal → J ≤ B.map f → Q ≤ B)
    (C : Subgroup M) [C.Normal] (hC : J ≤ C.map f)
    (B : Subgroup C) [B.Normal] (hB : B.map (f.comp C.subtype) = J)
    (hminB : ∀ A : Subgroup C, A.Normal → J ≤ A.map (f.comp C.subtype) → B ≤ A) :
    B.map C.subtype = Q := by
…

theorem OAI.FiniteLattice.CommonCore.least_image_normal_of_local_extension line 52

Source documentation

A local extension normalizes the least preimage when a normal subgroup covering the prescribed image is also normal in the ambient group.

theorem least_image_normal_of_local_extension
    (A : Subgroup D) [Finite A] (f : A →* H) (beta : D →* H)
    (hext : ∀ a : A, beta a = f a)
    (J : Subgroup H) [J.Normal] [Group.IsPerfect J]
    (Q : Subgroup A) [Q.Normal] (hQ : Q.map f = J)
    (hminQ : ∀ B : Subgroup A, B.Normal → J ≤ B.map f → Q ≤ B)
    (C : Subgroup A) [C.Normal] [(C.map A.subtype).Normal]
    (hC : J ≤ C.map f) : (Q.map A.subtype).Normal := by
…

theorem OAI.FiniteLattice.CommonCore.least_image_normal_of_core line 99

Source documentation

The least preimage is normal in the ambient group when the relative core covers the prescribed image.

theorem least_image_normal_of_core
    (A : Subgroup D) [Finite A] (f : A →* H) (beta : D →* H)
    (hext : ∀ a : A, beta a = f a)
    (J : Subgroup H) [J.Normal] [Group.IsPerfect J]
    (Q : Subgroup A) [Q.Normal] (hQ : Q.map f = J)
    (hminQ : ∀ B : Subgroup A, B.Normal → J ≤ B.map f → Q ≤ B)
    (hcore : J ≤ (A.normalCore.comap A.subtype).map f) :
    (Q.map A.subtype).Normal := by
…

theorem OAI.FiniteLattice.CommonCore.local_kernel_image_eq line 121

Source documentation

Intersecting a subgroup with the kernel of a restricted homomorphism commutes with its inclusion into the ambient group.

theorem local_kernel_image_eq
    (A : Subgroup D) (f : A →* H) (beta : D →* H)
    (hext : ∀ a : A, beta a = f a) (Q : Subgroup A) :
    (Q ⊓ f.ker).map A.subtype = Q.map A.subtype ⊓ beta.ker := by
…

theorem OAI.FiniteLattice.CommonCore.local_kernel_normal line 139
Source documentation
The intersection with the kernel is normal in the ambient group whenever the subgroup is normal and the homomorphism extends to that group.
```
theorem local_kernel_normal
    (A : Subgroup D) (f : A →* H) (beta : D →* H)
    (hext : ∀ a : A, beta a = f a) (Q : Subgroup A)
    [(Q.map A.subtype).Normal] : ((Q ⊓ f.ker).map A.subtype).Normal := by
…
```