Closed ranges of postcomposition by linear isometries

Postcomposition by a linear isometry acts pointwise on continuous linear maps. If its range is closed, the postcomposition operator also has closed range: its image consists precisely of operators whose values lie in that range. This lets smooth alternating pullback be checked through the underlying multilinear maps.

@[simp]

theorem LinearIsometry.postcomp_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {D : Type u_4} {E : Type u_5} {F : Type u_6} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] [SeminormedAddCommGroup E] [NormedSpace 𝕜₂ E] [SeminormedAddCommGroup F] [NormedSpace 𝕜₃ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (i : E →ₛₗᵢ[σ₂₃] F) (f : D →SL[σ₁₂] E) (x : D) : (i.postcomp f) x = i (f x)

Postcomposition by a linear isometry evaluates by composing the two maps.

theorem LinearIsometry.isClosed_range_postcomp {𝕜 : Type u_1} {D : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (i : E →ₗᵢ[𝕜] F) (hi : IsClosed (Set.range ⇑i)) : IsClosed (Set.range ⇑i.postcomp)

Postcomposition by a closed-range linear isometry has closed range on operators.