EncodingLinearity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.EncodingLinearity.intertwining line 15
Source documentation
Elements whose action commutes with a specified linear map form a subalgebra.
```
def intertwining (f : M →ₗ[k] N) : Subalgebra k (B P) where
…
```

theorem OAI.LittleFinitistic.EncodingLinearity.map_smul line 31

Source documentation

Full B-linearity follows from the actual three vertex and two finite arrow lists. Length-two actions require no additional hypothesis.

theorem map_smul (f : M →ₗ[k] N)
    (hv : ∀ i x, f (ThreeVertexAlgebra.vertex (composition P) i • x) =
      ThreeVertexAlgebra.vertex (composition P) i • f x)
    (h01 : ∀ a x, f (arrow01 P a • x) = arrow01 P a • f x)
    (h12 : ∀ a x, f (arrow12 P a • x) = arrow12 P a • f x)
    (b : B P) (x : M) : f (b • x) = b • f x := by
…

Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex

def OAI.LittleFinitistic.EncodingLinearity.linearMap line 42

Source documentation

The original k-linear map, upgraded without changing its values.

def linearMap (f : M →ₗ[k] N)
    (hv : ∀ i x, f (ThreeVertexAlgebra.vertex (composition P) i • x) =
      ThreeVertexAlgebra.vertex (composition P) i • f x)
    (h01 : ∀ a x, f (arrow01 P a • x) = arrow01 P a • f x)
    (h12 : ∀ a x, f (arrow12 P a • x) = arrow12 P a • f x) : M →ₗ[B P] N where
…

Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex

def OAI.LittleFinitistic.EncodingLinearity.linearEquiv line 53

Source documentation

A vector-space isomorphism respecting the finite generating actions is a B-module isomorphism with exactly the original forward and inverse functions.

def linearEquiv (f : M ≃ₗ[k] N)
    (hv : ∀ i x, f (ThreeVertexAlgebra.vertex (composition P) i • x) =
      ThreeVertexAlgebra.vertex (composition P) i • f x)
    (h01 : ∀ a x, f (arrow01 P a • x) = arrow01 P a • f x)
    (h12 : ∀ a x, f (arrow12 P a • x) = arrow12 P a • f x) : M ≃ₗ[B P] N :=
…

Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex