isInvariant_of_isGalois' — Mathlib

English

Replacing Gal(L/K) by Aut(B/A), the action descends to the quotient, giving an invariant structure on FixedPoints.subalgebra under H.

Русский

Замещая Gal(L/K) группой авто(B/A), действие спускается к фактор-группе, образуя инвариантность подалгебры фиксированных точек по H.

LaTeX

$$$\text{For normal } H,\; \text{MulSemiringAction}(G/H, \text{FixedPoints.subalgebra } A B H)$.$$

Lean4

/-- A variant of `Algebra.isInvariant_of_isGalois`, replacing `Gal(L/K)` by `Aut(B/A)`. -/
theorem isInvariant_of_isGalois' [FiniteDimensional K L] [IsGalois K L] : Algebra.IsInvariant A B (B ≃ₐ[A] B) :=
  ⟨fun b h ↦ (isInvariant_of_isGalois A K L B).1 b (fun g ↦ h (galRestrict A K L B g))⟩

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