From b9bf921c4c99099c3ef90554cafd128c64a26694 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 24 Jun 2021 13:55:29 +0000 Subject: [PATCH] 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. --- src/algebra/module/linear_map.lean | 23 ++++++----- src/analysis/normed_space/operator_norm.lean | 3 +- src/field_theory/finite/polynomial.lean | 6 +-- src/linear_algebra/basic.lean | 39 ++++++++++--------- src/linear_algebra/dfinsupp.lean | 4 +- src/linear_algebra/finsupp.lean | 6 ++- src/linear_algebra/linear_pmap.lean | 35 +++++++++-------- .../matrix/to_linear_equiv.lean | 9 ++++- src/linear_algebra/pi.lean | 6 ++- src/linear_algebra/prod.lean | 4 +- src/linear_algebra/tensor_product.lean | 14 +++---- src/ring_theory/hahn_series.lean | 4 +- src/topology/algebra/module.lean | 14 ++++--- src/topology/algebra/monoid.lean | 4 ++ src/topology/instances/real_vector_space.lean | 2 +- 15 files changed, 98 insertions(+), 75 deletions(-) diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean index 7b72d0fe2d1ef..955b95a150ad0 100644 --- a/src/algebra/module/linear_map.lean +++ b/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 diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean index fb1edb65aa88a..a83d745bcad7f 100644 --- a/src/analysis/normed_space/operator_norm.lean +++ b/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 diff --git a/src/field_theory/finite/polynomial.lean b/src/field_theory/finite/polynomial.lean index 8871c3f7ec2ba..e7e68569ced83 100644 --- a/src/field_theory/finite/polynomial.lean +++ b/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 := diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index b9a7377a6a3bc..781d329b88d29 100644 --- a/src/linear_algebra/basic.lean +++ b/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,7 +368,7 @@ 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 @@ -374,10 +376,9 @@ instance : has_neg (M →ₗ[R] M₂) := /-- 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 diff --git a/src/linear_algebra/dfinsupp.lean b/src/linear_algebra/dfinsupp.lean index a66a0ddcdd126..e264ea0790113 100644 --- a/src/linear_algebra/dfinsupp.lean +++ b/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⦄ diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean index fd10be6a9fe99..5964c77bcf4f7 100644 --- a/src/linear_algebra/finsupp.lean +++ b/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 diff --git a/src/linear_algebra/linear_pmap.lean b/src/linear_algebra/linear_pmap.lean index 03c39708b6c41..9362c87be5b20 100644 --- a/src/linear_algebra/linear_pmap.lean +++ b/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⟩, diff --git a/src/linear_algebra/matrix/to_linear_equiv.lean b/src/linear_algebra/matrix/to_linear_equiv.lean index b56831b9bb21c..4fcb719b2a99c 100644 --- a/src/linear_algebra/matrix/to_linear_equiv.lean +++ b/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 diff --git a/src/linear_algebra/pi.lean b/src/linear_algebra/pi.lean index b92b19c4ac249..4ab434673a37c 100644 --- a/src/linear_algebra/pi.lean +++ b/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 diff --git a/src/linear_algebra/prod.lean b/src/linear_algebra/prod.lean index 5132e5cc47712..b12f134275ae5 100644 --- a/src/linear_algebra/prod.lean +++ b/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 diff --git a/src/linear_algebra/tensor_product.lean b/src/linear_algebra/tensor_product.lean index 03818df492012..bd6ba00172b8b 100644 --- a/src/linear_algebra/tensor_product.lean +++ b/src/linear_algebra/tensor_product.lean @@ -55,9 +55,9 @@ def mk₂' (f : M → N → P) (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 := -⟨λ m, ⟨f m, H3 m, λ c, H4 c m⟩, -λ m₁ m₂, linear_map.ext $ H1 m₁ m₂, -λ c m, linear_map.ext $ H2 c m⟩ +{ 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 {R S} @[simp] theorem mk₂'_apply @@ -140,7 +140,7 @@ 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 := -⟨flip, λ _ _, rfl, λ _ _, rfl⟩ +{ to_fun := flip, map_add' := λ _ _, rfl, map_smul' := λ _ _, rfl } variables {R M N P} variables (f : M →ₗ[R] N →ₗ[R] P) @@ -160,9 +160,9 @@ variables {R P} 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) →ₗ M →ₗ P := -flip ⟨lcomp R P, - λ f f', ext₂ $ λ g x, g.map_add _ _, - λ (c : R) f, ext₂ $ λ g x, g.map_smul _ _⟩ +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} section diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean index 38c053449701d..8d79b69b24109 100644 --- a/src/ring_theory/hahn_series.lean +++ b/src/ring_theory/hahn_series.lean @@ -432,7 +432,7 @@ end /-- Extending the domain of Hahn series is a linear map. -/ @[simps] def emb_domain_linear_map (f : Γ ↪o Γ') : hahn_series Γ R →ₗ[R] hahn_series Γ' R := -⟨emb_domain f, emb_domain_add f, emb_domain_smul f⟩ +{ to_fun := emb_domain f, map_add' := emb_domain_add f, map_smul' := emb_domain_smul f } end domain @@ -1297,7 +1297,7 @@ end /-- The summation of a `summable_family` as a `linear_map`. -/ @[simps] def lsum : (summable_family Γ R α) →ₗ[hahn_series Γ R] (hahn_series Γ R) := -⟨hsum, λ _ _, hsum_add, λ _ _, hsum_smul⟩ +{ to_fun := hsum, map_add' := λ _ _, hsum_add, map_smul' := λ _ _, hsum_smul } @[simp] lemma hsum_sub {R : Type*} [ring R] {s t : summable_family Γ R α} : diff --git a/src/topology/algebra/module.lean b/src/topology/algebra/module.lean index afad80c9c3fe1..e2f499afee886 100644 --- a/src/topology/algebra/module.lean +++ b/src/topology/algebra/module.lean @@ -235,7 +235,7 @@ lemma ext_on [t2_space M₂] {s : set M} (hs : dense (submodule.span R s : set M ext $ λ x, eq_on_closure_span h (hs x) /-- The continuous map that is constantly zero. -/ -instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_const⟩⟩ +instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_zero⟩⟩ instance : inhabited (M →L[R] M₂) := ⟨0⟩ @[simp] lemma default_def : default (M →L[R] M₂) = 0 := rfl @@ -615,7 +615,7 @@ def infi_ker_proj_equiv {I J : set ι} [decidable_pred (λi, i ∈ I)] exact this end), continuous_subtype_mk _ (continuous_pi (λ i, begin - dsimp, split_ifs; [apply continuous_apply, exact continuous_const] + dsimp, split_ifs; [apply continuous_apply, exact continuous_zero] end)) ⟩ end pi @@ -749,7 +749,7 @@ variables {R S : Type*} [ring R] [ring S] [topological_space S] [module S M₃] [smul_comm_class R S M₃] [has_continuous_smul S M₃] instance : has_scalar S (M →L[R] M₃) := -⟨λ c f, ⟨c • f, continuous_const.smul f.2⟩⟩ +⟨λ c f, ⟨c • f, (continuous_const.smul f.2 : continuous (λ x, c • f x))⟩⟩ variables (c : S) (h : M₂ →L[R] M₃) (f g : M →L[R] M₂) (x y z : M) @@ -878,7 +878,9 @@ variables (A M M₂ R S) [topological_add_group M₂] /-- `continuous_linear_map.restrict_scalars` as a `linear_map`. See also `continuous_linear_map.restrict_scalarsL`. -/ def restrict_scalarsₗ : (M →L[A] M₂) →ₗ[S] (M →L[R] M₂) := -⟨restrict_scalars R, λ _ _, rfl, λ _ _, rfl⟩ +{ to_fun := restrict_scalars R, + map_add' := restrict_scalars_add, + map_smul' := restrict_scalars_smul } variables {A M M₂ R S} @@ -1047,8 +1049,8 @@ theorem surjective (e : M ≃L[R] M₂) : function.surjective e := e.to_linear_e @[simp] theorem trans_apply (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) (c : M) : (e₁.trans e₂) c = e₂ (e₁ c) := rfl -@[simp] theorem apply_symm_apply (e : M ≃L[R] M₂) (c : M₂) : e (e.symm c) = c := e.1.6 c -@[simp] theorem symm_apply_apply (e : M ≃L[R] M₂) (b : M) : e.symm (e b) = b := e.1.5 b +@[simp] theorem apply_symm_apply (e : M ≃L[R] M₂) (c : M₂) : e (e.symm c) = c := e.1.right_inv c +@[simp] theorem symm_apply_apply (e : M ≃L[R] M₂) (b : M) : e.symm (e b) = b := e.1.left_inv b @[simp] theorem symm_trans_apply (e₁ : M₂ ≃L[R] M) (e₂ : M₃ ≃L[R] M₂) (c : M) : (e₂.trans e₁).symm c = e₂.symm (e₁.symm c) := rfl diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean index 33bea77518794..cc0e1c518b7e3 100644 --- a/src/topology/algebra/monoid.lean +++ b/src/topology/algebra/monoid.lean @@ -22,6 +22,10 @@ open_locale classical topological_space big_operators variables {ι α X M N : Type*} [topological_space X] +@[to_additive] +lemma continuous_one [topological_space M] [has_one M] : continuous (1 : X → M) := +@continuous_const _ _ _ _ 1 + /-- Basic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the instances `add_monoid M` and `has_continuous_add M`. -/ diff --git a/src/topology/instances/real_vector_space.lean b/src/topology/instances/real_vector_space.lean index 6ce4f34a59760..b5eb902259652 100644 --- a/src/topology/instances/real_vector_space.lean +++ b/src/topology/instances/real_vector_space.lean @@ -31,7 +31,7 @@ dense_embedding_of_rat.dense.equalizer /-- Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map. -/ def to_real_linear_map (f : E →+ F) (hf : continuous f) : E →L[ℝ] F := -⟨⟨f, f.map_add, f.map_real_smul hf⟩, hf⟩ +⟨{ to_fun := f, map_add' := f.map_add, map_smul' := f.map_real_smul hf }, hf⟩ @[simp] lemma coe_to_real_linear_map (f : E →+ F) (hf : continuous f) : ⇑(f.to_real_linear_map hf) = f := rfl