style(linear_algebra/tensor_product): rename of -> tmul and ⊗ₛ -> ⊗ₜ; some cleanup in free_abelian_group

Author: johoelzl

group_theory/free_abelian_group.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
-Free abelian groups as abelianizatin of free groups.
+Free abelian groups as abelianization of free groups.
 -/
 
 import group_theory.free_group
@@ -29,57 +29,47 @@ abelianization.of $ free_group.of x
 instance : has_coe α (free_abelian_group α) :=
 ⟨of⟩
 
-theorem coe_def (x : α) : (x : free_abelian_group α) = of x :=
-rfl
-
-section to_comm_group
+def to_add_comm_group {β : Type v} [add_comm_group β] (f : α → β) (x : free_abelian_group α) : β :=
+@abelianization.to_comm_group _ _ (multiplicative β) _ (@free_group.to_group _ (multiplicative β) _ f) _ x
 
+namespace to_add_comm_group
 variables {β : Type v} [add_comm_group β] (f : α → β)
+open free_abelian_group
 
-def to_add_comm_group (x : free_abelian_group α) : β :=
-@abelianization.to_comm_group _ _ (multiplicative β) _ (@free_group.to_group _ (multiplicative β) _ f) _ x
-
-def to_add_comm_group.is_add_group_hom :
-  is_add_group_hom (to_add_comm_group f) :=
+protected lemma is_add_group_hom : is_add_group_hom (to_add_comm_group f) :=
 ⟨λ x y, @is_group_hom.mul _ (multiplicative β) _ _ _ (abelianization.to_comm_group.is_group_hom _) x y⟩
 
 local attribute [instance] to_add_comm_group.is_add_group_hom
 
-@[simp] lemma to_add_comm_group.add (x y : free_abelian_group α) :
+@[simp] protected lemma add (x y : free_abelian_group α) :
   to_add_comm_group f (x + y) = to_add_comm_group f x + to_add_comm_group f y :=
 is_add_group_hom.add _ _ _
 
-@[simp] lemma to_add_comm_group.neg (x : free_abelian_group α) :
-  to_add_comm_group f (-x) = -to_add_comm_group f x :=
+@[simp] protected lemma neg (x : free_abelian_group α) : to_add_comm_group f (-x) = -to_add_comm_group f x :=
 is_add_group_hom.neg _ _
 
-@[simp] lemma to_add_comm_group.sub (x y : free_abelian_group α) :
+@[simp] protected lemma sub (x y : free_abelian_group α) :
   to_add_comm_group f (x - y) = to_add_comm_group f x - to_add_comm_group f y :=
 by simp
 
-@[simp] lemma to_add_comm_group.zero :
-  to_add_comm_group f 0 = 0 :=
+@[simp] protected lemma zero : to_add_comm_group f 0 = 0 :=
 is_add_group_hom.zero _
 
-@[simp] lemma to_add_comm_group.of (x : α) :
-  to_add_comm_group f (of x) = f x :=
+@[simp] protected lemma of (x : α) : to_add_comm_group f (of x) = f x :=
 by unfold of; unfold to_add_comm_group; simp
 
-@[simp] lemma to_add_comm_group.coe (x : α) :
-  to_add_comm_group f ↑x = f x :=
+@[simp] protected lemma coe (x : α) : to_add_comm_group f ↑x = f x :=
 to_add_comm_group.of f x
 
-theorem to_add_comm_group.unique
-  (g : free_abelian_group α → β) [is_add_group_hom g]
+protected theorem unique (g : free_abelian_group α → β) [is_add_group_hom g]
   (hg : ∀ x, g (of x) = f x) {x} :
   g x = to_add_comm_group f x :=
 @abelianization.to_comm_group.unique (free_group α) _ (multiplicative β) _ _ _ g
   ⟨λ x y, @is_add_group_hom.add (additive $ abelianization (free_group α)) _ _ _ _ _ x y⟩ (λ x,
   @free_group.to_group.unique α (multiplicative β) _ _ (g ∘ abelianization.of)
     ⟨λ m n, is_add_group_hom.add g (abelianization.of m) (abelianization.of n)⟩ hg _) _
 
-theorem to_add_comm_group.ext
-  (g h : free_abelian_group α → β)
+protected theorem ext (g h : free_abelian_group α → β)
   [is_add_group_hom g] [is_add_group_hom h]
   (H : ∀ x, g (of x) = h (of x)) {x} :
   g x = h x :=
@@ -93,7 +83,7 @@ def UMP : (α → β) ≃ { f : free_abelian_group α → β // is_add_group_hom
   right_inv := λ f, subtype.eq $ funext $ λ x, eq.symm $ by letI := f.2; from
     to_add_comm_group.unique _ _ (λ _, rfl) }
 
