English
For a homeomorphism e: X ≃ Y, congrLeftₗ provides a linear equivalence between LocallyConstant X Z and LocallyConstant Y Z, reflecting the change of variables along e.
Русский
Для гомеоморфизма e: X ≃ Y конгLeftₗ задаёт линейное эквивалентное отображение между LocallyConstant(X,Z) и LocallyConstant(Y,Z), отражая смену переменных.
LaTeX
$$$\text{congrLeft}_{\ell}: \operatorname{LocallyConstant}(X,Z) \simeq_{\mathrm{linear}} \operatorname{LocallyConstant}(Y,Z)$$$
Lean4
/-- `LocallyConstant.congrLeft` as a linear equivalence. -/
@[simps!]
def congrLeftₗ (R : Type*) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :
LocallyConstant X Z ≃ₗ[R] LocallyConstant Y Z
where
toLinearMap := comapₗ R ⟨_, e.symm.continuous⟩
__ := congrLeft e
