autMulEquivAutGalois_symm_app — Mathlib

English

The isomorphism given by autMulEquivAutGalois symm satisfies a concrete formula in terms of π maps.

Русский

Изоморфизм, задаваемый symm через autMulEquivAutGalois, удовлетворяет конкретной формуле через отображения π.

LaTeX

$$$((autMulEquivAutGalois F).symm \\langle x \\rangle).hom.app A\\, a = F.map(AutGalois.\\pi F \\langle A, a, \\text{isGalois} \\rangle x).hom a$$$

Lean4

@[simp]
theorem autMulEquivAutGalois_symm_app (x : AutGalois F) (A : C) [IsGalois A] (a : F.obj A) :
    ((autMulEquivAutGalois F).symm ⟨x⟩).hom.app A a = F.map (AutGalois.π F ⟨A, a, inferInstance⟩ x).hom a :=
  by
  rw [← autMulEquivAutGalois_π, MulEquiv.apply_symm_apply]
  rfl

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