evaluationEquivOfIsGalois_apply — Mathlib

English

For a Galois A and a ∈ F.obj A, the evaluation equivalence sends φ ∈ Aut A to F.map φ.hom a.

Русский

Для галуа A и a ∈ F.obj A, эквивалентность оценивания отправляет φ ∈ Aut A в F.map φ.hom a.

LaTeX

$$$\mathrm{evaluationEquivOfIsGalois}(F,A,a)(\varphi) = F.map(\varphi.hom) a$$$

Lean4

@[simp]
theorem evaluationEquivOfIsGalois_apply (A : C) [IsGalois A] (a : F.obj A) (φ : Aut A) :
    evaluationEquivOfIsGalois F A a φ = F.map φ.hom a :=
  rfl

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