Pi instances for modules

This file defines instances for module and related structures on Pi types.

We also define the natural maps LinearMap.pi and LinearMap.proj on Pi types in the domain and codomain, respectively.

theorem IsSMulRegular.pi {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] {k : α} (hk : ∀ (i : I), IsSMulRegular (f i) k) : IsSMulRegular ((i : I) → f i) k

@[instance_reducible]

instance Pi.module (I : Type u) (f : I → Type v) (α : Type u_1) {r : Semiring α} {m : (i : I) → AddCommMonoid (f i)} [(i : I) → Module α (f i)] : Module α ((i : I) → f i)

Equations

• Pi.module I f α = { toDistribMulAction := Pi.distribMulAction α, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance Pi.Function.module (I : Type u) (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] : Module α (I → β)

A special case of Pi.module for non-dependent types. Lean struggles to elaborate definitions elsewhere in the library without this.

Equations

• Pi.Function.module I α β = Pi.module I (fun (a : I) => β) α

@[instance_reducible]

instance Pi.module' {I : Type u} {f : I → Type v} {g : I → Type u_1} {r : (i : I) → Semiring (f i)} {m : (i : I) → AddCommMonoid (g i)} [(i : I) → Module (f i) (g i)] : Module ((i : I) → f i) ((i : I) → g i)

Equations

• Pi.module' = { toDistribMulAction := Pi.distribMulAction', add_smul := ⋯, zero_smul := ⋯ }

def LinearMap.pi {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (i : ι) → φ i

pi construction for linear functions. From a family of linear functions it produces a linear function into a family of modules.

Equations

• LinearMap.pi f = { toFun := fun (c : M₂) (i : ι) => (f i) c, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.pi_apply {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (c : M₂) (i : ι) : (pi f) c i = (f i) c

theorem LinearMap.pi_eq_zero {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) : pi f = 0 ↔ ∀ (i : ι), f i = 0

theorem LinearMap.pi_zero {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : (pi fun (x : ι) => 0) = 0

theorem LinearMap.pi_comp {R : Type u_1} {M₂ : Type u_3} {M₃ : Type u_4} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : pi f ∘ₗ g = pi fun (i : ι) => f i ∘ₗ g

def LinearMap.const {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] : M₂ →ₗ[R] ι → M₂

The constant linear map, taking x to Function.const ι x.

Equations

• LinearMap.const = LinearMap.pi fun (x : ι) => LinearMap.id

@[simp]

theorem LinearMap.const_apply {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] (x : M₂) : const x = Function.const ι x

def LinearMap.proj {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : ((i : ι) → φ i) →ₗ[R] φ i

The projections from a family of modules are linear maps.

Note: this definition would be called Pi.evalLinearMap if we followed the pattern established by Pi.evalAddHom, Pi.evalMonoidHom, Pi.evalRingHom, ...

Equations

• LinearMap.proj i = { toFun := Function.eval i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_proj {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : ⇑(proj i) = Function.eval i

@[simp]

theorem LinearMap.toAddMonoidHom_proj {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : (proj i).toAddMonoidHom = Pi.evalAddMonoidHom φ i

theorem LinearMap.proj_apply {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) : (proj i) b = b i

@[simp]

theorem LinearMap.proj_pi {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →ₗ[R] φ i) (i : ι) : proj i ∘ₗ pi f = f i

@[simp]

theorem LinearMap.pi_proj {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : pi proj = id

@[simp]

theorem LinearMap.pi_proj_comp {R : Type u_1} {M₂ : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid M₂] [Module R M₂] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : M₂ →ₗ[R] (i : ι) → φ i) : (pi fun (x : ι) => proj x ∘ₗ f) = f

theorem LinearMap.proj_surjective {R : Type u_1} {ι : Type u_5} [Semiring R] {φ : ι → Type u_7} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : Function.Surjective ⇑(proj i)