AmbientCore.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteLattice.CommonCore.normal_image_normalized line 10
Source documentation
Normality inside a subgroup gives ambient normalization by that subgroup.
```
theorem normal_image_normalized (U : Subgroup K) (B : Subgroup U) [B.Normal] :
    U ≤ Subgroup.normalizer ((B.map U.subtype) : Set K) := by
…
```
theorem OAI.FiniteLattice.CommonCore.normal_of_image_normalized line 18
def OAI.FiniteLattice.CommonCore.relativeCore line 29
Source documentation
The core of A in U, pulled back to a subgroup of A.
```
def relativeCore (A U : Subgroup K) : Subgroup A :=
…
```
theorem OAI.FiniteLattice.CommonCore.relativeCore_image line 32
theorem OAI.FiniteLattice.CommonCore.relativeCore_normalized line 41
theorem OAI.FiniteLattice.CommonCore.relativeCore_normal line 46

theorem OAI.FiniteLattice.CommonCore.restriction_conjugation line 51

Source documentation

Restriction of a homomorphism determines its conjugation equation on A.

theorem restriction_conjugation (A U : Subgroup K) (hAU : A ≤ U)
    (f : A →* H) (beta : U →* H)
    (hext : ∀ a : A, beta (Subgroup.inclusion hAU a) = f a)
    (u : U) (a b : A) (hb : (b : K) = u * (a : K) * (u : K)⁻¹) :
    f b = beta u * f a * (beta u)⁻¹ := by
…

theorem OAI.FiniteLattice.CommonCore.canonical_preimage_normalized_by_local line 62

Source documentation

The least normal preimage is normalized by each extension domain whose relative core maps over the prescribed perfect subgroup.

theorem canonical_preimage_normalized_by_local
    (A U : Subgroup K) [Finite A] (hAU : A ≤ U)
    (f : A →* H) (beta : U →* H)
    (hext : ∀ a : A, beta (Subgroup.inclusion hAU 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 ≤ (relativeCore A U).map f) :
    U ≤ Subgroup.normalizer ((Q.map A.subtype) : Set K) := by
…

Mentions: OAI.FiniteLattice.CommonCore.relativeCore

theorem OAI.FiniteLattice.CommonCore.exists_common_normal_preimage line 107

Source documentation

The common least preimage and its intersection with the kernel are normal in the group generated by the extension domains.

theorem exists_common_normal_preimage [Finite K] {ι : Type*} [Nonempty ι]
    (A : Subgroup K) (U : ι → Subgroup K) (hAU : ∀ i, A ≤ U i)
    (hgen : (⨆ i, U i) = ⊤) (f : A →* H) (beta : ∀ i, U i →* H)
    (hext : ∀ i, ∀ a : A, beta i (Subgroup.inclusion (hAU i) a) = f a)
    (J : Subgroup H) [J.Normal] [Group.IsPerfect J]
    (hcore : ∀ i, J ≤ (relativeCore A (U i)).map f) :
    ∃ Q : Subgroup A, Q.Normal ∧ Q.map f = J ∧
      (Q.map A.subtype).Normal ∧ ((Q ⊓ f.ker).map A.subtype).Normal ∧
      (∀ i, U i ≤ Subgroup.normalizer ((Q.map A.subtype) : Set K)) := by
…

Mentions: OAI.FiniteLattice.CommonCore.relativeCore