CommonCoreAmbient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteLattice.CommonCore.subgroupInsideEquiv line 12
Source documentation
A subgroup contained in K, viewed inside K, is canonically the same group.
```
def subgroupInsideEquiv (A K : Subgroup D) (hAK : A ≤ K) : A.subgroupOf K ≃* A where
…
```

def OAI.FiniteLattice.CommonCore.AmbientStatement line 23

Source documentation

Compatible extensions in a finite group glue uniquely over their generated join, whose relative core retains the inner automorphisms.

def AmbientStatement (D T : Type*) [Group D] [Finite D] [Group T] [IsSimpleGroup T]
    (ι : Type*) [Finite ι] [Nonempty ι]
    (A : Subgroup D) (U : ι → Subgroup D) (hAU : ∀ i, A ≤ U i)
    (alpha : A →* MulAut T) (beta : ∀ i, U i →* MulAut T) : Prop :=
…

theorem OAI.FiniteLattice.CommonCore.common_core_ambient line 38

Source documentation

The common-core criterion for extension domains in a finite ambient group.

theorem common_core_ambient (D T : Type*) [Group D] [Finite D] [Group T]
    [IsSimpleGroup T] (ι : Type*) [Finite ι] [Nonempty ι]
    (A : Subgroup D) (U : ι → Subgroup D) (hAU : ∀ i, A ≤ U i)
    (alpha : A →* MulAut T) (beta : ∀ i, U i →* MulAut T) :
    AmbientStatement D T ι A U hAU alpha beta := by
…

Mentions: OAI.FiniteLattice.CommonCore.AmbientStatement