English
Let e : Y ≃ₐ[R] Z be an algebra equivalence. Then e induces a LocallyConstant algebra equivalence LocallyConstant(X,Y) ≃ₐ[R] LocallyConstant(X,Z) by transporting along e.
Русский
Пусть e : Y ≃ₐ[R] Z — алгебраическое эквивалентность. Тогда e индуцирует локально-константное алгебраическое эквивалентство LocallyConstant(X,Y) ≃ₐ[R] LocallyConstant(X,Z), перенося структуру через e.
LaTeX
$$$\\operatorname{congrRight}_{\\mathsf{A}}(e) : \\operatorname{LocallyConstant}(X,Y) \\simeq_{\\mathsf{A}}[R] \\operatorname{LocallyConstant}(X,Z)$$$
Lean4
/-- `LocallyConstant.congrRight` as an `AlgEquiv`. -/
@[simps!]
def congrRightₐ (R : Type*) [CommSemiring R] [Semiring Y] [Algebra R Y] [Semiring Z] [Algebra R Z] (e : Y ≃ₐ[R] Z) :
LocallyConstant X Y ≃ₐ[R] LocallyConstant X Z
where
toEquiv := congrRight e
__ := mapₐ R e.toAlgHom
