S01_Vector_Spaces.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 1 file

example (example at line 12) line 12 source
example (example at line 15) line 15 source
example (example at line 18) line 18 source
example (example at line 21) line 21 source
example (example at line 37) line 37 source
example (example at line 50) line 50 source
example (example at line 53) line 53 source
example (example at line 68) line 68 source
example (example at line 85) line 85 source
example (example at line 88) line 88 source
example (example at line 99) line 99 source
Source comment
First projection map
```
example : V × W →ₗ[K] V := LinearMap.fst K V W
```
example (example at line 102) line 102 source
Source comment
Second projection map
```
example : V × W →ₗ[K] W := LinearMap.snd K V W
```

example (example at line 105) line 105 source

Source comment

Universal property of the product

example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K]  V × W := LinearMap.prod φ ψ

example (example at line 108) line 108 source
Source comment
The product map does the expected thing, first component
```
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl
```
example (example at line 111) line 111 source
Source comment
The product map does the expected thing, second component
```
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl
```

example (example at line 114) line 114 source

Source comment

We can also combine maps in parallel

example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) : (V × W) →ₗ[K] (U × T) := φ.prodMap ψ

example (example at line 117) line 117 source
Source comment
This is simply done by combining the projections with the universal property
```
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
  φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl
```
example (example at line 121) line 121 source
Source comment
First inclusion map
```
example : V →ₗ[K] V × W := LinearMap.inl K V W
```
example (example at line 124) line 124 source
Source comment
Second inclusion map
```
example : W →ₗ[K] V × W := LinearMap.inr K V W
```
example (example at line 127) line 127 source
Source comment
Universal property of the sum (aka coproduct)
```
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : V × W →ₗ[K] U := φ.coprod ψ
```
example (example at line 130) line 130 source
Source comment
The coproduct map does the expected thing, first component
```
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ :=
…
```
example (example at line 134) line 134 source
Source comment
The coproduct map does the expected thing, second component
```
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ :=
…
```

example (example at line 138) line 138 source

Source comment

The coproduct map is defined in the expected way

example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w :=
…

example (example at line 153) line 153 source
Source comment
The universal property of the direct sum assembles maps from the summands to build a map from the direct sum
```
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
…
```
example (example at line 158) line 158 source
Source comment
The universal property of the direct product assembles maps into the factors to build a map into the direct product
```
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
…
```
example (example at line 162) line 162 source
Source comment
The projection maps from the product
```
example (i : ι) : (Π j, V j) →ₗ[K] V i := LinearMap.proj i
```
example (example at line 165) line 165 source
Source comment
The inclusion maps into the sum
```
example (i : ι) : V i →ₗ[K] (⨁ i, V i) := DirectSum.lof K ι V i
```
example (example at line 168) line 168 source
Source comment
The inclusion maps into the product
```
example (i : ι) : V i →ₗ[K] (Π i, V i) := LinearMap.single K V i
```
example (example at line 171) line 171 source
Source comment
In case `ι` is a finite type, there is an isomorphism between the sum and product.
```
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
…
```