Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear #17932

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat: algebraic properties of LinearMap.compMultilinear #17932

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
69f1798
feat: algebraic properties of `LinearMap.compMultilinear`
eric-wieser Oct 18, 2024
02370cc
why not bundle it too
eric-wieser Oct 18, 2024
5b29ee7
variable cleanup
eric-wieser Oct 18, 2024
9e71aa5
one more
eric-wieser Oct 18, 2024
a644005
golf
eric-wieser Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 45 additions & 11 deletions Mathlib/LinearAlgebra/Alternating/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -407,19 +407,12 @@ end AlternatingMap

namespace LinearMap

variable {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]
variable {S : Type*} {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]

/-- Composing an alternating map with a linear map on the left gives again an alternating map. -/
def compAlternatingMap (g : N →ₗ[R] N₂) : (M [⋀^ι]→ₗ[R] N) →+ (M [⋀^ι]→ₗ[R] N₂) where
toFun f :=
{ g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N) with
map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }
map_zero' := by
ext
simp
map_add' a b := by
ext
simp
def compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι]→ₗ[R] N₂ where
__ := g.compMultilinearMap (f : MultilinearMap R (fun _ : ι => M) N)
map_eq_zero_of_eq' v i j h hij := by simp [f.map_eq_zero_of_eq v h hij]

@[simp]
theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
Expand All @@ -431,6 +424,47 @@ theorem compAlternatingMap_apply (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R]
g.compAlternatingMap f m = g (f m) :=
rfl

@[simp]
theorem compAlternatingMap_zero (g : N →ₗ[R] N₂) :
g.compAlternatingMap (0 : M [⋀^ι]→ₗ[R] N) = 0 :=
AlternatingMap.ext fun _ => map_zero g

@[simp]
theorem zero_compAlternatingMap (f: M [⋀^ι]→ₗ[R] N) :
(0 : N →ₗ[R] N₂).compAlternatingMap f = 0 := rfl

@[simp]
theorem compAlternatingMap_add (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :
g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂ :=
AlternatingMap.ext fun _ => map_add g _ _

@[simp]
theorem add_compAlternatingMap (g₁ g₂ : N →ₗ[R] N₂) (f: M [⋀^ι]→ₗ[R] N) :
(g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f := rfl

@[simp]
theorem compAlternatingMap_smul [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂]
[SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R]
(g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
g.compAlternatingMap (s • f) = s • g.compAlternatingMap f :=
AlternatingMap.ext fun _ => g.map_smul_of_tower _ _

@[simp]
theorem smul_compAlternatingMap [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂]
(g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
(s • g).compAlternatingMap f = s • g.compAlternatingMap f := rfl

variable (S) in
/-- `LinearMap.compAlternatingMap` as an `S`-linear map. -/
@[simps]
def compAlternatingMapₗ [Semiring S] [Module S N] [Module S N₂]
Copy link
Member

Choose a reason for hiding this comment

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

We have several different conventions about naming of bundled versions of maps. Some day, we should decide what to do about it.

Copy link
Member Author

Choose a reason for hiding this comment

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

In this case, I copied MultilinearMap.compLinearMapₗ

[SMulCommClass R S N] [SMulCommClass R S N₂] [LinearMap.CompatibleSMul N N₂ S R]
(g : N →ₗ[R] N₂) :
(M [⋀^ι]→ₗ[R] N) →ₗ[S] (M [⋀^ι]→ₗ[R] N₂) where
toFun := g.compAlternatingMap
map_add' := g.compAlternatingMap_add
map_smul' := g.compAlternatingMap_smul

theorem smulRight_eq_comp {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁]
[AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
f.smulRight z = (LinearMap.id.smulRight z).compAlternatingMap f :=
Expand Down
47 changes: 43 additions & 4 deletions Mathlib/LinearAlgebra/Multilinear/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -787,6 +787,36 @@ theorem compMultilinearMap_apply (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R
g.compMultilinearMap f m = g (f m) :=
rfl

@[simp]
theorem compMultilinearMap_zero (g : M₂ →ₗ[R] M₃) :
g.compMultilinearMap (0 : MultilinearMap R M₁ M₂) = 0 :=
MultilinearMap.ext fun _ => map_zero g

@[simp]
theorem zero_compMultilinearMap (f: MultilinearMap R M₁ M₂) :
(0 : M₂ →ₗ[R] M₃).compMultilinearMap f = 0 := rfl

@[simp]
theorem compMultilinearMap_add (g : M₂ →ₗ[R] M₃) (f₁ f₂ : MultilinearMap R M₁ M₂) :
g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂ :=
MultilinearMap.ext fun _ => map_add g _ _

@[simp]
theorem add_compMultilinearMap (g₁ g₂ : M₂ →ₗ[R] M₃) (f: MultilinearMap R M₁ M₂) :
(g₁ + g₂).compMultilinearMap f = g₁.compMultilinearMap f + g₂.compMultilinearMap f := rfl

@[simp]
theorem compMultilinearMap_smul [Monoid S] [DistribMulAction S M₂] [DistribMulAction S M₃]
[SMulCommClass R S M₂] [SMulCommClass R S M₃] [CompatibleSMul M₂ M₃ S R]
(g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
g.compMultilinearMap (s • f) = s • g.compMultilinearMap f :=
MultilinearMap.ext fun _ => g.map_smul_of_tower _ _

@[simp]
theorem smul_compMultilinearMap [Monoid S] [DistribMulAction S M₃] [SMulCommClass R S M₃]
(g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
(s • g).compMultilinearMap f = s • g.compMultilinearMap f := rfl

/-- The multilinear version of `LinearMap.subtype_comp_codRestrict` -/
@[simp]
theorem subtype_compMultilinearMap_codRestrict (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂)
Expand Down Expand Up @@ -835,12 +865,23 @@ instance : Module S (MultilinearMap R M₁ M₂) :=
instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M₁ M₂) :=
coe_injective.noZeroSMulDivisors _ rfl coe_smul

variable [AddCommMonoid M₃] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃]

variable (S) in
/-- `LinearMap.compMultilinearMap` as an `S`-linear map. -/
@[simps]
def _root_.LinearMap.compMultilinearMapₗ [Semiring S] [Module S M₂] [Module S M₃]
[SMulCommClass R S M₂] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₂ M₃ S R]
(g : M₂ →ₗ[R] M₃) :
MultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃ where
toFun := g.compMultilinearMap
map_add' := g.compMultilinearMap_add
map_smul' := g.compMultilinearMap_smul

variable (R S M₁ M₂ M₃)

section OfSubsingleton

variable [AddCommMonoid M₃] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃]

/-- Linear equivalence between linear maps `M₂ →ₗ[R] M₃`
and one-multilinear maps `MultilinearMap R (fun _ : ι ↦ M₂) M₃`. -/
@[simps (config := { simpRhs := true })]
Expand Down Expand Up @@ -904,8 +945,6 @@ def constLinearEquivOfIsEmpty [IsEmpty ι] : M₂ ≃ₗ[S] MultilinearMap R M
left_inv _ := rfl
right_inv f := ext fun _ => MultilinearMap.congr_arg f <| Subsingleton.elim _ _

variable [AddCommMonoid M₃] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃]

/-- `MultilinearMap.domDomCongr` as a `LinearEquiv`. -/
@[simps apply symm_apply]
def domDomCongrLinearEquiv {ι₁ ι₂} (σ : ι₁ ≃ ι₂) :
Expand Down
Loading