instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient

English

If there is invariant action of G on B, then the quotient invariants descend to the fixed subalgebra under H.

Русский

Если существует инвариантное действие G на B, наследуется инвариантность по отношению к фактор-группе H.

LaTeX

$$$\text{Algebra.IsInvariant } A (FixedPoints.subalgebra A B H) (G/H).$$$

Lean4

instance (H : Subgroup G) [H.Normal] [Algebra.IsInvariant A B G] :
    Algebra.IsInvariant A (FixedPoints.subalgebra A B H) (G ⧸ H) where
  isInvariant x
    hx :=
    by
    obtain ⟨y, hy⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) x.1 (fun g ↦ congr_arg Subtype.val (hx g))
    exact ⟨y, Subtype.ext hy⟩

Похожие утверждения