Skip to content

hom approach of tensor of type p q#1

Open
jjaassoonn wants to merge 19 commits intomainfrom
zjj/test-hom-approach
Open

hom approach of tensor of type p q#1
jjaassoonn wants to merge 19 commits intomainfrom
zjj/test-hom-approach

Conversation

@jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Aug 1, 2024

  1. a tensor of type $(p, q)$ is a $k$ linear map $V^{\otimes^q} \to V^{\otimes^p}$.
  2. a $k$-object of type $(p,q)$ is a $k$ vector space $V$ with a tensor $\Phi$ of type $(p, q)$.
  3. a $k$-object morphism between $(V, \Phi) \to (W, \Psi)$ is a $k$ linear map $f$ such that
V^q -f^q-> W^q
  |\Phi             |\Psi
  v                   v
V^p -f^p-> W^p
  1. if $K/k$ is field extension, there is functor from $k$-object to $K$-object sending $(V, \Phi)$ to $(V_K, \Phi_K)$.
  2. if $\sigma \in \mathrm{Gal}(K/k)$ and $f$ is a $K$-morphism between $(V_K, \Phi_K)$ and $(W_K, \Psi_K)$, $\sigma$ induces another $K$-morphism by conjugation

simp only [extendScalars_carrier, ← LinearMap.comp_assoc]
rfl

def inducedByGal (σ : K ≃ₐ[k] K) (f : V.extendScalars K bV ⟶ W.extendScalars K bW) :
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the action of $\mathrm{Gal}(K/k)$ on $K$-morphism between $V_K$ and $W_K$

Copy link
Owner

@Whysoserioushah Whysoserioushah left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

牛啊wk

@Whysoserioushah Whysoserioushah marked this pull request as ready for review October 26, 2024 14:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants