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.

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.

@[implicit_reducible]

instance ModuleCat.instFunLikeAlternatingMapForallFinCarrier {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) (n : ℕ) : FunLike (M.AlternatingMap N 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) : φ = φ'

theorem ModuleCat.AlternatingMap.ext_iff {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {φ φ' : M.AlternatingMap N n} : φ = φ' ↔ ∀ (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.

@[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 : ℕ.

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

theorem ModuleCat.exteriorPower.hom_ext_iff {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {f g : M.exteriorPower n ⟶ N} : f = g ↔ mk.postcomp f = mk.postcomp 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.

@[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.

@[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.

@[simp]

theorem ModuleCat.exteriorPower.functor_obj (R : Type u) [CommRing R] (n : ℕ) (M : ModuleCat R) : (functor R n).obj M = M.exteriorPower n

@[simp]

theorem ModuleCat.exteriorPower.functor_map (R : Type u) [CommRing R] (n : ℕ) {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (functor R n).map f = map f n

noncomputable def ModuleCat.exteriorPower.iso₀ {R : Type u} [CommRing R] (M : ModuleCat R) : M.exteriorPower 0 ≅ of R R

The isomorphism M.exteriorPower 0 ≅ ModuleCat.of R R.

@[simp]

theorem ModuleCat.exteriorPower.iso₀_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (f : Fin 0 → ↑M) : (CategoryTheory.ConcreteCategory.hom (iso₀ M).hom) (mk f) = 1

@[simp]

theorem ModuleCat.exteriorPower.iso₀_hom_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (map f 0) (iso₀ N).hom = (iso₀ M).hom

@[simp]

theorem ModuleCat.exteriorPower.iso₀_hom_naturality_assoc {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : of R R ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f 0) (CategoryTheory.CategoryStruct.comp (iso₀ N).hom h) = CategoryTheory.CategoryStruct.comp (iso₀ M).hom h

noncomputable def ModuleCat.exteriorPower.iso₁ {R : Type u} [CommRing R] (M : ModuleCat R) : M.exteriorPower 1 ≅ M

The isomorphism M.exteriorPower 1 ≅ M.

@[simp]

theorem ModuleCat.exteriorPower.iso₁_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (f : Fin 1 → ↑M) : (CategoryTheory.ConcreteCategory.hom (iso₁ M).hom) (mk f) = f 0

@[simp]

theorem ModuleCat.exteriorPower.iso₁_hom_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (map f 1) (iso₁ N).hom = CategoryTheory.CategoryStruct.comp (iso₁ M).hom f

@[simp]

theorem ModuleCat.exteriorPower.iso₁_hom_naturality_assoc {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f 1) (CategoryTheory.CategoryStruct.comp (iso₁ N).hom h) = CategoryTheory.CategoryStruct.comp (iso₁ M).hom (CategoryTheory.CategoryStruct.comp f h)

noncomputable def ModuleCat.exteriorPower.natIso₀ (R : Type u) [CommRing R] : functor R 0 ≅ (CategoryTheory.Functor.const (ModuleCat R)).obj (of R R)

The natural isomorphism M.exteriorPower 0 ≅ ModuleCat.of R R.

noncomputable def ModuleCat.exteriorPower.natIso₁ (R : Type u) [CommRing R] : functor R 1 ≅ CategoryTheory.Functor.id (ModuleCat R)

The natural isomorphism M.exteriorPower 1 ≅ M.