Top-degree continuous alternating forms

Top-degree scalar-valued continuous alternating forms over a commutative ring are determined by their basis coefficient, which vanishes only for the zero form. Pullback by a continuous linear endomorphism multiplies that coefficient by its determinant. Pullback along a continuous linear map A : E → F multiplies it by the determinant of C⁻¹ ∘ A for any continuous linear equivalence C : E ≃ F, the target coefficient being taken in the transported basis. Above the top degree, continuous alternating maps on a finite-dimensional space over a division ring vanish. No compatibility between the topology and the module structure is required for those statements.

theorem ContinuousAlternatingMap.apply_eq_det_mul {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [Fintype ι] [DecidableEq ι] (ω : E [⋀^ι]→L[R] R) (b : Module.Basis ι R E) (v : ι → E) : ω v = b.det v * ω ⇑b

A top-degree alternating form is determined by its scalar coefficient in a basis.

theorem ContinuousAlternatingMap.compContinuousLinearMap_apply_basis {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [Finite ι] (ω : E [⋀^ι]→L[R] R) (b : Module.Basis ι R E) (A : E →L[R] E) : (ω.compContinuousLinearMap A) ⇑b = LinearMap.det ↑A * ω ⇑b

Pullback of a top-degree coefficient multiplies by the determinant.

theorem ContinuousAlternatingMap.compContinuousLinearMap_apply_basis_map {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [Finite ι] {F : Type u_4} [AddCommGroup F] [Module R F] [TopologicalSpace F] (ω : F [⋀^ι]→L[R] R) (b : Module.Basis ι R E) (A : E →L[R] F) (C : E ≃L[R] F) : (ω.compContinuousLinearMap A) ⇑b = LinearMap.det ↑(↑C.symm ∘SL A) * ω ⇑(b.map ↑C)

Pullback along a continuous linear map A : E → F multiplies the coefficient of a top-degree form by the determinant of A read in E through a continuous linear equivalence C : E ≃ F: the coefficient of A^* ω in a basis b of E is det (C⁻¹ ∘ A) times the coefficient of ω in the basis C ∘ b of F.

@[simp]

theorem ContinuousAlternatingMap.map_basis_eq_zero_iff {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [Finite ι] (ω : E [⋀^ι]→L[R] R) (b : Module.Basis ι R E) : ω ⇑b = 0 ↔ ω = 0

A top-degree alternating form vanishes on a basis exactly when it is zero.

theorem ContinuousAlternatingMap.map_basis_ne_zero_iff {R : Type u_1} {E : Type u_2} {ι : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [Finite ι] (ω : E [⋀^ι]→L[R] R) (b : Module.Basis ι R E) : ω ⇑b ≠ 0 ↔ ω ≠ 0

A nonzero top-degree alternating form is nonzero on every basis.

theorem ContinuousAlternatingMap.eq_zero_of_finrank_lt {K : Type u_4} {E : Type u_5} {F : Type u_6} {ι : Type u_7} [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [AddCommGroup F] [Module K F] [TopologicalSpace F] [Module.Finite K E] [Fintype ι] (f : E [⋀^ι]→L[K] F) (h : Module.finrank K E < Fintype.card ι) : f = 0

A continuous alternating map in more variables than the dimension of its domain is zero.