congrLeftRingEquiv — Mathlib

English

There is an algebra isomorphism (AlgEquiv) between LocallyConstant X Z and LocallyConstant Y Z induced by a homeomorphism X ≃ₜ Y, respecting the R-algebra structure.

Русский

Существует алгебраическое эквивалентное отображение между LocallyConstant X Z и LocallyConstant Y Z, индуцированное гомеоморфизмом X ≃ₜ Y, сохраняющее структуру R-алгебры.

LaTeX

$$$\text{LocallyConstant}(X,Z) \cong_{\mathsf{Alg}}^{R} \text{LocallyConstant}(Y,Z).$$$

Lean4

/-- `LocallyConstant.congrLeft` as a `RingEquiv`. -/
@[simps!]
def congrLeftRingEquiv [Semiring Z] (e : X ≃ₜ Y) : LocallyConstant X Z ≃+* LocallyConstant Y Z
    where
  toEquiv := congrLeft e
  __ := comapMonoidHom ⟨_, e.symm.continuous⟩
  __ := comapAddMonoidHom ⟨_, e.symm.continuous⟩

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