Alternating pullbacks and postcompositions

The underlying continuous multilinear map of an alternating pullback is the multilinear pullback. This identity allows consumers to move between the two APIs without unfolding their implementations.

Postcomposing a continuous alternating map with the identity continuous linear map leaves it unchanged.

Pullback along a continuous linear map is linear, and postcomposition with a continuous linear map that is semilinear for an additional scalar action is semilinear, over any scalars acting on the codomain compatibly with the base ring. For instance, complex-valued real alternating forms form a complex vector space, and these operations are complex-linear or conjugate-linear.

Main declarations

• ContinuousAlternatingMap.compContinuousLinearMapLinear: pullback as a linear map over the scalars of the codomain.
• ContinuousLinearMap.compContinuousAlternatingMapSemilinear: postcomposition with a semilinear map as a semilinear map of alternating maps.
• ContinuousAlternatingMap.eq_zero_iff_forall_apply_fin_one: an alternating map of one vector vanishes exactly when it vanishes on every vector.
• ContinuousAlternatingMap.compContinuousLinearMap_compContinuousLinearMap: pulling back along A and then along B is pulling back along A.comp B.

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_compContinuousLinearMap {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [Semiring R] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommMonoid F] [Module R F] [TopologicalSpace F] [AddCommMonoid G] [Module R G] [TopologicalSpace G] (φ : F [⋀^ι]→L[R] G) (f : E →L[R] F) : (φ.compContinuousLinearMap f).toContinuousMultilinearMap = φ.compContinuousLinearMap fun (x : ι) => f

Taking the underlying multilinear map commutes with continuous linear pullback.

def ContinuousAlternatingMap.compContinuousLinearMapLinear {A : Type u_1} (S : Type u_2) {M : Type u_3} {M' : Type u_4} {N : Type u_5} {ι : Type u_6} [Semiring A] [Semiring S] [AddCommMonoid M] [Module A M] [TopologicalSpace M] [AddCommMonoid M'] [Module A M'] [TopologicalSpace M'] [AddCommMonoid N] [Module A N] [TopologicalSpace N] [ContinuousAdd N] [Module S N] [ContinuousConstSMul S N] [SMulCommClass A S N] (f : M →L[A] M') : M' [⋀^ι]→L[A] N →ₗ[S] M [⋀^ι]→L[A] N

ContinuousAlternatingMap.compContinuousLinearMap as a linear map over any scalars acting on the codomain. This generalizes Mathlib's ContinuousAlternatingMap.compContinuousLinearMapₗ, which is linear over the base ring only.

@[simp]

theorem ContinuousAlternatingMap.compContinuousLinearMapLinear_apply {A : Type u_1} {S : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {ι : Type u_6} [Semiring A] [Semiring S] [AddCommMonoid M] [Module A M] [TopologicalSpace M] [AddCommMonoid M'] [Module A M'] [TopologicalSpace M'] [AddCommMonoid N] [Module A N] [TopologicalSpace N] [ContinuousAdd N] [Module S N] [ContinuousConstSMul S N] [SMulCommClass A S N] (f : M →L[A] M') (g : M' [⋀^ι]→L[A] N) : (compContinuousLinearMapLinear S f) g = g.compContinuousLinearMap f

theorem ContinuousAlternatingMap.eq_zero_iff_forall_apply_fin_one {R : Type u_7} {M : Type u_8} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] (α : M [⋀^Fin 1]→L[R] N) : α = 0 ↔ ∀ (v : M), α ![v] = 0

A continuous alternating map of one vector vanishes exactly when it vanishes on every vector.

@[simp]

theorem ContinuousAlternatingMap.compContinuousLinearMap_compContinuousLinearMap {R : Type u_7} {M : Type u_8} {M' : Type u_9} {M'' : Type u_10} {F : Type u_11} {ι : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid M'] [Module R M'] [TopologicalSpace M'] [AddCommMonoid M''] [Module R M''] [TopologicalSpace M''] [AddCommMonoid F] [Module R F] [TopologicalSpace F] (a : M'' [⋀^ι]→L[R] F) (A : M →L[R] M'') (B : M' →L[R] M) : (a.compContinuousLinearMap A).compContinuousLinearMap B = a.compContinuousLinearMap (A ∘SL B)

Pulling a form back along A and then along B is pulling it back along A.comp B.

@[simp]

theorem ContinuousLinearMap.id_compContinuousAlternatingMap {R : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid E] [Module R E] [TopologicalSpace E] [AddCommMonoid F] [Module R F] [TopologicalSpace F] (f : E [⋀^ι]→L[R] F) : (ContinuousLinearMap.id R F).compContinuousAlternatingMap f = f

Postcomposing a continuous alternating map with the identity leaves it unchanged.

def ContinuousLinearMap.compContinuousAlternatingMapSemilinear {A : Type u_1} {S : Type u_2} {S₂ : Type u_3} {M : Type u_4} {N : Type u_5} {N' : Type u_6} {ι : Type u_7} [Semiring A] [Semiring S] [Semiring S₂] [AddCommMonoid M] [Module A M] [TopologicalSpace M] [AddCommMonoid N] [Module A N] [TopologicalSpace N] [ContinuousAdd N] [Module S N] [ContinuousConstSMul S N] [SMulCommClass A S N] [AddCommMonoid N'] [Module A N'] [TopologicalSpace N'] [ContinuousAdd N'] [Module S₂ N'] [ContinuousConstSMul S₂ N'] [SMulCommClass A S₂ N'] {σ : S →+* S₂} (L : N →L[A] N') (hL : ∀ (c : S) (x : N), L (c • x) = σ c • L x) : M [⋀^ι]→L[A] N →ₛₗ[σ] M [⋀^ι]→L[A] N'

Postcomposition with a continuous linear map L that is σ-semilinear for additional scalar actions on its domain and codomain, as a σ-semilinear map of alternating maps.

@[simp]

theorem ContinuousLinearMap.compContinuousAlternatingMapSemilinear_apply {A : Type u_1} {S : Type u_2} {S₂ : Type u_3} {M : Type u_4} {N : Type u_5} {N' : Type u_6} {ι : Type u_7} [Semiring A] [Semiring S] [Semiring S₂] [AddCommMonoid M] [Module A M] [TopologicalSpace M] [AddCommMonoid N] [Module A N] [TopologicalSpace N] [ContinuousAdd N] [Module S N] [ContinuousConstSMul S N] [SMulCommClass A S N] [AddCommMonoid N'] [Module A N'] [TopologicalSpace N'] [ContinuousAdd N'] [Module S₂ N'] [ContinuousConstSMul S₂ N'] [SMulCommClass A S₂ N'] {σ : S →+* S₂} (L : N →L[A] N') (hL : ∀ (c : S) (x : N), L (c • x) = σ c • L x) (ω : M [⋀^ι]→L[A] N) : (L.compContinuousAlternatingMapSemilinear hL) ω = L.compContinuousAlternatingMap ω