SectionAction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Conjugation actions on normal sections and uniqueness on generated groups.

def OAI.FiniteLattice.CommonCore.quotientAction line 12

Source documentation

An action preserving a normal subgroup descends to the quotient.

def quotientAction (a : K →* MulAut M) (L : Subgroup M) [L.Normal]
    (hL : ∀ k, L.map (a k).toMonoidHom = L) : K →* MulAut (M ⧸ L) where
…

def OAI.FiniteLattice.CommonCore.transportAction line 30
Source documentation
An isomorphism transports an automorphism action.
```
def transportAction (a : K →* MulAut M) (e : M ≃* T) : K →* MulAut T where
…
```
theorem OAI.FiniteLattice.CommonCore.normal_section_invariant line 45
Source documentation
An ambient normal subgroup is preserved by conjugation on a normal subgroup.
```
theorem normal_section_invariant (Q L : Subgroup K) [Q.Normal] [L.Normal]
    (k : K) :
    (L.subgroupOf Q).map (MulAut.conjNormal (H := Q) k).toMonoidHom =
…
```

def OAI.FiniteLattice.CommonCore.normalSectionAction line 62

Source documentation

Conjugation on Q / (Q ∩ L) transported through theta.

def normalSectionAction (Q L : Subgroup K) [Q.Normal] [L.Normal]
    (theta : (Q ⧸ L.subgroupOf Q) ≃* T) : K →* MulAut T :=
…

theorem OAI.FiniteLattice.CommonCore.normalSectionAction_apply line 69

Source documentation

The transported action on a quotient representative.

theorem normalSectionAction_apply (Q L : Subgroup K) [Q.Normal] [L.Normal]
    (theta : (Q ⧸ L.subgroupOf Q) ≃* T) (k : K) (q : Q) :
    normalSectionAction Q L theta k (theta (QuotientGroup.mk' _ q)) =
      theta (QuotientGroup.mk' _ (MulAut.conjNormal (H := Q) k q)) := by
…

Mentions: OAI.FiniteLattice.CommonCore.normalSectionAction

theorem OAI.FiniteLattice.CommonCore.normalSectionAction_eq_of_representatives line 80

Source documentation

Agreement on quotient representatives determines the transported automorphism.

theorem normalSectionAction_eq_of_representatives
    (Q L : Subgroup K) [Q.Normal] [L.Normal]
    (theta : (Q ⧸ L.subgroupOf Q) ≃* T) (k : K) (b : MulAut T)
    (h : ∀ q : Q,
      theta (QuotientGroup.mk' _ (MulAut.conjNormal (H := Q) k q)) =
…

theorem OAI.FiniteLattice.CommonCore.generated_hom_unique line 95

Source documentation

Homomorphisms agreeing on a generating family of subgroups are equal.

theorem generated_hom_unique {H : Type*} [Group H] {ι : Type*}
    (U : ι → Subgroup K) (hgen : (⨆ i, U i) = ⊤)
    (f g : K →* H) (h : ∀ i, ∀ x : U i, f x = g x) : f = g := by
…