English
Two linear maps from ExteriorAlgebra R M to N are equal if they agree on the family of maps comping from ιMulti i for all i; this is a stronger extensional principle for ExteriorAlgebra.
Русский
Два линейных отображения из ExteriorAlgebra_R(M) в N равны, если они совпадают на семействах отображений, получаемых из ιMulti i для всех i.
LaTeX
$$$\forall i, f\circAlternatingMap(ιMulti i) = g\circAlternatingMap(ιMulti i) \Rightarrow f=g$$$
Lean4
/-- `ExteriorAlgebra.liftAlternating` is an equivalence. -/
@[simps apply symm_apply]
def liftAlternatingEquiv : (∀ i, M [⋀^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
where
toFun := liftAlternating (R := R)
map_add' := map_add _
map_smul' := map_smul _
invFun F i := F.compAlternatingMap (ιMulti R i)
left_inv _ := funext fun _ => liftAlternating_comp_ιMulti _
right_inv F := (liftAlternating_comp _ _).trans <| by rw [liftAlternating_ιMulti, LinearMap.comp_id]
