English
The exterior power ⨀^n_R M is presented by generators indexed by all functions m: ι → M with relations encoding bilinearity in each slot, scalar-linearity, and total antisymmetry; that is, the standard presentation uses a G = ι → M of generators and a system R = Rels R ι M of relations describing additivity, scalar multiplication, and alternation.
Русский
Внешнее произведение ⨀^n_R M имеет презентацию с генераторами, пронумерованными по всем функциям m: ι → M, и отношениями, описывающими билинейность по каждому слоту, линейность по скалярам и общую антисимметрию.
LaTeX
$$$\\text{presentation}_{R}(R,ι,M) = \\bigl( G=ι\\to M,\\; R=Rels(R,ι,M) \\bigr).$$$
Lean4
/-- The relations in the standard presentation of `⋀[R]^n M` with generators and relations. -/
@[simps]
noncomputable def relations (ι : Type*) [DecidableEq ι] (M : Type*) [AddCommGroup M] [Module R M] : Module.Relations R
where
G := ι → M
R := Rels R ι M
relation
| .add m i x y =>
Finsupp.single (update m i x) 1 + Finsupp.single (update m i y) 1 - Finsupp.single (update m i (x + y)) 1
| .smul m i r x => Finsupp.single (update m i (r • x)) 1 - r • Finsupp.single (update m i x) 1
| .alt m _ _ _ _ => Finsupp.single m 1
