English
A variant of isInvariant_of_isGalois replacing the Gal(L/K) group by Aut(B/A): the invariant property still holds for B over A under automorphisms.
Русский
Вариант теоремы об инвариантности, заменяющий Gal(L/K) на Aut(B/A): свойство инвариантности сохраняется.
LaTeX
$$$\text{IsInvariant } A B (B \simeq_A B)$ under Aut(B/A).$$$
Lean4
instance (H : Subgroup G) [H.Normal] : MulSemiringAction (G ⧸ H) (FixedPoints.subring B H)
where
smul :=
Quotient.lift
(fun g x ↦ ⟨g • x, fun h ↦ by simpa [mul_smul] using congr(g • $(x.2 ⟨_, ‹H.Normal›.conj_mem' _ h.2 g⟩))⟩)
(by
rintro _ a ⟨⟨⟨b⟩, hb⟩, rfl⟩
ext c
simpa [mul_smul] using congr(a • $(c.2 ⟨b, hb⟩)))
one_smul b := Subtype.ext (one_smul G b.1)
mul_smul := Quotient.ind₂ fun _ _ _ ↦ Subtype.ext (mul_smul _ _ _)
smul_zero := Quotient.ind fun _ ↦ Subtype.ext (smul_zero _)
smul_add := Quotient.ind fun _ _ _ ↦ Subtype.ext (smul_add _ _ _)
smul_one := Quotient.ind fun _ ↦ Subtype.ext (smul_one _)
smul_mul := Quotient.ind fun _ _ _ ↦ Subtype.ext (MulSemiringAction.smul_mul _ _ _)
