Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.Tensors.Product
public import Physlib.Relativity.Tensors.Evaluation
public import Mathlib.Topology.Algebra.Module.FiniteDimensionTensorial class
i. Overview
We define a class called Tensorial.
This class is used to enable the use of index notation on a type M via a linear equivalence to a
tensor of a TensorSpecies.
We define the class Tensorial here, and provide an API around its use.
ii. Key results
Tensorial : The class used to allow index notation on a type M.
Tensorial.numIndices : The number of indices of an element of an M
carrying a tensorial instance.
Tensorial.mulAction : The action of the group G on a
type M carrying a tensorial instance.
Tensorial.prod : The product of two tensorial instances is a tensorial instance.
iii. Table of contents
A. Defining the tensorial class
A.1. Tensors carry a tensorial instance
A.2. The number of indices
B. The action of the group on a module with a tensorial instance
B.1. Relation between the action and the equivalence to tensors
B.2. Linear properties of the action
B.3. The action as a linear map
B.4. The SMulCommClass property
C. Properties of the basis
D. Products of tensorial instances
D.1. The equivalence to tensors on products
D.2. The group action on products
D.3. The basis on products
E. Continuous properties
E.1. Finite dimensionality
E.2. The map to tensors as a continuous linear equivalence
E.3. The Lorentz action as a continuous linear equivalence
iv. References
There are no known references for this material.
@[expose] public sectionattribute [-simp] LinearEquiv.cast_applyA. Defining the tensorial class
We first define the Tensorial class.
The tensorial class is used to define a tensor structure on a type M through a
linear equivalence with a module S.Tensor c for S a tensor species.
The equivalence between M and S.Tensor c in a tensorial instance.
class Tensorial {n : outParam ℕ}
{k : outParam Type} [CommRing k] {C : outParam Type} {G : outParam Type} [Group G]
{V :outParam (C → Type)} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
{basisIdx : outParam (C → Type)} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
{rep : outParam ((c : C) → Representation k G (V c))}
{b : outParam ((c : C) → Module.Basis (basisIdx c) k (V c))}
(S : outParam (TensorSpecies k C G V basisIdx rep b))
(c :outParam (Fin n → C)) (M : Type)
[AddCommMonoid M] [Module k M] where toTensor : M ≃ₗ[k] S.Tensor cA.1. Tensors carry a tensorial instance
The module of tensors of a tensor species carries a canonical tensorial instance, through the equivalence.
k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)n:ℕS:TensorSpecies k C G V basisIdx rep bc:Fin n → Ct:S.Tensor c⊢ (self S c).1 t = t
All goals completed! 🐙A.2. The number of indices
B. The action of the group on a module with a tensorial instance
We now define the action of the group G on a type M carrying a tensorial instance.
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c Mg:Gh:Gm:M⊢ (g * h) • m = toTensor.symm ((g * h) • toTensor m)
All goals completed! 🐙B.1. Relation between the action and the equivalence to tensors
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Gt:Minst✝:S.Tensorial c M⊢ g • t = inst✝.1.symm (g • inst✝.1 t)
All goals completed! 🐙k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Gt:Minst✝:S.Tensorial c M⊢ toTensor (toTensor.symm (g • toTensor t)) = g • toTensor t
All goals completed! 🐙k:Typeinst✝⁷:CommRing kC:TypeG:Typeinst✝⁶:Group GV:C → Typeinst✝⁵:(c : C) → AddCommGroup (V c)inst✝⁴:(c : C) → Module k (V c)basisIdx:C → Typeinst✝³:(c : C) → Fintype (basisIdx c)inst✝²:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝¹:AddCommMonoid Minst✝:Module k Mg:Gt:S.Tensor cself:S.Tensorial c M⊢ toTensor.symm (g • toTensor (toTensor.symm t)) = toTensor.symm (g • t)
All goals completed! 🐙B.2. Linear properties of the action
set_option backward.isDefEq.respectTransparency false in
noncomputable instance (priority := high) distribMulAction [Tensorial S c M] :
DistribMulAction G M where
smul_add g m m' := k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c Mg:Gm:Mm':M⊢ g • (m + m') = g • m + g • m'
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c Mg:Gm:Mm':M⊢ toTensor (g • (m + m')) = toTensor (g • m + g • m')
All goals completed! 🐙
smul_zero g := k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c Mg:G⊢ g • 0 = 0
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c Mg:G⊢ toTensor (g • 0) = toTensor 0
All goals completed! 🐙B.3. The action as a linear map
The action of the group on a Tensorial instance as a linear map.
set_option backward.isDefEq.respectTransparency false innoncomputable def smulLinearMap (g : G) [Tensorial S c M] : M →ₗ[k] M where
toFun m := g • m
map_add' x y := k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Ginst✝:S.Tensorial c Mx:My:M⊢ g • (x + y) = g • x + g • y
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Ginst✝:S.Tensorial c Mx:My:M⊢ toTensor (g • (x + y)) = toTensor (g • x + g • y)
All goals completed! 🐙
map_smul' c x := k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc✝:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Ginst✝:S.Tensorial c Mc:kx:M⊢ g • c • x = (RingHom.id k) c • g • x
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc✝:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Mg:Ginst✝:S.Tensorial c Mc:kx:M⊢ toTensor (g • c • x) = toTensor ((RingHom.id k) c • g • x)
All goals completed! 🐙lemma smulLinearMap_apply {g : G} [Tensorial S c M] (m : M) :
smulLinearMap g m = g • m := rflB.4. The SMulCommClass property
set_option backward.isDefEq.respectTransparency false in
instance [Tensorial S c M] : SMulCommClass k G M where
smul_comm c g m := k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc✝:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c✝ Mc:kg:Gm:M⊢ c • g • m = g • c • m
k:Typeinst✝⁸:CommRing kC:TypeG:Typeinst✝⁷:Group GV:C → Typeinst✝⁶:(c : C) → AddCommGroup (V c)inst✝⁵:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁴:(c : C) → Fintype (basisIdx c)inst✝³:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc✝:Fin n → CM:Typeinst✝²:AddCommMonoid Minst✝¹:Module k Minst✝:S.Tensorial c✝ Mc:kg:Gm:M⊢ toTensor (c • g • m) = toTensor (g • c • m)
All goals completed! 🐙C. Properties of the basis
We now prove some properties of the basis induced on a Tensorial instance.
lemma basis_toTensor_apply [Tensorial S c M] (m : M) :
(Tensor.basis c).repr (toTensor m) = ((Tensor.basis c).map toTensor.symm).repr m := rflD. Products of tensorial instances
D.1. The equivalence to tensors on products
lemma toTensor_tprod {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type}
[Tensorial S c M] [AddCommMonoid M₂] [Module k M₂]
[Tensorial S c2 M₂] (m : M) (m2 : M₂) :
toTensor (m ⊗ₜ[k] m2) = Tensor.prodT (toTensor m) (toTensor m2) := rflD.2. The group action on products
All goals completed! 🐙D.3. The basis on products
attribute [-simp] Matrix.cons_val_zero Matrix.cons_val Fin.succAbove_zeroE. Continuous properties
E.1. Finite dimensionality
instance [Tensorial S c M] : FiniteDimensional k M := LinearEquiv.finiteDimensional
(Tensorial.toTensor (M := M)).symmE.2. The map to tensors as a continuous linear equivalence
The map from a type carrying an Tensorial instance to tensors, as a continuous linear map.
def toTensorCLM [IsTopologicalAddGroup M]
[ContinuousSMul k M] [Tensorial S c M] [T2Space M] : M ≃L[k] (S.Tensor c) where
toLinearMap := (Tensorial.toTensor (M := M))
invFun := (Tensorial.toTensor (M := M)).symm
left_inv x := k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space Mx:M⊢ toTensor.symm ((↑toTensor).toFun x) = x All goals completed! 🐙
right_inv x := k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space Mx:S.Tensor c⊢ (↑toTensor).toFun (toTensor.symm x) = x All goals completed! 🐙
continuous_toFun := k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space M⊢ Continuous (↑toTensor).toFun
k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space Me:M →L[k] S.Tensor c := LinearMap.toContinuousLinearMap ↑toTensor⊢ Continuous (↑toTensor).toFun
k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space Me:M →L[k] S.Tensor c := LinearMap.toContinuousLinearMap ↑toTensor⊢ Continuous ⇑e
All goals completed! 🐙
continuous_invFun := k✝:Typeinst✝²⁰:CommRing k✝C✝:TypeG✝:Typeinst✝¹⁹:Group G✝V✝:C✝ → Typeinst✝¹⁸:(c : C✝) → AddCommGroup (V✝ c)inst✝¹⁷:(c : C✝) → Module k✝ (V✝ c)basisIdx✝:C✝ → Typeinst✝¹⁶:(c : C✝) → Fintype (basisIdx✝ c)inst✝¹⁵:(c : C✝) → DecidableEq (basisIdx✝ c)rep✝:(c : C✝) → Representation k✝ G✝ (V✝ c)b✝:(c : C✝) → Module.Basis (basisIdx✝ c) k✝ (V✝ c)S✝:TensorSpecies k✝ C✝ G✝ V✝ basisIdx✝ rep✝ b✝n:ℕc✝:Fin n → C✝M✝:Typeinst✝¹⁴:AddCommMonoid M✝inst✝¹³:Module k✝ M✝k:Typeinst✝¹²:RCLike kC:TypeG:Typeinst✝¹¹:Group GV:C → Typeinst✝¹⁰:(c : C) → AddCommGroup (V c)inst✝⁹:(c : C) → Module k (V c)basisIdx:C → Typeinst✝⁸:(c : C) → Fintype (basisIdx c)inst✝⁷:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin n → CM:Typeinst✝⁶:AddCommGroup Minst✝⁵:Module k Minst✝⁴:TopologicalSpace Minst✝³:IsTopologicalAddGroup Minst✝²:ContinuousSMul k Minst✝¹:S.Tensorial c Minst✝:T2Space M⊢ Continuous ⇑toTensor.symm All goals completed! 🐙