Pi types of modules #
This file defines constructors for linear maps whose domains or codomains are pi types.
It contains theorems relating these to each other, as well as to LinearMap.ker.
Main definitions #
- pi types in the codomain:
- pi types in the domain:
def
LinearMap.pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ 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 = let __src := Pi.addHom fun (i : ι) => (f i).toAddHom; { toAddHom := { toFun := fun (c : M₂) (i : ι) => (f i) c, map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.pi_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ i)
(c : M₂)
(i : ι)
:
(LinearMap.pi f) c i = (f i) c
theorem
LinearMap.ker_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ i)
:
LinearMap.ker (LinearMap.pi f) = ⨅ (i : ι), LinearMap.ker (f i)
theorem
LinearMap.pi_eq_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ i)
:
LinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0
theorem
LinearMap.pi_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
:
(LinearMap.pi fun (i : ι) => 0) = 0
theorem
LinearMap.pi_comp
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ i)
(g : M₃ →ₗ[R] M₂)
:
LinearMap.pi f ∘ₗ g = LinearMap.pi fun (i : ι) => f i ∘ₗ g
def
LinearMap.proj
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(i : ι)
:
The projections from a family of modules are linear maps.
Note: known here as LinearMap.proj, this construction is in other categories called eval, for
example Pi.evalMonoidHom, Pi.evalRingHom.
Equations
- LinearMap.proj i = { toAddHom := { toFun := Function.eval i, map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.coe_proj
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(i : ι)
:
⇑(LinearMap.proj i) = Function.eval i
theorem
LinearMap.proj_apply
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(i : ι)
(b : (i : ι) → φ i)
:
(LinearMap.proj i) b = b i
theorem
LinearMap.proj_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(f : (i : ι) → M₂ →ₗ[R] φ i)
(i : ι)
:
LinearMap.proj i ∘ₗ LinearMap.pi f = f i
theorem
LinearMap.iInf_ker_proj
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
:
⨅ (i : ι), LinearMap.ker (LinearMap.proj i) = ⊥
instance
LinearMap.CompatibleSMul.pi
(R : Type u_1)
(S : Type u_2)
(M : Type u_3)
(N : Type u_4)
(ι : Type u_5)
[Semiring S]
[AddCommMonoid M]
[AddCommMonoid N]
[SMul R M]
[SMul R N]
[Module S M]
[Module S N]
[LinearMap.CompatibleSMul M N R S]
:
LinearMap.CompatibleSMul M (ι → N) R S
Equations
- ⋯ = ⋯
@[simp]
theorem
LinearMap.compLeft_apply
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
(f : M₂ →ₗ[R] M₃)
(I : Type u_1)
(h : I → M₂)
:
∀ (a : I), (LinearMap.compLeft f I) h a = (⇑f ∘ h) a
def
LinearMap.compLeft
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
(f : M₂ →ₗ[R] M₃)
(I : Type u_1)
:
Linear map between the function spaces I → M₂ and I → M₃, induced by a linear map f
between M₂ and M₃.
Equations
- LinearMap.compLeft f I = let __src := AddMonoidHom.compLeft (LinearMap.toAddMonoidHom f) I; { toAddHom := { toFun := fun (h : I → M₂) => ⇑f ∘ h, map_add' := ⋯ }, map_smul' := ⋯ }
theorem
LinearMap.apply_single
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[AddCommMonoid M]
[Module R M]
[DecidableEq ι]
(f : (i : ι) → φ i →ₗ[R] M)
(i : ι)
(j : ι)
(x : φ i)
:
def
LinearMap.single
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[DecidableEq ι]
(i : ι)
:
The LinearMap version of AddMonoidHom.single and Pi.single.
Equations
- LinearMap.single i = let __src := AddMonoidHom.single φ i; { toAddHom := { toFun := Pi.single i, map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.coe_single
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[DecidableEq ι]
(i : ι)
:
⇑(LinearMap.single i) = Pi.single i
@[simp]
theorem
LinearMap.lsum_symm_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[Semiring R]
(φ : ι → Type i)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(S : Type u_1)
[AddCommMonoid M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[Module S M]
[SMulCommClass R S M]
(f : ((i : ι) → φ i) →ₗ[R] M)
(i : ι)
:
(LinearEquiv.symm (LinearMap.lsum R φ S)) f i = LinearMap.comp f (LinearMap.single i)
def
LinearMap.lsum
(R : Type u)
{M : Type v}
{ι : Type x}
[Semiring R]
(φ : ι → Type i)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(S : Type u_1)
[AddCommMonoid M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[Module S M]
[SMulCommClass R S M]
:
The linear equivalence between linear functions on a finite product of modules and families of functions on these modules. See note [bundled maps over different rings].
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearMap.lsum_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[Semiring R]
(φ : ι → Type i)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(S : Type u_1)
[AddCommMonoid M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[Module S M]
[SMulCommClass R S M]
(f : (i : ι) → φ i →ₗ[R] M)
:
(LinearMap.lsum R φ S) f = Finset.sum Finset.univ fun (i : ι) => f i ∘ₗ LinearMap.proj i
@[simp]
theorem
LinearMap.lsum_single
{ι : Type u_1}
{R : Type u_2}
[Fintype ι]
[DecidableEq ι]
[CommRing R]
{M : ι → Type u_3}
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
:
(LinearMap.lsum R M R) LinearMap.single = LinearMap.id
theorem
LinearMap.pi_ext
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[Finite ι]
[DecidableEq ι]
[AddCommMonoid M]
[Module R M]
{f : ((i : ι) → φ i) →ₗ[R] M}
{g : ((i : ι) → φ i) →ₗ[R] M}
(h : ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x))
:
f = g
theorem
LinearMap.pi_ext_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[Finite ι]
[DecidableEq ι]
[AddCommMonoid M]
[Module R M]
{f : ((i : ι) → φ i) →ₗ[R] M}
{g : ((i : ι) → φ i) →ₗ[R] M}
:
theorem
LinearMap.pi_ext'
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[Finite ι]
[DecidableEq ι]
[AddCommMonoid M]
[Module R M]
{f : ((i : ι) → φ i) →ₗ[R] M}
{g : ((i : ι) → φ i) →ₗ[R] M}
(h : ∀ (i : ι), f ∘ₗ LinearMap.single i = g ∘ₗ LinearMap.single i)
:
f = g
This is used as the ext lemma instead of LinearMap.pi_ext for reasons explained in
note [partially-applied ext lemmas].
theorem
LinearMap.pi_ext'_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[Finite ι]
[DecidableEq ι]
[AddCommMonoid M]
[Module R M]
{f : ((i : ι) → φ i) →ₗ[R] M}
{g : ((i : ι) → φ i) →ₗ[R] M}
:
f = g ↔ ∀ (i : ι), f ∘ₗ LinearMap.single i = g ∘ₗ LinearMap.single i
def
LinearMap.iInfKerProjEquiv
(R : Type u)
{ι : Type x}
[Semiring R]
(φ : ι → Type i)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{I : Set ι}
{J : Set ι}
[DecidablePred fun (i : ι) => i ∈ I]
(hd : Disjoint I J)
(hu : Set.univ ⊆ I ∪ J)
:
↥(⨅ i ∈ J, LinearMap.ker (LinearMap.proj i)) ≃ₗ[R] (i : ↑I) → φ ↑i
If I and J are disjoint index sets, the product of the kernels of the Jth projections of
φ is linearly equivalent to the product over I.
Equations
- One or more equations did not get rendered due to their size.
def
LinearMap.diag
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[DecidableEq ι]
(i : ι)
(j : ι)
:
diag i j is the identity map if i = j. Otherwise it is the constant 0 map.
Equations
- LinearMap.diag i j = Function.update 0 i LinearMap.id j
theorem
LinearMap.update_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
{φ : ι → Type i}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[DecidableEq ι]
(f : (i : ι) → M₂ →ₗ[R] φ i)
(c : M₂)
(i : ι)
(j : ι)
(b : M₂ →ₗ[R] φ i)
:
(Function.update f i b j) c = Function.update (fun (i : ι) => (f i) c) i (b c) j
theorem
LinearMap.pi_apply_eq_sum_univ
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[Semiring R]
[AddCommMonoid M₂]
[Module R M₂]
[Fintype ι]
[DecidableEq ι]
(f : (ι → R) →ₗ[R] M₂)
(x : ι → R)
:
f x = Finset.sum Finset.univ fun (i : ι) => x i • f fun (j : ι) => if i = j then 1 else 0
A linear map f applied to x : ι → R can be computed using the image under f of elements
of the canonical basis.
def
Submodule.pi
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(I : Set ι)
(p : (i : ι) → Submodule R (φ i))
:
Submodule R ((i : ι) → φ i)
A version of Set.pi for submodules. Given an index set I and a family of submodules
p : (i : ι) → Submodule R (φ i), pi I s is the submodule of dependent functions
f : (i : ι) → φ i such that f i belongs to p a whenever i ∈ I.
Equations
- Submodule.pi I p = { toAddSubmonoid := { toAddSubsemigroup := { carrier := Set.pi I fun (i : ι) => ↑(p i), add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }
@[simp]
theorem
Submodule.mem_pi
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{I : Set ι}
{p : (i : ι) → Submodule R (φ i)}
{x : (i : ι) → φ i}
:
x ∈ Submodule.pi I p ↔ ∀ i ∈ I, x i ∈ p i
@[simp]
theorem
Submodule.coe_pi
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{I : Set ι}
{p : (i : ι) → Submodule R (φ i)}
:
↑(Submodule.pi I p) = Set.pi I fun (i : ι) => ↑(p i)
@[simp]
theorem
Submodule.pi_empty
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(p : (i : ι) → Submodule R (φ i))
:
Submodule.pi ∅ p = ⊤
@[simp]
theorem
Submodule.pi_top
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(s : Set ι)
:
(Submodule.pi s fun (i : ι) => ⊤) = ⊤
theorem
Submodule.pi_mono
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{p : (i : ι) → Submodule R (φ i)}
{q : (i : ι) → Submodule R (φ i)}
{s : Set ι}
(h : ∀ i ∈ s, p i ≤ q i)
:
Submodule.pi s p ≤ Submodule.pi s q
theorem
Submodule.biInf_comap_proj
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{I : Set ι}
{p : (i : ι) → Submodule R (φ i)}
:
⨅ i ∈ I, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi I p
theorem
Submodule.iInf_comap_proj
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{p : (i : ι) → Submodule R (φ i)}
:
⨅ (i : ι), Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi Set.univ p
theorem
Submodule.iSup_map_single
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{p : (i : ι) → Submodule R (φ i)}
[DecidableEq ι]
[Finite ι]
:
⨆ (i : ι), Submodule.map (LinearMap.single i) (p i) = Submodule.pi Set.univ p
theorem
Submodule.le_comap_single_pi
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[DecidableEq ι]
(p : (i : ι) → Submodule R (φ i))
{i : ι}
:
p i ≤ Submodule.comap (LinearMap.single i) (Submodule.pi Set.univ p)
def
LinearEquiv.piCongrRight
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[(i : ι) → AddCommMonoid (ψ i)]
[(i : ι) → Module R (ψ i)]
(e : (i : ι) → φ i ≃ₗ[R] ψ i)
:
Combine a family of linear equivalences into a linear equivalence of pi-types.
This is Equiv.piCongrRight as a LinearEquiv
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearEquiv.piCongrRight_apply
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[(i : ι) → AddCommMonoid (ψ i)]
[(i : ι) → Module R (ψ i)]
(e : (i : ι) → φ i ≃ₗ[R] ψ i)
(f : (i : ι) → φ i)
(i : ι)
:
(LinearEquiv.piCongrRight e) f i = (e i) (f i)
@[simp]
theorem
LinearEquiv.piCongrRight_refl
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
:
(LinearEquiv.piCongrRight fun (j : ι) => LinearEquiv.refl R (φ j)) = LinearEquiv.refl R ((i : ι) → φ i)
@[simp]
theorem
LinearEquiv.piCongrRight_symm
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[(i : ι) → AddCommMonoid (ψ i)]
[(i : ι) → Module R (ψ i)]
(e : (i : ι) → φ i ≃ₗ[R] ψ i)
:
LinearEquiv.symm (LinearEquiv.piCongrRight e) = LinearEquiv.piCongrRight fun (i : ι) => LinearEquiv.symm (e i)
@[simp]
theorem
LinearEquiv.piCongrRight_trans
{R : Type u}
{ι : Type x}
[Semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
{χ : ι → Type u_3}
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[(i : ι) → AddCommMonoid (ψ i)]
[(i : ι) → Module R (ψ i)]
[(i : ι) → AddCommMonoid (χ i)]
[(i : ι) → Module R (χ i)]
(e : (i : ι) → φ i ≃ₗ[R] ψ i)
(f : (i : ι) → ψ i ≃ₗ[R] χ i)
:
LinearEquiv.piCongrRight e ≪≫ₗ LinearEquiv.piCongrRight f = LinearEquiv.piCongrRight fun (i : ι) => e i ≪≫ₗ f i
@[simp]
theorem
LinearEquiv.piCongrLeft'_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[Semiring R]
(φ : ι → Type u_1)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(e : ι ≃ ι')
:
∀ (a : (a : ι) → φ a) (b : ι'), (LinearEquiv.piCongrLeft' R φ e) a b = a (e.symm b)
@[simp]
theorem
LinearEquiv.piCongrLeft'_symm_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[Semiring R]
(φ : ι → Type u_1)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(e : ι ≃ ι')
:
∀ (a : (b : ι') → φ (e.symm b)) (a_1 : ι), (LinearEquiv.symm (LinearEquiv.piCongrLeft' R φ e)) a a_1 = ⋯ ▸ a (e a_1)
def
LinearEquiv.piCongrLeft'
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[Semiring R]
(φ : ι → Type u_1)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(e : ι ≃ ι')
:
Transport dependent functions through an equivalence of the base space.
This is Equiv.piCongrLeft' as a LinearEquiv.
Equations
- One or more equations did not get rendered due to their size.
def
LinearEquiv.piCongrLeft
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[Semiring R]
(φ : ι → Type u_1)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
(e : ι' ≃ ι)
:
Transporting dependent functions through an equivalence of the base, expressed as a "simplification".
This is Equiv.piCongrLeft as a LinearEquiv
Equations
- LinearEquiv.piCongrLeft R φ e = LinearEquiv.symm (LinearEquiv.piCongrLeft' R φ e.symm)
def
LinearEquiv.piOptionEquivProd
(R : Type u)
[Semiring R]
{ι : Type u_4}
{M : Option ι → Type u_5}
[(i : Option ι) → AddCommGroup (M i)]
[(i : Option ι) → Module R (M i)]
:
This is Equiv.piOptionEquivProd as a LinearEquiv
Equations
- One or more equations did not get rendered due to their size.
def
LinearEquiv.piRing
(R : Type u)
(M : Type v)
(ι : Type x)
[Semiring R]
(S : Type u_4)
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
:
Linear equivalence between linear functions Rⁿ → M and Mⁿ. The spaces Rⁿ and Mⁿ
are represented as ι → R and ι → M, respectively, where ι is a finite type.
This as an S-linear equivalence, under the assumption that S acts on M commuting with R.
When R is commutative, we can take this to be the usual action with S = R.
Otherwise, S = ℕ shows that the equivalence is additive.
See note [bundled maps over different rings].
Equations
- LinearEquiv.piRing R M ι S = LinearEquiv.trans (LinearEquiv.symm (LinearMap.lsum R (fun (x : ι) => R) S)) (LinearEquiv.piCongrRight fun (x : ι) => LinearMap.ringLmapEquivSelf R S M)
@[simp]
theorem
LinearEquiv.piRing_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
(S : Type u_4)
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
(f : (ι → R) →ₗ[R] M)
(i : ι)
:
(LinearEquiv.piRing R M ι S) f i = f (Pi.single i 1)
@[simp]
theorem
LinearEquiv.piRing_symm_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[Semiring R]
(S : Type u_4)
[Fintype ι]
[DecidableEq ι]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
(f : ι → M)
(g : ι → R)
:
((LinearEquiv.symm (LinearEquiv.piRing R M ι S)) f) g = Finset.sum Finset.univ fun (i : ι) => g i • f i
def
LinearEquiv.sumArrowLequivProdArrow
(α : Type u_5)
(β : Type u_6)
(R : Type u_7)
(M : Type u_8)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equiv.sumArrowEquivProdArrow as a linear equivalence.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearEquiv.sumArrowLequivProdArrow_apply_fst
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_5}
{β : Type u_6}
(f : α ⊕ β → M)
(a : α)
:
((LinearEquiv.sumArrowLequivProdArrow α β R M) f).1 a = f (Sum.inl a)
@[simp]
theorem
LinearEquiv.sumArrowLequivProdArrow_apply_snd
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_5}
{β : Type u_6}
(f : α ⊕ β → M)
(b : β)
:
((LinearEquiv.sumArrowLequivProdArrow α β R M) f).2 b = f (Sum.inr b)
@[simp]
theorem
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_5}
{β : Type u_6}
(f : α → M)
(g : β → M)
(a : α)
:
(LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow α β R M)) (f, g) (Sum.inl a) = f a
@[simp]
theorem
LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{α : Type u_5}
{β : Type u_6}
(f : α → M)
(g : β → M)
(b : β)
:
(LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow α β R M)) (f, g) (Sum.inr b) = g b
@[simp]
theorem
LinearEquiv.funUnique_symm_apply
(ι : Type u_5)
(R : Type u_6)
(M : Type u_7)
[Unique ι]
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
⇑(LinearEquiv.symm (LinearEquiv.funUnique ι R M)) = uniqueElim
@[simp]
theorem
LinearEquiv.funUnique_apply
(ι : Type u_5)
(R : Type u_6)
(M : Type u_7)
[Unique ι]
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
⇑(LinearEquiv.funUnique ι R M) = Function.eval default
@[simp]
theorem
LinearEquiv.piFinTwo_symm_apply
(R : Type u)
[Semiring R]
(M : Fin 2 → Type v)
[(i : Fin 2) → AddCommMonoid (M i)]
[(i : Fin 2) → Module R (M i)]
:
⇑(LinearEquiv.symm (LinearEquiv.piFinTwo R M)) = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
def
LinearEquiv.piFinTwo
(R : Type u)
[Semiring R]
(M : Fin 2 → Type v)
[(i : Fin 2) → AddCommMonoid (M i)]
[(i : Fin 2) → Module R (M i)]
:
Linear equivalence between dependent functions (i : Fin 2) → M i and M 0 × M 1.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LinearEquiv.piFinTwo_apply
(R : Type u)
[Semiring R]
(M : Fin 2 → Type v)
[(i : Fin 2) → AddCommMonoid (M i)]
[(i : Fin 2) → Module R (M i)]
:
⇑(LinearEquiv.piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)
@[simp]
theorem
LinearEquiv.finTwoArrow_apply
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
⇑(LinearEquiv.finTwoArrow R M) = fun (f : Fin 2 → M) => (f 0, f 1)
@[simp]
theorem
LinearEquiv.finTwoArrow_symm_apply
(R : Type u)
(M : Type v)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
⇑(LinearEquiv.symm (LinearEquiv.finTwoArrow R M)) = fun (x : M × M) => ![x.1, x.2]
@[simp]
theorem
Function.ExtendByZero.linearMap_apply
(R : Type u)
{ι : Type x}
{η : Type x}
[Semiring R]
(s : ι → η)
(f : ι → R)
:
∀ (a : η), (Function.ExtendByZero.linearMap R s) f a = Function.extend s f 0 a
noncomputable def
Function.ExtendByZero.linearMap
(R : Type u)
{ι : Type x}
{η : Type x}
[Semiring R]
(s : ι → η)
:
Function.extend s f 0 as a bundled linear map.
Equations
- Function.ExtendByZero.linearMap R s = let __src := Function.ExtendByZero.hom R s; { toAddHom := { toFun := fun (f : ι → R) => Function.extend s f 0, map_add' := ⋯ }, map_smul' := ⋯ }
Bundled versions of Matrix.vecCons and Matrix.vecEmpty #
The idea of these definitions is to be able to define a map as x ↦ ![f₁ x, f₂ x, f₃ x], where
f₁ f₂ f₃ are already linear maps, as f₁.vecCons <| f₂.vecCons <| f₃.vecCons <| vecEmpty.
While the same thing could be achieved using LinearMap.pi ![f₁, f₂, f₃], this is not
definitionally equal to the result using LinearMap.vecCons, as Fin.cases and function
application do not commute definitionally.
Versions for when f₁ f₂ f₃ are bilinear maps are also provided.
def
LinearMap.vecEmpty
{R : Type u}
{M : Type v}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₃]
[Module R M]
[Module R M₃]
:
The linear map defeq to Matrix.vecEmpty
Equations
- LinearMap.vecEmpty = { toAddHom := { toFun := fun (x : M) => ![], map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.vecEmpty_apply
{R : Type u}
{M : Type v}
{M₃ : Type y}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₃]
[Module R M]
[Module R M₃]
(m : M)
:
LinearMap.vecEmpty m = ![]
def
LinearMap.vecCons
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
{n : ℕ}
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] Fin n → M₂)
:
A linear map into Fin n.succ → M₃ can be built out of a map into M₃ and a map into
Fin n → M₃.
Equations
- LinearMap.vecCons f g = { toAddHom := { toFun := fun (m : M) => Matrix.vecCons (f m) (g m), map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.vecCons_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
{n : ℕ}
(f : M →ₗ[R] M₂)
(g : M →ₗ[R] Fin n → M₂)
(m : M)
:
(LinearMap.vecCons f g) m = Matrix.vecCons (f m) (g m)
@[simp]
theorem
LinearMap.vecEmpty₂_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
:
∀ (x : M), LinearMap.vecEmpty₂ x = LinearMap.vecEmpty
def
LinearMap.vecEmpty₂
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
:
The empty bilinear map defeq to Matrix.vecEmpty
Equations
- LinearMap.vecEmpty₂ = { toAddHom := { toFun := fun (x : M) => LinearMap.vecEmpty, map_add' := ⋯ }, map_smul' := ⋯ }
@[simp]
theorem
LinearMap.vecCons₂_apply
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
{n : ℕ}
(f : M →ₗ[R] M₂ →ₗ[R] M₃)
(g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃)
(m : M)
:
(LinearMap.vecCons₂ f g) m = LinearMap.vecCons (f m) (g m)
def
LinearMap.vecCons₂
{R : Type u}
{M : Type v}
{M₂ : Type w}
{M₃ : Type y}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M]
[Module R M₂]
[Module R M₃]
{n : ℕ}
(f : M →ₗ[R] M₂ →ₗ[R] M₃)
(g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃)
:
A bilinear map into Fin n.succ → M₃ can be built out of a map into M₃ and a map into
Fin n → M₃
Equations
- LinearMap.vecCons₂ f g = { toAddHom := { toFun := fun (m : M) => LinearMap.vecCons (f m) (g m), map_add' := ⋯ }, map_smul' := ⋯ }