map_fixingSubgroup — Mathlib

English

The fixingSubgroup under a map is mapped to the conjugation action of that map.

Русский

Подгруппа фиксаций под действием отображения переходит в конъюгацию этого отображения.

LaTeX

$$$\text{map fixingSubgroup}(E) = (\operatorname{MulAut.conj} \sigma) \cdot E.fixingSubgroup$$$

Lean4

@[simp]
theorem map_fixingSubgroup (σ : L ≃ₐ[K] L) : (E.map σ).fixingSubgroup = (MulAut.conj σ) • E.fixingSubgroup :=
  by
  ext τ
  simp only [coe_map, AlgHom.coe_coe, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]
  rfl

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