Addenda to the direct sums and tensor products in mathlib

This file adds some lemmas about direct sums and tensor products in mathlib.

Contents

• DirectSum_equiv_linearmap : if β ≃ₗ[A] γ then DirectSum ι β ≃ₗ[A] DirectSum ι γ
• DirectSum_eq_sum_direct : Given a family x : (i : ι) → β i of indexed types on a fintype ι, we have the identity : (∑ (i : ι), (DirectSum.of β i) (x i)) j = x j.
• iso_hom_tens : isomorphism between $Hom_B(B⊗_AM,N)$ and $Hom_A(M,N)$ for $B$ an A-algebra, M an A-module and N a B-module.

def DirectSum_equiv (ι : Type v) (β γ : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (γ i)] (h : (i : ι) → β i ≃+ γ i) : DirectSum ι β ≃+ DirectSum ι γ

If two types β and γ are indexed by a same type ι, then we have an AddEquiv between DirectSum i β and DirectSum i γ.

Equations

• One or more equations did not get rendered due to their size.

def DirectSum_equiv_linearmap (A : Type) [Semiring A] (ι : Type v) (β γ : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (γ i)] [(i : ι) → Module A (β i)] [(i : ι) → Module A (γ i)] (h : (i : ι) → β i ≃ₗ[A] γ i) : DirectSum ι β ≃ₗ[A] DirectSum ι γ

DirectSum_equiv as a k linear equivalence.

Equations

• DirectSum_equiv_linearmap A ι β γ h = (DirectSum_equiv ι β γ fun (i : ι) => (h i).toAddEquiv).toLinearEquiv ⋯

@[simp]

theorem DirectSum_eq_sum_direct (ι : Type u_1) [hi : Fintype ι] (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (x : (i : ι) → β i) (j : ι) : (∑ i : ι, (DirectSum.of β i) (x i)) j = x j

Given a family x : (i : ι) → β i of indexed types on a fintype ι, we have the identity : (∑ (i : ι), (DirectSum.of β i) (x i)) j = x j.

noncomputable def iso_hom_tens (A : Type u_1) (M : Type u_2) (N : Type u_3) (B : Type u_4) [CommSemiring A] [Semiring B] [Algebra A B] [AddCommMonoid M] [Module A M] [AddCommMonoid N] [Module A N] [Module B N] [IsScalarTower A B N] : (TensorProduct A B M →ₗ[B] N) ≃ₗ[A] M →ₗ[A] N

Isomorphism between $Hom_B(B⊗_AM,N)$ and $Hom_A(M,N)$ for $B$ an A-algebra, M an A-module and N a B-module.

Equations

• One or more equations did not get rendered due to their size.