feat(linear_algebra/bilinear_map): semilinearize bilinear maps (#10373)

This PR generalizes most of `linear_algebra/bilinear_map` to semilinear maps. Along the way, we introduce an instance for `module S (E →ₛₗ[σ] F)`, with `σ : R →+* S`. This allows us to define "semibilinear" maps of type `E →ₛₗ[σ] F →ₛₗ[ρ] G`, where `E`, `F` and `G` are modules over `R₁`, `R₂` and `R₃` respectively, and `σ : R₁ →+* R₃` and `ρ : R₂ →+* R₃`. See `mk₂'ₛₗ` to see how to construct such a map.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

src/algebra/module/linear_map.lean

@@ -57,7 +57,7 @@ open_locale big_operators
 
 universes u u' v w x y z
 variables {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
-variables {k : Type*} {S : Type*} {T : Type*}
+variables {k : Type*} {S : Type*} {S₃ : Type*} {T : Type*}
 variables {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*}
 variables {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {ι : Type*}
 
@@ -585,56 +585,62 @@ instance : add_comm_group (M →ₛₗ[σ₁₂] N₂) :=
 
 end arithmetic
 
--- TODO: generalize this section to semilinear maps where possible
 section actions
 
-variables [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
-variables [module R M] [module R M₂] [module R M₃]
+variables [semiring R] [semiring R₂] [semiring R₃]
+variables [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
+variables [module R M] [module R₂ M₂] [module R₃ M₃]
+variables {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
 
 section has_scalar
-variables [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂]
-variables [monoid T] [distrib_mul_action T M₂] [smul_comm_class R T M₂]
+variables [monoid S] [distrib_mul_action S M₂] [smul_comm_class R₂ S M₂]
+variables [monoid S₃] [distrib_mul_action S₃ M₃] [smul_comm_class R₃ S₃ M₃]
+variables [monoid T] [distrib_mul_action T M₂] [smul_comm_class R₂ T M₂]
 
-instance : has_scalar S (M →ₗ[R] M₂) :=
+instance : has_scalar S (M →ₛₗ[σ₁₂] M₂) :=
 ⟨λ a f, { to_fun := a • f,
           map_add' := λ x y, by simp only [pi.smul_apply, f.map_add, smul_add],
-          map_smul' := λ c x, by simp [pi.smul_apply, f.map_smul, smul_comm c] }⟩
+          map_smul' := λ c x, by simp [pi.smul_apply, smul_comm (σ₁₂ c)] }⟩
 
-@[simp] lemma smul_apply (a : S) (f : M →ₗ[R] M₂) (x : M) : (a • f) x = a • f x := rfl
+@[simp] lemma smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x := rfl
 
-lemma coe_smul (a : S) (f : M →ₗ[R] M₂) : ⇑(a • f) = a • f := rfl
+lemma coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ⇑(a • f) = a • f := rfl
 
-instance [smul_comm_class S T M₂] : smul_comm_class S T (M →ₗ[R] M₂) :=
+instance [smul_comm_class S T M₂] : smul_comm_class S T (M →ₛₗ[σ₁₂] M₂) :=
 ⟨λ a b f, ext $ λ x, smul_comm _ _ _⟩
 
 -- example application of this instance: if S -> T -> R are homomorphisms of commutative rings and
 -- M and M₂ are R-modules then the S-module and T-module structures on Hom_R(M,M₂) are compatible.
-instance [has_scalar S T] [is_scalar_tower S T M₂] : is_scalar_tower S T (M →ₗ[R] M₂) :=
+instance [has_scalar S T] [is_scalar_tower S T M₂] : is_scalar_tower S T (M →ₛₗ[σ₁₂] M₂) :=
 { smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ }
 
-instance : distrib_mul_action S (M →ₗ[R] M₂) :=
+instance : distrib_mul_action S (M →ₛₗ[σ₁₂] M₂) :=
 { one_smul := λ f, ext $ λ _, one_smul _ _,
   mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _,
   smul_add := λ c f g, ext $ λ x, smul_add _ _ _,
   smul_zero := λ c, ext $ λ x, smul_zero _ }
 
-theorem smul_comp (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] M₃) : (a • g).comp f = a • (g.comp f) :=
-rfl
+include σ₁₃
+theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) :
+  (a • g).comp f = a • (g.comp f) := rfl
+omit σ₁₃
 
-theorem comp_smul [distrib_mul_action S M₃] [smul_comm_class R S M₃] [compatible_smul M₃ M₂ S R]
+-- TODO: generalize this to semilinear maps
+theorem comp_smul [module R M₂] [module R M₃] [smul_comm_class R S M₂] [distrib_mul_action S M₃]
+  [smul_comm_class R S M₃] [compatible_smul M₃ M₂ S R]
   (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • (g.comp f) :=
 ext $ λ x, g.map_smul_of_tower _ _
 
 end has_scalar
 
 section module
-variables [semiring S] [module S M₂] [smul_comm_class R S M₂]
+variables [semiring S] [module S M₂] [smul_comm_class R₂ S M₂]
 
-instance : module S (M →ₗ[R] M₂) :=
+instance : module S (M →ₛₗ[σ₁₂] M₂) :=
 { add_smul := λ a b f, ext $ λ x, add_smul _ _ _,
   zero_smul := λ f, ext $ λ x, zero_smul _ _ }
 
-instance [no_zero_smul_divisors S M₂] : no_zero_smul_divisors S (M →ₗ[R] M₂) :=
+instance [no_zero_smul_divisors S M₂] : no_zero_smul_divisors S (M →ₛₗ[σ₁₂] M₂) :=
 coe_injective.no_zero_smul_divisors _ rfl coe_smul
 
 end module

src/linear_algebra/bilinear_map.lean

@@ -9,7 +9,10 @@ import linear_algebra.basic
 /-!
 # Basics on bilinear maps
 
-This file provides basics on bilinear maps.
+This file provides basics on bilinear maps. The most general form considered are maps that are
+semilinear in both arguments. They are of type `M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P`, where `M` and `N`
+are modules over `R` and `S` respectively, `P` is a module over both `R₂` and `S₂` with
+commuting actions, and `ρ₁₂ : R →+* R₂` and `σ₁₂ : S →+* S₂`.
 
 ## Main declarations
 
@@ -30,35 +33,55 @@ namespace linear_map
 
 section semiring
 
+-- the `ₗ` subscript variables are for special cases about linear (as opposed to semilinear) maps
 variables {R : Type*} [semiring R] {S : Type*} [semiring S]
+variables {R₂ : Type*} [semiring R₂] {S₂ : Type*} [semiring S₂]
 variables {M : Type*} {N : Type*} {P : Type*}
+variables {Nₗ : Type*} {Pₗ : Type*}
 variables {M' : Type*} {N' : Type*} {P' : Type*}
 
 variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
+variables [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
 variables [add_comm_group M'] [add_comm_group N'] [add_comm_group P']
-variables [module R M] [module S N] [module R P] [module S P]
-variables [module R M'] [module S N'] [module R P'] [module S P']
-variables [smul_comm_class S R P] [smul_comm_class S R P']
-include R
+variables [module R M] [module S N] [module R₂ P] [module S₂ P]
+variables [module R Pₗ] [module S Pₗ]
+variables [module R M'] [module S N'] [module R₂ P'] [module S₂ P']
+variables [smul_comm_class S₂ R₂ P] [smul_comm_class S R Pₗ] [smul_comm_class S₂ R₂ P']
+variables {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
+
+variables (ρ₁₂ σ₁₂)
+/-- Create a bilinear map from a function that is semilinear in each component.
+See `mk₂'` and `mk₂` for the linear case. -/
+def mk₂'ₛₗ (f : M → N → P)
+  (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
+  (H2 : ∀ (c:R) m n, f (c • m) n = (ρ₁₂ c) • f m n)
+  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
+  (H4 : ∀ (c:S) m n, f m (c • n) = (σ₁₂ c) • f m n) : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P :=
+{ to_fun := λ m, { to_fun := f m, map_add' := H3 m, map_smul' := λ c, H4 c m},
+  map_add' := λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
+  map_smul' := λ c m, linear_map.ext $ H2 c m }
+variables {ρ₁₂ σ₁₂}
+
+@[simp] theorem mk₂'ₛₗ_apply
+  (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
+  (mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) m n = f m n := rfl
 
 variables (R S)
 /-- Create a bilinear map from a function that is linear in each component.
 See `mk₂` for the special case where both arguments come from modules over the same ring. -/
-def mk₂' (f : M → N → P)
+def mk₂' (f : M → N → Pₗ)
   (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
   (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
   (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
-  (H4 : ∀ (c:S) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] P :=
-{ to_fun := λ m, { to_fun := f m, map_add' := H3 m, map_smul' := λ c, H4 c m},
-  map_add' := λ m₁ m₂, linear_map.ext $ H1 m₁ m₂,
-  map_smul' := λ c m, linear_map.ext $ H2 c m }
+  (H4 : ∀ (c:S) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] Pₗ :=
+mk₂'ₛₗ (ring_hom.id R) (ring_hom.id S) f H1 H2 H3 H4
 variables {R S}
 
 @[simp] theorem mk₂'_apply
-  (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
-  (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] P) m n = f m n := rfl
+  (f : M → N → Pₗ) {H1 H2 H3 H4} (m : M) (n : N) :
+  (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] Pₗ) m n = f m n := rfl
 
-theorem ext₂ {f g : M →ₗ[R] N →ₗ[S] P}
+theorem ext₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
   (H : ∀ m n, f m n = g m n) : f = g :=
 linear_map.ext (λ m, linear_map.ext $ λ n, H m n)
 
@@ -68,115 +91,139 @@ local attribute [instance] smul_comm_class.symm
 
 /-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
 `P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
-def flip (f : M →ₗ[R] N →ₗ[S] P) : N →ₗ[S] M →ₗ[R] P :=
-mk₂' S R (λ n m, f m n)
+def flip (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P :=
+mk₂'ₛₗ σ₁₂ ρ₁₂ (λ n m, f m n)
   (λ n₁ n₂ m, (f m).map_add _ _)
-  (λ c n m, (f m).map_smul _ _)
+  (λ c n m, (f m).map_smulₛₗ _ _)
   (λ n m₁ m₂, by rw f.map_add; refl)
-  (λ c n m, by rw f.map_smul; refl)
+  (λ c n m, by rw f.map_smulₛₗ; refl)
 
 end
 
-@[simp] theorem flip_apply (f : M →ₗ[R] N →ₗ[S] P) (m : M) (n : N) : flip f n m = f m n := rfl
+@[simp] theorem flip_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : flip f n m = f m n := rfl
 
 open_locale big_operators
 
 variables {R}
-theorem flip_inj {f g : M →ₗ[R] N →ₗ[S] P} (H : flip f = flip g) : f = g :=
+theorem flip_inj {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : flip f = flip g) : f = g :=
 ext₂ $ λ m n, show flip f n m = flip g n m, by rw H
 
-theorem map_zero₂ (f : M →ₗ[R] N →ₗ[S] P) (y) : f 0 y = 0 :=
+theorem map_zero₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y) : f 0 y = 0 :=
 (flip f y).map_zero
 
-theorem map_neg₂ (f : M' →ₗ[R] N →ₗ[S] P') (x y) : f (-x) y = -f x y :=
+theorem map_neg₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y) : f (-x) y = -f x y :=
 (flip f y).map_neg _
 
-theorem map_sub₂ (f : M' →ₗ[R] N →ₗ[S] P') (x y z) : f (x - y) z = f x z - f y z :=
+theorem map_sub₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y z) : f (x - y) z = f x z - f y z :=
 (flip f z).map_sub _ _
 
-theorem map_add₂ (f : M →ₗ[R] N →ₗ[S] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
+theorem map_add₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
 (flip f y).map_add _ _
 
-theorem map_smul₂ (f : M →ₗ[R] N →ₗ[S] P) (r : R) (x y) : f (r • x) y = r • f x y :=
+theorem map_smul₂ (f : M →ₗ[R] N →ₗ[S] Pₗ) (r : R) (x y) : f (r • x) y = r • f x y :=
 (flip f y).map_smul _ _
 
-theorem map_sum₂ {ι : Type*} (f : M →ₗ[R] N →ₗ[S] P) (t : finset ι) (x : ι → M) (y) :
+theorem map_smulₛₗ₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x y) : f (r • x) y = (ρ₁₂ r) • f x y :=
+(flip f y).map_smulₛₗ _ _
+
+theorem map_sum₂ {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : finset ι) (x : ι → M) (y) :
   f (∑ i in t, x i) y = ∑ i in t, f (x i) y :=
 (flip f y).map_sum
 
 end semiring
 
 section comm_semiring
 
-variables {R : Type*} [comm_semiring R]
+variables {R : Type*} [comm_semiring R] {R₂ : Type*} [comm_semiring R₂]
+variables {R₃ : Type*} [comm_semiring R₃] {R₄ : Type*} [comm_semiring R₄]
 variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
+variables {Nₗ : Type*} {Pₗ : Type*} {Qₗ : Type*}
 
 variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
-variables [module R M] [module R N] [module R P] [module R Q]
+variables [add_comm_monoid Nₗ] [add_comm_monoid Pₗ] [add_comm_monoid Qₗ]
+variables [module R M] [module R₂ N] [module R₃ P] [module R₄ Q]
+variables [module R Nₗ] [module R Pₗ] [module R Qₗ]
+variables {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
+variables {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
+variables [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₄₂ σ₂₃ σ₄₃]
 
 variables (R)
 
 /-- Create a bilinear map from a function that is linear in each component.
 
 This is a shorthand for `mk₂'` for the common case when `R = S`. -/
-def mk₂ (f : M → N → P)
+def mk₂ (f : M → Nₗ → Pₗ)
   (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
   (H2 : ∀ (c:R) m n, f (c • m) n = c • f m n)
   (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
-  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[R] P :=
+  (H4 : ∀ (c:R) m n, f m (c • n) = c • f m n) : M →ₗ[R] Nₗ →ₗ[R] Pₗ :=
 mk₂' R R f H1 H2 H3 H4
 
 @[simp] theorem mk₂_apply
-  (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
-  (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[R] P) m n = f m n := rfl
+  (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) :
+  (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] Nₗ →ₗ[R] Pₗ) m n = f m n := rfl
 
 variables (R M N P)
 /-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map `M → N → P`,
 change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
-def lflip : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] N →ₗ[R] M →ₗ[R] P :=
+def lflip : (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P :=
 { to_fun := flip, map_add' := λ _ _, rfl, map_smul' := λ _ _, rfl }
 variables {R M N P}
 
-variables (f : M →ₗ[R] N →ₗ[R] P)
+variables (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
 
 @[simp] theorem lflip_apply (m : M) (n : N) : lflip R M N P f n m = f m n := rfl
 
-variables (R P)
+variables (R Pₗ)
 /-- Composing a linear map `M → N` and a linear map `N → P` to form a linear map `M → P`. -/
-def lcomp (f : M →ₗ[R] N) : (N →ₗ[R] P) →ₗ[R] M →ₗ[R] P :=
+def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[R] M →ₗ[R] Pₗ :=
 flip $ linear_map.comp (flip id) f
 
-variables {R P}
+variables {R Pₗ}
 
-@[simp] theorem lcomp_apply (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : M) :
-  lcomp R P f g x = g (f x) := rfl
+@[simp] theorem lcomp_apply (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) :
+  lcomp R Pₗ f g x = g (f x) := rfl
 
-variables (R M N P)
+variables (P σ₂₃)
+/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
+`M → P` is itself a linear map. -/
+def lcompₛₗ (f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P :=
+flip $ linear_map.comp (flip id) f
+variables {P σ₂₃}
+
+include σ₁₃
+@[simp] theorem lcompₛₗ_apply (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
+  lcompₛₗ P σ₂₃ f g x = g (f x) := rfl
+omit σ₁₃
+
+variables (R M Nₗ Pₗ)
 /-- Composing a linear map `M → N` and a linear map `N → P` to form a linear map `M → P`. -/
-def llcomp : (N →ₗ[R] P) →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P :=
-flip { to_fun := lcomp R P,
+def llcomp : (Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ :=
+flip { to_fun := lcomp R Pₗ,
        map_add' := λ f f', ext₂ $ λ g x, g.map_add _ _,
        map_smul' := λ (c : R) f, ext₂ $ λ g x, g.map_smul _ _ }
-variables {R M N P}
+variables {R M Nₗ Pₗ}
 
 section
-@[simp] theorem llcomp_apply (f : N →ₗ[R] P) (g : M →ₗ[R] N) (x : M) :
-  llcomp R M N P f g x = f (g x) := rfl
+@[simp] theorem llcomp_apply (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) :
+  llcomp R M Nₗ Pₗ f g x = f (g x) := rfl
 end
 
 /-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
 form a bilinear map `M → Q → P`. -/
-def compl₂ (g : Q →ₗ[R] N) : M →ₗ[R] Q →ₗ[R] P := (lcomp R _ g).comp f
+def compl₂ (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₃] Q →ₛₗ[σ₄₃] P := (lcompₛₗ _ _ g).comp f
 
-@[simp] theorem compl₂_apply (g : Q →ₗ[R] N) (m : M) (q : Q) :
+include σ₄₃
+@[simp] theorem compl₂_apply (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) :
   f.compl₂ g m q = f m (g q) := rfl
+omit σ₄₃
 
 /-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
 form a bilinear map `M → N → Q`. -/
-def compr₂ (g : P →ₗ[R] Q) : M →ₗ[R] N →ₗ[R] Q :=
-linear_map.comp (llcomp R N P Q g) f
+def compr₂ (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) : M →ₗ[R] Nₗ →ₗ[R] Qₗ :=
+(llcomp R Nₗ Pₗ Qₗ g) ∘ₗ f
 
-@[simp] theorem compr₂_apply (g : P →ₗ[R] Q) (m : M) (n : N) :
+@[simp] theorem compr₂_apply (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) :
   f.compr₂ g m n = g (f m n) := rfl
 
 variables (R M)