Theorems · Definition · linear algebra
ModuleCat.exteriorPower.map
{R : Type u} → [inst : CommRing R] → {M N : ModuleCat R} → (M ⟶ N) → (n : ℕ) → M.exteriorPower n ⟶ N.exteriorPower nThe morphism M.exteriorPower n ⟶ N.exteriorPower n induced by a morphism M ⟶ N
in ModuleCat R.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.Hom.homproof · cited by 341
- ModuleCat.ofHomproof · cited by 200
- exteriorPower.mapproof · cited by 14
- ModuleCat.exteriorPowerstatement · cited by 12
Cited by7
Results whose statement or proof uses this declaration.
- ModuleCat.exteriorPower.functorproof · cited by 2
- ModuleCat.exteriorPower.iso₁_hom_naturalitystatement · cited by 1
- ModuleCat.exteriorPower.iso₀_hom_naturalitystatement · cited by 1
- ModuleCat.exteriorPower.iso₁_hom_naturality_assocstatement and proof · cited by 0
- ModuleCat.exteriorPower.map_mkstatement · cited by 0
- ModuleCat.exteriorPower.functor_mapstatement · cited by 0
- ModuleCat.exteriorPower.iso₀_hom_naturality_assocstatement and proof · cited by 0