English
The composition is compatible with domain equivalence: (σ acts on indices) (g).compMultilinearMap f = g.compMultilinearMap (f.domDomCongr σ).
Русский
Композиция совместима с эквивалентностью доменов по индексов: (σ) (g).compMultilinearMap f = g.compMultilinearMap (f.domDomCongr σ).
LaTeX
$$$$ (g.compMultilinearMap f).domDomCongr \sigma = g.compMultilinearMap (f.domDomCongr \sigma). $$$$
Lean4
/-- The dependent version of `MultilinearMap.domDomCongrLinearEquiv`. -/
@[simps apply symm_apply]
def domDomCongrLinearEquiv' {ι' : Type*} (σ : ι ≃ ι') :
MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun i => M₁ (σ.symm i)) M₂
where
toFun
f :=
{ toFun := f ∘ (σ.piCongrLeft' M₁).symm
map_update_add' := fun m i => by
letI := σ.decidableEq
rw [← σ.apply_symm_apply i]
intro x y
simp only [comp_apply, piCongrLeft'_symm_update, f.map_update_add]
map_update_smul' := fun m i c => by
letI := σ.decidableEq
rw [← σ.apply_symm_apply i]
intro x
simp only [Function.comp, piCongrLeft'_symm_update, f.map_update_smul] }
invFun
f :=
{ toFun := f ∘ σ.piCongrLeft' M₁
map_update_add' := fun m i => by
letI := σ.symm.decidableEq
rw [← σ.symm_apply_apply i]
intro x y
simp only [comp_apply, piCongrLeft'_update, f.map_update_add]
map_update_smul' := fun m i c => by
letI := σ.symm.decidableEq
rw [← σ.symm_apply_apply i]
intro x
simp only [Function.comp, piCongrLeft'_update, f.map_update_smul] }
map_add' f₁
f₂ := by
ext
simp only [Function.comp, coe_mk, add_apply]
map_smul' c
f := by
ext
simp only [Function.comp, coe_mk, smul_apply, RingHom.id_apply]
left_inv
f := by
ext
simp only [coe_mk, comp_apply, Equiv.symm_apply_apply]
right_inv
f := by
ext
simp only [coe_mk, comp_apply, Equiv.apply_symm_apply]
