English
For a continuous linear isomorphism e : N ≃L[R] N', postcomposing with e yields an equivalence between spaces of continuous alternating maps with codomains N and N'.
Русский
Для непрерывного линейного биекция e : N ≃L[R] N' посткомпозиция с e дает эквивалентность между пространствами непрерывных чередующихся отображений с кодоменами N и N'.
LaTeX
$$$ (M [⋀^ι]→L[R] N) \simeq (M [⋀^ι]→L[R] N') $$$
Lean4
/-- If `I` and `J` are complementary index sets, the product of the kernels of the `J`th projections
of `φ` is linearly equivalent to the product over `I`. -/
def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) :
(⨅ i ∈ J, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i)) ≃L[R] ∀ i : I, φ i
where
toLinearEquiv := LinearMap.iInfKerProjEquiv R φ hd hu
continuous_toFun :=
continuous_pi fun i =>
Continuous.comp (continuous_apply (A := φ) i) <|
@continuous_subtype_val _ _ fun x => x ∈ (⨅ i ∈ J, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i))
continuous_invFun :=
Continuous.subtype_mk
(continuous_pi fun i => by
dsimp
split_ifs <;> [apply continuous_apply; exact continuous_zero])
_
