reflection_dualMap_eq_coreflection

English

For any i ∈ ι, the dual map of the i-th reflection composed with flip equals flip composed with the coreflection at i: (reflection i).dualMap ∘ P.toLinearMap.flip = P.toLinearMap.flip ∘ coreflection i.

Русский

Для любого i ∈ ι сопряжённая карта отражения в i, затем flip, равна flip, затем корефлексия i: (reflection i).dualMap ∘ P.toLinearMap.flip = P.toLinearMap.flip ∘ coreflection i.

LaTeX

$$$ (P.reflection(i)).dualMap \circ P.toLinearMap.flip = P.toLinearMap.flip \circ P.coreflection(i) $$$

Lean4

theorem reflection_dualMap_eq_coreflection :
    (P.reflection i).dualMap ∘ₗ P.toLinearMap.flip = P.toLinearMap.flip ∘ₗ P.coreflection i :=
  by
  ext n m
  simp [map_sub, coreflection_apply, reflection_apply, mul_comm (P.toLinearMap m (P.coroot i))]

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