chore(linear_algebra): switch to named constructors for linear_map (#8059)

This makes some ideas I have for future refactors easier, and generally makes things less fragile to changes such as additional fields or reordering of fields.
The extra verbosity is not really significant.

This conversion is not exhaustive, there may be anonymous constructors elsewhere that I've missed.

Author: eric-wieser

src/algebra/module/linear_map.lean

@@ -86,7 +86,7 @@ initialize_simps_projections linear_map (to_fun → apply)
 
 /-- Identity map as a `linear_map` -/
 def id : M →ₗ[R] M :=
-⟨id, λ _ _, rfl, λ _ _, rfl⟩
+{ to_fun := id, ..distrib_mul_action_hom.id R }
 
 lemma id_apply (x : M) :
   @id R M _ _ _ x = x := rfl
@@ -102,7 +102,7 @@ variables (f g : M →ₗ[R] M₂)
 
 @[simp] lemma to_fun_eq_coe : f.to_fun = ⇑f := rfl
 
-theorem is_linear : is_linear_map R f := ⟨f.2, f.3⟩
+theorem is_linear : is_linear_map R f := ⟨f.map_add', f.map_smul'⟩
 
 variables {f g}
 
@@ -226,7 +226,8 @@ variables {module_M : module R M} {module_M₂ : module R M₂}
 variables (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂)
 
 /-- Composition of two linear maps is a linear map -/
-def comp : M →ₗ[R] M₃ := ⟨f ∘ g, by simp, by simp⟩
+def comp : M →ₗ[R] M₃ :=
+{ to_fun := f ∘ g, .. f.to_distrib_mul_action_hom.comp g.to_distrib_mul_action_hom }
 
 lemma comp_apply (x : M) : f.comp g x = f (g x) := rfl
 
@@ -245,8 +246,9 @@ def inverse [module R M] [module R M₂]
   (f : M →ₗ[R] M₂) (g : M₂ → M) (h₁ : left_inverse g f) (h₂ : right_inverse g f) :
   M₂ →ₗ[R] M :=
 by dsimp [left_inverse, function.right_inverse] at h₁ h₂; exact
-  ⟨g, λ x y, by { rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂] },
-      λ a b, by { rw [← h₁ (g (a • b)), ← h₁ (a • g b)]; simp [h₂] }⟩
+  { to_fun := g,
+    map_add' := λ x y, by { rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂] },
+    map_smul' := λ a b, by { rw [← h₁ (g (a • b)), ← h₁ (a • g b)]; simp [h₂] } }
 
 end add_comm_monoid
 
@@ -292,7 +294,8 @@ variables [module R M] [module R M₂]
 include R
 
 /-- Convert an `is_linear_map` predicate to a `linear_map` -/
-def mk' (f : M → M₂) (H : is_linear_map R f) : M →ₗ M₂ := ⟨f, H.1, H.2⟩
+def mk' (f : M → M₂) (H : is_linear_map R f) : M →ₗ M₂ :=
+{ to_fun := f, map_add' := H.1, map_smul' := H.2 }
 
 @[simp] theorem mk'_apply {f : M → M₂} (H : is_linear_map R f) (x : M) :
   mk' f H x = f x := rfl
@@ -346,7 +349,7 @@ abbreviation module.End (R : Type u) (M : Type v)
 /-- Reinterpret an additive homomorphism as a `ℕ`-linear map. -/
 def add_monoid_hom.to_nat_linear_map [add_comm_monoid M] [add_comm_monoid M₂] (f : M →+ M₂) :
   M →ₗ[ℕ] M₂ :=
-⟨f, f.map_add, f.map_nat_module_smul⟩
+{ to_fun := f, map_add' := f.map_add, map_smul' := f.map_nat_module_smul }
 
 lemma add_monoid_hom.to_nat_linear_map_injective [add_comm_monoid M] [add_comm_monoid M₂] :
   function.injective (@add_monoid_hom.to_nat_linear_map M M₂ _ _) :=
@@ -355,7 +358,7 @@ by { intros f g h, ext, exact linear_map.congr_fun h x }
 /-- Reinterpret an additive homomorphism as a `ℤ`-linear map. -/
 def add_monoid_hom.to_int_linear_map [add_comm_group M] [add_comm_group M₂] (f : M →+ M₂) :
   M →ₗ[ℤ] M₂ :=
-⟨f, f.map_add, f.map_int_module_smul⟩
+{ to_fun := f, map_add' := f.map_add, map_smul' := f.map_int_module_smul }
 
 lemma add_monoid_hom.to_int_linear_map_injective [add_comm_group M] [add_comm_group M₂] :
   function.injective (@add_monoid_hom.to_int_linear_map M M₂ _ _) :=
@@ -505,8 +508,8 @@ rfl
 
 @[simp] theorem trans_apply (c : M) :
   (e₁.trans e₂) c = e₂ (e₁ c) := rfl
-@[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.6 c
-@[simp] theorem symm_apply_apply (b : M) : e.symm (e b) = b := e.5 b
+@[simp] theorem apply_symm_apply (c : M₂) : e (e.symm c) = c := e.right_inv c
+@[simp] theorem symm_apply_apply (b : M) : e.symm (e b) = b := e.left_inv b
 @[simp] lemma symm_trans_apply (c : M₃) : (e₁.trans e₂).symm c = e₁.symm (e₂.symm c) := rfl
 
 @[simp] lemma trans_refl : e.trans (refl R M₂) = e := to_equiv_injective e.to_equiv.trans_refl

src/analysis/normed_space/operator_norm.lean

@@ -84,7 +84,8 @@ def linear_map.mk_continuous_of_exists_bound (h : ∃C, ∀x, ∥f x∥ ≤ C *
 lemma continuous_of_linear_of_bound {f : E → F} (h_add : ∀ x y, f (x + y) = f x + f y)
   (h_smul : ∀ (c : 𝕜) x, f (c • x) = c • f x) {C : ℝ} (h_bound : ∀ x, ∥f x∥ ≤ C*∥x∥) :
   continuous f :=
-let φ : E →ₗ[𝕜] F := ⟨f, h_add, h_smul⟩ in φ.continuous_of_bound C h_bound
+let φ : E →ₗ[𝕜] F := { to_fun := f, map_add' := h_add, map_smul' := h_smul } in
+φ.continuous_of_bound C h_bound
 
 @[simp, norm_cast] lemma linear_map.mk_continuous_coe (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   ((f.mk_continuous C h) : E →ₗ[𝕜] F) = f := rfl

src/field_theory/finite/polynomial.lean

@@ -113,9 +113,9 @@ end
 section
 variables (K σ)
 def evalₗ : mv_polynomial σ K →ₗ[K] (σ → K) → K :=
-⟨ λp e, eval e p,
-  assume p q, (by { ext x, rw ring_hom.map_add, refl, }),
-  assume a p, funext $ assume e, by rw [smul_eq_C_mul, ring_hom.map_mul, eval_C]; refl ⟩
+{ to_fun := λ p e, eval e p,
+  map_add' := λ p q, by { ext x, rw ring_hom.map_add, refl, },
+  map_smul' := λ a p, by { ext e, rw [smul_eq_C_mul, ring_hom.map_mul, eval_C], refl } }
 end
 
 lemma evalₗ_apply (p : mv_polynomial σ K) (e : σ → K) : evalₗ K σ p e = eval e p :=

src/linear_algebra/basic.lean

@@ -184,7 +184,8 @@ lemma restrict_eq_dom_restrict_cod_restrict
   f.restrict (λ x _, hf x) = (f.cod_restrict p hf).dom_restrict p := rfl
 
 /-- The constant 0 map is linear. -/
-instance : has_zero (M →ₗ[R] M₂) := ⟨⟨λ _, 0, by simp, by simp⟩⟩
+instance : has_zero (M →ₗ[R] M₂) :=
+⟨{ to_fun := 0, map_add' := by simp, map_smul' := by simp }⟩
 
 instance : inhabited (M →ₗ[R] M₂) := ⟨0⟩
 
@@ -201,7 +202,8 @@ coe_injective.unique
 
 /-- The sum of two linear maps is linear. -/
 instance : has_add (M →ₗ[R] M₂) :=
-⟨λ f g, ⟨λ b, f b + g b, by simp [add_comm, add_left_comm], by simp [smul_add]⟩⟩
+⟨λ f g, { to_fun := f + g,
+          map_add' := by simp [add_comm, add_left_comm], map_smul' := by simp [smul_add] }⟩
 
 @[simp] lemma add_apply (x : M) : (f + g) x = f x + g x := rfl
 
@@ -366,18 +368,17 @@ variables [semiring R]
 
 /-- The negation of a linear map is linear. -/
 instance : has_neg (M →ₗ[R] M₂) :=
-⟨λ f, ⟨λ b, - f b, by simp [add_comm], by simp⟩⟩
+⟨λ f, { to_fun := -f, map_add' := by simp [add_comm], map_smul' := by simp }⟩
 
 @[simp] lemma neg_apply (x : M) : (- f) x = - f x := rfl
 
 @[simp] lemma comp_neg (g : M₂ →ₗ[R] M₃) : g.comp (- f) = - g.comp f := by { ext, simp }
 
 /-- The negation of a linear map is linear. -/
 instance : has_sub (M →ₗ[R] M₂) :=
-⟨λ f g,
-  ⟨λ b, f b - g b,
-   by { simp only [map_add, sub_eq_add_neg, neg_add], cc },
-   by { intros, simp only [map_smul, smul_sub] }⟩⟩
+⟨λ f g, { to_fun := f - g,
+          map_add' := λ x y, by simp only [pi.sub_apply, map_add, add_sub_comm],
+          map_smul' := λ r x, by simp only [pi.sub_apply, map_smul, smul_sub] }⟩
 
 @[simp] lemma sub_apply (x : M) : (f - g) x = f x - g x := rfl
 
@@ -424,8 +425,9 @@ variables {S : Type*} [semiring R] [monoid S]
   (f : M →ₗ[R] M₂)
 
 instance : has_scalar S (M →ₗ[R] M₂) :=
-⟨λ a f, ⟨λ b, a • f b, λ x y, by rw [f.map_add, smul_add],
-  λ c x, by simp only [f.map_smul, smul_comm c]⟩⟩
+⟨λ 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 only [pi.smul_apply, f.map_smul, smul_comm c] }⟩
 
 @[simp] lemma smul_apply (a : S) (x : M) : (a • f) x = a • f x := rfl
 
@@ -515,9 +517,9 @@ ext $ assume b, by rw [comp_apply, smul_apply, g.map_smul]; refl
 /-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂`
 to the space of linear maps `M₂ → M₃`. -/
 def comp_right (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃) :=
-⟨f.comp,
-λ _ _, linear_map.ext $ λ _, f.2 _ _,
-λ _ _, linear_map.ext $ λ _, f.3 _ _⟩
+{ to_fun := f.comp,
+  map_add' := λ _ _, linear_map.ext $ λ _, f.map_add _ _,
+  map_smul' := λ _ _, linear_map.ext $ λ _, f.map_smul _ _ }
 
 /-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
 See also `linear_map.applyₗ'` for a version that works with two different semirings.
@@ -1873,17 +1875,18 @@ def map_subtype.order_embedding :
 
 
 /-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
-def mkq : M →ₗ[R] p.quotient := ⟨quotient.mk, by simp, by simp⟩
+def mkq : M →ₗ[R] p.quotient :=
+{ to_fun := quotient.mk, map_add' := by simp, map_smul' := by simp }
 
 @[simp] theorem mkq_apply (x : M) : p.mkq x = quotient.mk x := rfl
 
 /-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
 vanishing on `p`, as a linear map. -/
 def liftq (f : M →ₗ[R] M₂) (h : p ≤ f.ker) : p.quotient →ₗ[R] M₂ :=
-⟨λ x, _root_.quotient.lift_on' x f $
-   λ a b (ab : a - b ∈ p), eq_of_sub_eq_zero $ by simpa using h ab,
- by rintro ⟨x⟩ ⟨y⟩; exact f.map_add x y,
- by rintro a ⟨x⟩; exact f.map_smul a x⟩
+{ to_fun := λ x, _root_.quotient.lift_on' x f $
+    λ a b (ab : a - b ∈ p), eq_of_sub_eq_zero $ by simpa using h ab,
+  map_add' := by rintro ⟨x⟩ ⟨y⟩; exact f.map_add x y,
+  map_smul' := by rintro a ⟨x⟩; exact f.map_smul a x }
 
 @[simp] theorem liftq_apply (f : M →ₗ[R] M₂) {h} (x : M) :
   p.liftq f h (quotient.mk x) = f x := rfl
@@ -2679,7 +2682,7 @@ variables {m n p : Type*}
 /-- Given an `R`-module `M` and a function `m → n` between arbitrary types,
 construct a linear map `(n → M) →ₗ[R] (m → M)` -/
 def fun_left (f : m → n) : (n → M) →ₗ[R] (m → M) :=
-mk (∘f) (λ _ _, rfl) (λ _ _, rfl)
+{ to_fun := (∘ f), map_add' := λ _ _, rfl, map_smul' := λ _ _, rfl }
 
 @[simp] theorem fun_left_apply (f : m → n) (g : n → M) (i : m) : fun_left R M f g i = g (f i) :=
 rfl

src/linear_algebra/dfinsupp.lean

@@ -44,11 +44,11 @@ include dec_ι
 
 /-- `dfinsupp.mk` as a `linear_map`. -/
 def lmk (s : finset ι) : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i :=
-⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul R x]⟩
+{ to_fun := mk s, map_add' := λ _ _, mk_add, map_smul' := λ c x, mk_smul R x }
 
 /-- `dfinsupp.single` as a `linear_map` -/
 def lsingle (i) : M i →ₗ[R] Π₀ i, M i :=
-⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩
+{ to_fun := single i, map_smul' := λ r x, single_smul _, .. dfinsupp.single_add_hom _ _ }
 
 /-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. -/
 lemma lhom_ext ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄

src/linear_algebra/finsupp.lean

@@ -91,7 +91,9 @@ variables (s : set α)
 
 /-- Interpret `finsupp.subtype_domain s` as a linear map. -/
 def lsubtype_domain : (α →₀ M) →ₗ[R] (s →₀ M) :=
-⟨subtype_domain (λx, x ∈ s), assume a b, subtype_domain_add, assume c a, ext $ assume a, rfl⟩
+{ to_fun := subtype_domain (λx, x ∈ s),
+  map_add' := λ a b, subtype_domain_add,
+  map_smul' := λ c a, ext $ λ a, rfl }
 
 lemma lsubtype_domain_apply (f : α →₀ M) :
   (lsubtype_domain s : (α →₀ M) →ₗ[R] (s →₀ M)) f = subtype_domain (λx, x ∈ s) f := rfl
@@ -349,7 +351,7 @@ variables {α' : Type*} {α'' : Type*} (M R)
 
 /-- Interpret `finsupp.map_domain` as a linear map. -/
 def lmap_domain (f : α → α') : (α →₀ M) →ₗ[R] (α' →₀ M) :=
-⟨map_domain f, assume a b, map_domain_add, map_domain_smul⟩
+{ to_fun := map_domain f, map_add' := λ a b, map_domain_add, map_smul' := map_domain_smul }
 
 @[simp] theorem lmap_domain_apply (f : α → α') (l : α →₀ M) :
   (lmap_domain M R f : (α →₀ M) →ₗ[R] (α' →₀ M)) l = map_domain f l := rfl

src/linear_algebra/linear_pmap.lean

@@ -71,24 +71,25 @@ f.to_fun.map_smul c x
 over rings, and requires a proof of `∀ c, c • x = 0 → c • y = 0`. -/
 noncomputable def mk_span_singleton' (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) :
   linear_pmap R E F :=
-begin
-  replace H : ∀ c₁ c₂ : R, c₁ • x = c₂ • x → c₁ • y = c₂ • y,
+{ domain := R ∙ x,
+  to_fun :=
+  have H : ∀ c₁ c₂ : R, c₁ • x = c₂ • x → c₁ • y = c₂ • y,
   { intros c₁ c₂ h,
     rw [← sub_eq_zero, ← sub_smul] at h ⊢,
     exact H _ h },
-  refine ⟨R ∙ x, λ z, _, _, _⟩,
-  { exact (classical.some (mem_span_singleton.1 z.prop) • y) },
-  { intros z₁ z₂,
-    rw [← add_smul],
-    apply H,
-    simp only [add_smul, sub_smul, classical.some_spec (mem_span_singleton.1 _)],
-    apply coe_add },
-  { intros c z,
-    rw [smul_smul],
-    apply H,
-    simp only [mul_smul, classical.some_spec (mem_span_singleton.1 _)],
-    apply coe_smul }
-end
+  { to_fun := λ z, (classical.some (mem_span_singleton.1 z.prop) • y),
+    map_add' := λ y z, begin
+      rw [← add_smul],
+      apply H,
+      simp only [add_smul, sub_smul, classical.some_spec (mem_span_singleton.1 _)],
+      apply coe_add
+    end,
+    map_smul' := λ c z, begin
+      rw [smul_smul],
+      apply H,
+      simp only [mul_smul, classical.some_spec (mem_span_singleton.1 _)],
+      apply coe_smul
+    end } }
 
 @[simp] lemma domain_mk_span_singleton (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) :
   (mk_span_singleton' x y H).domain = R ∙ x := rfl
@@ -213,7 +214,7 @@ begin
     simp only [← eq_sub_iff_add_eq] at hxy,
     simp only [coe_sub, coe_mk, coe_mk, hxy, ← sub_add, ← sub_sub, sub_self, zero_sub, ← H],
     apply neg_add_eq_sub },
-  refine ⟨⟨fg, _, _⟩, fg_eq⟩,
+  refine ⟨{ to_fun := fg, .. }, fg_eq⟩,
   { rintros ⟨z₁, hz₁⟩ ⟨z₂, hz₂⟩,
     rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add],
     apply fg_eq,
@@ -326,7 +327,7 @@ begin
     rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, hqc, hxq, hpq⟩,
     refine (hxq.2 _).trans (hpq.2 _).symm,
     exacts [of_le hpq.1 y, hxy, rfl] },
-  refine ⟨⟨f, _, _⟩, _⟩,
+  refine ⟨{ to_fun := f, .. }, _⟩,
   { intros x y,
     rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩,
     set x' := of_le hpx.1 ⟨x, (P x).2⟩,

src/linear_algebra/matrix/to_linear_equiv.lean

@@ -71,12 +71,17 @@ See `matrix.to_linear_equiv'` for this result on `n → R`.
 noncomputable def to_linear_equiv [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
   M ≃ₗ[R] M :=
 begin
-  refine ⟨to_lin b b A, linear_map.map_add _, linear_map.map_smul _, to_lin b b A⁻¹,
-          λ x, _, λ x, _⟩;
+  refine {
+    to_fun := to_lin b b A,
+    inv_fun := to_lin b b A⁻¹,
+    left_inv := λ x, _,
+    right_inv := λ x, _,
+    .. to_lin b b A };
   simp only [← linear_map.comp_apply, ← matrix.to_lin_mul b b b,
              matrix.nonsing_inv_mul _ hA, matrix.mul_nonsing_inv _ hA,
              to_lin_one, linear_map.id_apply]
 end
+
 lemma ker_to_lin_eq_bot [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
   (to_lin b b A).ker = ⊥ :=
 ker_eq_bot.mpr (to_linear_equiv b A hA).injective

src/linear_algebra/pi.lean

@@ -39,7 +39,9 @@ variables [semiring R] [add_comm_monoid M₂] [module R M₂] [add_comm_monoid M
 /-- `pi` construction for linear functions. From a family of linear functions it produces a linear
 function into a family of modules. -/
 def pi (f : Πi, M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (Πi, φ i) :=
-⟨λc i, f i c, λ c d, funext $ λ i, (f i).map_add _ _, λ c d, funext $ λ i, (f i).map_smul _ _⟩
+{ to_fun := λ c i, f i c,
+  map_add' := λ c d, funext $ λ i, (f i).map_add _ _,
+  map_smul' := λ c d, funext $ λ i, (f i).map_smul _ _ }
 
 @[simp] lemma pi_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
   pi f c i = f i c := rfl
@@ -61,7 +63,7 @@ rfl
 Note:  known here as `linear_map.proj`, this construction is in other categories called `eval`, for
 example `pi.eval_monoid_hom`, `pi.eval_ring_hom`. -/
 def proj (i : ι) : (Πi, φ i) →ₗ[R] φ i :=
-⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
+{ to_fun := function.eval i, map_add' := λ f g, rfl, map_smul' := λ c f, rfl }
 
 @[simp] lemma coe_proj (i : ι) : ⇑(proj i : (Πi, φ i) →ₗ[R] φ i) = function.eval i := rfl
 

src/linear_algebra/prod.lean

@@ -48,10 +48,10 @@ section
 variables (R M M₂)
 
 /-- The first projection of a product is a linear map. -/
-def fst : M × M₂ →ₗ[R] M := ⟨prod.fst, λ x y, rfl, λ x y, rfl⟩
+def fst : M × M₂ →ₗ[R] M := { to_fun := prod.fst, map_add' := λ x y, rfl, map_smul' := λ x y, rfl }
 
 /-- The second projection of a product is a linear map. -/
-def snd : M × M₂ →ₗ[R] M₂ := ⟨prod.snd, λ x y, rfl, λ x y, rfl⟩
+def snd : M × M₂ →ₗ[R] M₂ := { to_fun := prod.snd, map_add' := λ x y, rfl, map_smul' := λ x y, rfl }
 end
 
 @[simp] theorem fst_apply (x : M × M₂) : fst R M M₂ x = x.1 := rfl