evaluationEquivOfIsGalois_symm_fiber

English

The inverse of the evaluation equivalence satisfies F.map((evaluationEquivOfIsGalois F A a).symm b).hom a = b for all b ∈ F.obj A.

Русский

Обратное к эквивалентности оценивания удовлетворяет F.map((evaluationEquivOfIsGalois F A a).symm b).hom a = b для любого b в F.obj A.

LaTeX

$$$\forall b \in F.obj A,\ F.map((\mathrm{evaluationEquivOfIsGalois}\ F\ A\ a)^{-1} b).hom\ a = b$$$

Lean4

@[simp]
theorem evaluationEquivOfIsGalois_symm_fiber (A : C) [IsGalois A] (a b : F.obj A) :
    F.map ((evaluationEquivOfIsGalois F A a).symm b).hom a = b :=
  by
  change (evaluationEquivOfIsGalois F A a) _ = _
  simp

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