-end to_comm_group
+end to_add_comm_group
 
 local attribute [instance] quotient_group.left_rel normal_subgroup.to_is_subgroup
 

linear_algebra/tensor_product.lean

@@ -102,41 +102,40 @@ instance quotient.mk.is_add_group_hom :
     quotient.mk :=
 quotient_add_group.is_add_group_hom _
 
-section of
+section tmul
 variables {M N}
 
-def of (m : M) (n : N) : M ⊗ N :=
-quotient_add_group.mk $ free_abelian_group.of (m, n)
+def tmul (m : M) (n : N) : M ⊗ N := quotient_add_group.mk $ free_abelian_group.of (m, n)
 
-infix ` ⊗ₛ `:100 := of
+infix ` ⊗ₜ `:100 := tmul
 
-lemma of.add_left (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₛ n = m₁ ⊗ₛ n + m₂ ⊗ₛ n :=
+lemma tmul.add_left (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₜ n = m₁ ⊗ₜ n + m₂ ⊗ₜ n :=
 eq.symm $ sub_eq_zero.1 $ eq.symm $ quotient.sound $
   group.in_closure.basic $ or.inl $ ⟨m₁, m₂, n, rfl⟩
 
-lemma of.add_right (m : M) (n₁ n₂ : N) : m ⊗ₛ (n₁ + n₂) = m ⊗ₛ n₁ + m ⊗ₛ n₂ :=
+lemma tmul.add_right (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ n₂ :=
 eq.symm $ sub_eq_zero.1 $ eq.symm $ quotient.sound $
   group.in_closure.basic $ or.inr $ or.inl $ ⟨m, n₁, n₂, rfl⟩
 
-lemma of.smul (r : R) (m : M) (n : N) : (r • m) ⊗ₛ n = m ⊗ₛ (r • n) :=
+lemma tmul.smul (r : R) (m : M) (n : N) : (r • m) ⊗ₜ n = m ⊗ₜ (r • n) :=
 sub_eq_zero.1 $ eq.symm $ quotient.sound $
   group.in_closure.basic $ or.inr $ or.inr $ ⟨r, m, n, rfl⟩
 
-end of
+end tmul
 
 local attribute [instance] free_abelian_group.to_add_comm_group.is_add_group_hom
 local attribute [instance] quotient_add_group.is_add_group_hom_quotient_lift
 
 @[reducible] def smul.aux (r : R) (x : free_abelian_group (M × N)) : M ⊗ N :=
-free_abelian_group.to_add_comm_group (λ (y : M × N), (r • y.1) ⊗ₛ (y.2)) x
+free_abelian_group.to_add_comm_group (λ (y : M × N), (r • y.1) ⊗ₜ (y.2)) x
 
 @[reducible] def smul (r : R) : M ⊗ N → M ⊗ N :=
 quotient_add_group.lift _ (smul.aux M N r)
 begin
   assume x hx,
   induction hx with _ hx _ _ ih _ _ _ _ ih1 ih2,
   { rcases hx with ⟨m₁, m₂, n, rfl⟩ | ⟨m, n₁, n₂, rfl⟩ | ⟨q, m, n, rfl⟩;
-      simp [smul.aux, -sub_eq_add_neg, sub_self, of.add_left, of.add_right, of.smul,
+      simp [smul.aux, -sub_eq_add_neg, sub_self, tmul.add_left, tmul.add_right, tmul.smul,
         smul_add, smul_smul, mul_comm] },
   { refl },
   { change smul.aux M N r (-_) = 0,
@@ -164,8 +163,8 @@ instance : module R (M ⊗ N) :=
       refine @free_abelian_group.to_add_comm_group.unique _ _ _ _ _ ⟨λ p q, _⟩ _ z,
       { simp [tensor_product.smul_add] },
       rintro ⟨m, n⟩,
-      show (r • m) ⊗ₛ n + (s • m) ⊗ₛ n = ((r + s) • m) ⊗ₛ n,
-      simp [add_smul, of.add_left]
+      show (r • m) ⊗ₜ n + (s • m) ⊗ₜ n = ((r + s) • m) ⊗ₜ n,
+      simp [add_smul, tmul.add_left]
     end,
   mul_smul := begin
       intros r s x,
@@ -176,29 +175,29 @@ instance : module R (M ⊗ N) :=
         ⟨λ p q, _⟩ _ z,
       { simp [tensor_product.smul_add] },
       rintro ⟨m, n⟩,
-      simp [smul, smul.aux, mul_smul, of]
+      simp [smul, smul.aux, mul_smul, tmul]
     end,
   one_smul := λ x, quotient.induction_on x $ λ _,
     eq.symm $ free_abelian_group.to_add_comm_group.unique _ _ $ λ ⟨p, q⟩,
     by rw [one_smul]; refl,
   .. tensor_product.add_comm_group M N }
 
-theorem bilinear : is_bilinear_map (@of R _ M N _ _) :=
-{ add_left := of.add_left,
-  add_right := of.add_right,
+theorem bilinear : is_bilinear_map (@tmul R _ M N _ _) :=
+{ add_left := tmul.add_left,
+  add_right := tmul.add_right,
   smul_left := λ r x y, rfl,
-  smul_right := assume r m n, (of.smul r m n).symm }
+  smul_right := assume r m n, (tmul.smul r m n).symm }
 
-@[simp] lemma add_of (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₛ n = m₁ ⊗ₛ n + m₂ ⊗ₛ n :=
+@[simp] lemma add_tmul (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₜ n = m₁ ⊗ₜ n + m₂ ⊗ₜ n :=
 (bilinear M N).add_left m₁ m₂ n
 
-@[simp] lemma of_add (m : M) (n₁ n₂ : N) : m ⊗ₛ (n₁ + n₂) = m ⊗ₛ n₁ + m ⊗ₛ n₂ :=
+@[simp] lemma tmul_add (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ n₂ :=
 (bilinear M N).add_right m n₁ n₂
 
-@[simp] lemma smul_of (r : R) (x : M) (y : N) : (r • x) ⊗ₛ y = r • (x ⊗ₛ y) :=
+@[simp] lemma smul_tmul (r : R) (x : M) (y : N) : (r • x) ⊗ₜ y = r • (x ⊗ₜ y) :=
 rfl
 
-@[simp] lemma of_smul (r : R) (x : M) (y : N) : x ⊗ₛ (r • y) = r • (x ⊗ₛ y) :=
+@[simp] lemma tmul_smul (r : R) (x : M) (y : N) : x ⊗ₜ (r • y) = r • (x ⊗ₜ y) :=
 (bilinear M N).smul_right r x y
 
 end module
@@ -211,11 +210,11 @@ protected theorem induction_on
   {C : M ⊗ N → Prop}
   (z : M ⊗ N)
   (C0 : C 0)
-  (C1 : ∀ x y, C $ x ⊗ₛ y)
+  (C1 : ∀ x y, C $ x ⊗ₜ y)
   (Cp : ∀ x y, C x → C y → C (x + y)) : C z :=
 quotient.induction_on z $ λ x, free_abelian_group.induction_on x
   C0 (λ ⟨p, q⟩, C1 p q)
-  (λ ⟨p, q⟩ _, show C (-(p ⊗ₛ q)), by rw ← (bilinear M N).neg_left; from C1 (-p) q)
+  (λ ⟨p, q⟩ _, show C (-(p ⊗ₜ q)), by rw ← (bilinear M N).neg_left; from C1 (-p) q)
   (λ _ _, Cp _ _)
 
 section UMP
@@ -254,7 +253,7 @@ free_abelian_group.to_add_comm_group.add _ _ _
   = r • to_module f hf x :=
 tensor_product.induction_on x smul_zero.symm
   (λ p q, by rw [← (bilinear M N).smul_left];
-    simp [to_module, of, hf.smul_left])
+    simp [to_module, tmul, hf.smul_left])
   (λ p q ih1 ih2, by simp [@smul_add _ _ _ _ r p q,
     to_module.add, ih1, ih2, smul_add])
 
@@ -263,12 +262,12 @@ def to_module.linear :
 { add := to_module.add hf,
   smul := to_module.smul hf }
 
-@[simp] lemma to_module.of (x y) :
-  to_module f hf (x ⊗ₛ y) = f x y :=
-by simp [to_module, of]
+@[simp] lemma to_module.tmul (x y) :
+  to_module f hf (x ⊗ₜ y) = f x y :=
+by simp [to_module, tmul]
 
 theorem to_module.unique {g : M ⊗ N → P}
-  (hg : is_linear_map g) (H : ∀ x y, g (x ⊗ₛ y) = f x y)
+  (hg : is_linear_map g) (H : ∀ x y, g (x ⊗ₜ y) = f x y)
   (z : M ⊗ N) : g z = to_module f hf z :=
 begin
   apply quotient_add_group.induction_on' z,
@@ -282,7 +281,7 @@ omit hf
 
 theorem to_module.ext {g h : M ⊗ N → P}
   (hg : is_linear_map g) (hh : is_linear_map h)
-  (H : ∀ x y, g (x ⊗ₛ y) = h (x ⊗ₛ y))
+  (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y))
   (z : M ⊗ N) : g z = h z :=
 begin
   apply quotient_add_group.induction_on' z,
@@ -301,10 +300,10 @@ end
 def to_module.equiv : { f : M → N → P // is_bilinear_map f }
   ≃ linear_map (M ⊗ N) P :=
 { to_fun := λ f, ⟨to_module f.1 f.2, to_module.linear f.2⟩,
-  inv_fun := λ f, ⟨λ m n, f (m ⊗ₛ n),
+  inv_fun := λ f, ⟨λ m n, f (m ⊗ₜ n),
     is_bilinear_map.comp (bilinear M N) f.2⟩,
   left_inv := λ f, subtype.eq $ funext $ λ x, funext $ λ y,
-    to_module.of f.2 _ _,
+    to_module.tmul f.2 _ _,
   right_inv := λ f, subtype.eq $ eq.symm $ funext $ λ z,
     to_module.unique _ f.2 (λ x y, rfl) _ }
 
@@ -313,11 +312,11 @@ end UMP
 protected def id : R ⊗ M ≃ₗ M :=
 { to_fun := @to_module _ _ _ _ _ _ _ _ (λ c x, c • x) $
     by refine {..}; intros; simp [smul_add, add_smul, smul_smul, mul_comm, mul_left_comm],
-  inv_fun := λ x, 1 ⊗ₛ x,
+  inv_fun := λ x, 1 ⊗ₜ x,
   left_inv := λ z, by refine to_module.ext
     (((bilinear R M).linear_right 1).comp $ to_module.linear _)
     is_linear_map.id (λ c x, _) z;
-    simp; rw [← smul_of, smul_eq_mul, mul_one],
+    simp; rw [← smul_tmul, smul_eq_mul, mul_one],
   right_inv := λ z, by simp,
   linear_fun := to_module.linear _ }
 
@@ -334,7 +333,7 @@ protected def comm : M ⊗ N ≃ₗ N ⊗ M :=
 
 protected def assoc : (M ⊗ N) ⊗ P ≃ₗ M ⊗ (N ⊗ P) :=
 { to_fun := begin
-      refine to_module (λ mn p, to_module (λ m n, m ⊗ₛ (n ⊗ₛ p)) _ mn) _;
+      refine to_module (λ mn p, to_module (λ m n, m ⊗ₜ (n ⊗ₜ p)) _ mn) _;
       constructor; intros; simp,
       { symmetry,
         refine to_module.unique _
@@ -346,7 +345,7 @@ protected def assoc : (M ⊗ N) ⊗ P ≃ₗ M ⊗ (N ⊗ P) :=
         intros; simp }
     end,
   inv_fun := begin
-      refine to_module (λ m, to_module (λ n p, (m ⊗ₛ n) ⊗ₛ p) _) _;
+      refine to_module (λ m, to_module (λ n p, (m ⊗ₜ n) ⊗ₜ p) _) _;
       constructor; intros; simp,
       { symmetry,
         refine to_module.unique _
@@ -357,14 +356,26 @@ protected def assoc : (M ⊗ N) ⊗ P ≃ₗ M ⊗ (N ⊗ P) :=
           (is_linear_map.map_smul_right (to_module.linear _)) _ _,
         intros; simp }
     end,
-  left_inv := λ z, by refine to_module.ext ((to_module.linear _).comp (to_module.linear _)) is_linear_map.id (λ mn p, _) z;
-    simp;
-    refine to_module.ext ((to_module.linear _).comp (to_module.linear _)) ((bilinear _ _).linear_left p) (λ m n, _) mn;
+  left_inv :=
+  begin
+    intro z,
+    refine to_module.ext ((to_module.linear _).comp
+      (to_module.linear _)) is_linear_map.id (λ mn p, _) z,
     simp,
-  right_inv := λ z, by refine to_module.ext ((to_module.linear _).comp (to_module.linear _)) is_linear_map.id (λ m np, _) z;
-    simp;
-    refine to_module.ext ((to_module.linear _).comp (to_module.linear _)) ((bilinear _ _).linear_right m) (λ n p, _) np;
+    refine to_module.ext ((to_module.linear _).comp
+      (to_module.linear _)) ((bilinear _ _).linear_left p) (λ m n, _) mn,
+    simp
+  end,
+  right_inv :=
+  begin
+    intro z,
+    refine to_module.ext ((to_module.linear _).comp
+      (to_module.linear _)) is_linear_map.id (λ m np, _) z,
     simp,
+    refine to_module.ext ((to_module.linear _).comp
+      (to_module.linear _)) ((bilinear _ _).linear_right m) (λ n p, _) np,
+    simp
+  end,
   linear_fun := to_module.linear _ }
 
 end tensor_product