Semilinear maps on exterior powers

This file constructs the exterior power of a semilinear map between modules. It is ordinary linear algebra and has no categorical or geometric hypotheses.

noncomputable def LinearMap.exteriorPower {R S : Type u} [CommRing R] [CommRing S] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module S N] (n : ℕ) (σ : R →+* S) (f : M →ₛₗ[σ] N) : ↥(⋀[R]^n M) →ₛₗ[σ] ↥(⋀[S]^n N)

A semilinear map induces a semilinear map on exterior powers.

Equations

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

@[simp]

theorem LinearMap.exteriorPower_ιMulti {R S : Type u} [CommRing R] [CommRing S] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module S N] (n : ℕ) (σ : R →+* S) (f : M →ₛₗ[σ] N) (x : Fin n → M) : (exteriorPower n σ f) ((exteriorPower.ιMulti R n) x) = (exteriorPower.ιMulti S n) (⇑f ∘ x)