constLinearEquivOfIsEmpty — Mathlib

English

The space of constant maps indexed by an empty set is canonically linearly equivalent to the space of alternating maps in ι = ∅.

Русский

Пространство константных отображений над пустым индексным множеством эквивалентно пространству чередующихся отображений при ι = ∅.

LaTeX

$$$[IsEmpty ι] \\Rightarrow N'' \\cong_{R'} (M'' [⋀^ι]→ₗ[R'] N'')$$$

Lean4

/-- The space of constant maps is equivalent to the space of maps that are alternating with respect
to an empty family. -/
@[simps]
def constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'')
    where
  toFun := AlternatingMap.constOfIsEmpty R' M'' ι
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := f 0
  right_inv f := ext fun _ => AlternatingMap.congr_arg f <| Subsingleton.elim _ _

Похожие утверждения