toAlgHomEquiv — Mathlib

English

There is a MulEquiv between G and algebra automorphisms of the fixed-points field fixing FixedPoints.subfield G F.

Русский

Существует мультигомологическое эквивариантное соотношение между G и алгебраическими авто фиксированной области.

LaTeX

$$$\\text{toAlgAutMulEquiv } G (\\operatorname{FixedPoints.subfield } G F) F : G \\simeq_\\text{Mul} (\\operatorname{AlgAut}(\\operatorname{FixedPoints.subfield } G F, F))$$$

Lean4

/-- Bijection between `G` and algebra endomorphisms of `F` that fix the fixed points. -/
def toAlgHomEquiv [Finite G] [FaithfulSMul G F] : G ≃ (F →ₐ[FixedPoints.subfield G F] F) :=
  Equiv.ofBijective _ (toAlgHom_bijective G F)

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