English
There is a canonical linear equivalence between alternating maps when precomposed with a linear equivalence between domains.
Русский
Существуют естественные линейные эквивалентности между чередующимися картами при предварительном композиции с линейным эквивалентом между областями.
LaTeX
$$domLCongr(e)(f) = f \\circ e^{-1}$$
Lean4
/-- Construct a linear equivalence between maps from a linear equivalence between domains.
This is `AlternatingMap.compLinearMap` as an isomorphism,
and the alternating version of `LinearEquiv.multilinearMapCongrLeft`.
It could also have been called `LinearEquiv.alternatingMapCongrLeft`. -/
@[simps apply]
def domLCongr (e : M ≃ₗ[R] M₂) : M [⋀^ι]→ₗ[R] N ≃ₗ[S] (M₂ [⋀^ι]→ₗ[R] N)
where
toFun f := f.compLinearMap e.symm
invFun g := g.compLinearMap e
map_add' _ _ := rfl
map_smul' _ _ := rfl
left_inv f := AlternatingMap.ext fun _ => f.congr_arg <| funext fun _ => e.symm_apply_apply _
right_inv f := AlternatingMap.ext fun _ => f.congr_arg <| funext fun _ => e.apply_symm_apply _
