English
The exterior power satisfies a universal property: there exists a core presentation core (isPresentationCore) that encodes the lifting and injectivity properties of the canonical construction through the relations, ensuring uniqueness of liftings of alternating maps through the presentation.
Русский
Внешнее произведение удовлетворяет универсальному свойству: существует ядро презентации (isPresentationCore), кодирующее свойства подъема и инъективности канонической конструкции через отношения, обеспечивающее единственность леберингов (lifting) чередующихся отображений через презентацию.
LaTeX
$$$\\text{isPresentationCore} : (\\text{relationsSolutionEquiv}^{-1}(\\iota_{Multi} )) .\\text{IsPresentationCore}$$$
Lean4
/-- The universal property of the exterior power. -/
noncomputable def isPresentationCore : (relationsSolutionEquiv.symm (ιMulti R n (M := M))).IsPresentationCore
where
desc
s :=
LinearMap.comp (ExteriorAlgebra.liftAlternating (Function.update 0 n (relationsSolutionEquiv s)))
(Submodule.subtype _)
postcomp_desc s := by aesop
postcomp_injective
{N _ _ f f' h} := by
rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (ιMulti_span R n M)]
rintro ⟨_, ⟨f, rfl⟩⟩
exact Module.Relations.Solution.congr_var h f
