The exterior powers as functors on the category of modules

In this file, given M : ModuleCat R and n : ℕ, we define M.exteriorPower n : ModuleCat R, and this extends to a functor ModuleCat.exteriorPower.functor : ModuleCat R ⥤ ModuleCat R.

def ModuleCat.exteriorPower {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) : ModuleCat R

The exterior power of an object in ModuleCat R.

Equations

• M.exteriorPower n = ModuleCat.of R ↥(⋀[R]^n ↑M)

def ModuleCat.AlternatingMap {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) (n : ℕ) : Type (max (max v u v) 0)

The type of n-alternating maps on M : ModuleCat R to N : ModuleCat R.

Equations

• M.AlternatingMap N n = ↑M [⋀^Fin n]→ₗ[R] ↑N

instance ModuleCat.instFunLikeAlternatingMapForallFinCarrier {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) (n : ℕ) : FunLike (M.AlternatingMap N n) (Fin n → ↑M) ↑N

Equations

• M.instFunLikeAlternatingMapForallFinCarrier N n = inferInstanceAs (FunLike (↑M [⋀^Fin n]→ₗ[R] ↑N) (Fin n → ↑M) ↑N)

theorem ModuleCat.AlternatingMap.ext {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {φ φ' : M.AlternatingMap N n} (h : ∀ (x : Fin n → ↑M), φ x = φ' x) : φ = φ'

def ModuleCat.AlternatingMap.postcomp {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} (φ : M.AlternatingMap N n) {N' : ModuleCat R} (g : N ⟶ N') : M.AlternatingMap N' n

The postcomposition of an alternating map by a linear map.

Equations

• φ.postcomp g = (ModuleCat.Hom.hom g).compAlternatingMap φ

@[simp]

theorem ModuleCat.AlternatingMap.postcomp_apply {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} (φ : M.AlternatingMap N n) {N' : ModuleCat R} (g : N ⟶ N') (x : Fin n → ↑M) : (φ.postcomp g) x = (CategoryTheory.ConcreteCategory.hom g) (φ x)

def ModuleCat.exteriorPower.mk {R : Type u} [CommRing R] {M : ModuleCat R} {n : ℕ} : M.AlternatingMap (M.exteriorPower n) n

Constructor for elements in M.exteriorPower n when M is an object of ModuleCat R and n : ℕ.

Equations

• ModuleCat.exteriorPower.mk = exteriorPower.ιMulti R n

theorem ModuleCat.exteriorPower.hom_ext {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {f g : M.exteriorPower n ⟶ N} (h : mk.postcomp f = mk.postcomp g) : f = g

noncomputable def ModuleCat.exteriorPower.desc {R : Type u} [CommRing R] {M : ModuleCat R} {n : ℕ} {N : ModuleCat R} (φ : M.AlternatingMap N n) : M.exteriorPower n ⟶ N

The morphism M.exteriorPower n ⟶ N induced by an alternating map.

Equations

• ModuleCat.exteriorPower.desc φ = ModuleCat.ofHom (exteriorPower.alternatingMapLinearEquiv φ)

@[simp]

theorem ModuleCat.exteriorPower.desc_mk {R : Type u} [CommRing R] {M : ModuleCat R} {n : ℕ} {N : ModuleCat R} (φ : M.AlternatingMap N n) (x : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom (desc φ)) (mk x) = φ x

noncomputable def ModuleCat.exteriorPower.map {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (n : ℕ) : M.exteriorPower n ⟶ N.exteriorPower n

The morphism M.exteriorPower n ⟶ N.exteriorPower n induced by a morphism M ⟶ N in ModuleCat R.

Equations

• ModuleCat.exteriorPower.map f n = ModuleCat.ofHom (exteriorPower.map n (ModuleCat.Hom.hom f))

@[simp]

theorem ModuleCat.exteriorPower.map_mk {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {n : ℕ} (x : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom (map f n)) (mk x) = mk (⇑(CategoryTheory.ConcreteCategory.hom f) ∘ x)

noncomputable def ModuleCat.exteriorPower.functor (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

The functor ModuleCat R ⥤ ModuleCat R which sends a module to its nth exterior power.

Equations

• One or more equations did not get rendered due to their size.