algEquivOfEqMap_apply — Mathlib

English

For the induced isomorphism φ from the previous item, its action on a representative x∈B is given by φ(x̄) = σ(x)̄, i.e., the image of x in B/P maps to the image of σ(x) in C/Q.

Русский

Для полученного из предыдущего пункта изоморфизма φ действие на представитель x ∈ B задаётся как φ(x̄) = σ(x)̄, то есть образ класса x в B/P переходит в образ σ(x) в C/Q.

LaTeX

$$$(\text{algEquivOfEqMap } p σ h)(x) = σ(x)\,\text{ in } C/Q$ for x∈B$$

Lean4

@[simp]
theorem algEquivOfEqMap_apply (h : Q = P.map σ) (x : B) : algEquivOfEqMap p σ h x = σ x :=
  rfl

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