golf

src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean

@@ -6,13 +6,14 @@ Note that `quadratic_form.isometry` is already taken for isometric equivalences.
 -/
 set_option old_structure_cmd true
 
-variables {ι R M M₁ M₂ M₃ : Type*}
+variables {ι R M M₁ M₂ M₃ M₄ : Type*}
 
 namespace quadratic_form
 
 variables [semiring R]
-variables [add_comm_monoid M] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃]
-variables [module R M] [module R M₁] [module R M₂] [module R M₃]
+variables [add_comm_monoid M]
+variables [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄]
+variables [module R M] [module R M₁] [module R M₂] [module R M₃] [module R M₄]
 
 /-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
 is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms. -/
@@ -22,7 +23,8 @@ is a linear equivalence between `M₁` and `M₂` that commutes with the quadrat
 
 namespace isometric_map
 
-variables {Q₁ : quadratic_form R M₁} {Q₂ : quadratic_form R M₂} {Q₃ : quadratic_form R M₃}
+variables {Q₁ : quadratic_form R M₁} {Q₂ : quadratic_form R M₂}
+variables {Q₃ : quadratic_form R M₃} {Q₄ : quadratic_form R M₄}
 
 instance : semilinear_map_class (Q₁.isometric_map Q₂) (ring_hom.id R) M₁ M₂ :=
 { coe := λ f, f.to_linear_map,
@@ -61,6 +63,11 @@ def comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) : Q₁.isom
 @[simp] lemma to_linear_map_comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) :
   (g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl
 
+@[simp] lemma id_comp (f : Q₁.isometric_map Q₂) : (id Q₂).comp f = f := ext $ λ _, rfl
+@[simp] lemma comp_id (f : Q₁.isometric_map Q₂) : f.comp (id Q₁) = f := ext $ λ _, rfl
+lemma comp_assoc (h : Q₃.isometric_map Q₄) (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) :
+  (h.comp g).comp f = h.comp (g.comp f) := ext $ λ _, rfl
+
 /-- Isometries are isometric maps -/
 @[simps]
 def _root_.quadratic_form.isometry.to_isometric_map (g : Q₁.isometry Q₂) :

src/geometric_algebra/from_mathlib/category_theory.lean

@@ -41,12 +41,15 @@ instance (V : QuadraticModule.{v} R) : module R V := V.is_module
 def form (V : QuadraticModule.{v} R) : quadratic_form R V := V.form'
 
 instance category : category (QuadraticModule.{v} R) :=
-{ hom   := λ M N, M.form.isometric_map N.form,
-  id    := λ M, isometric_map.id M.form,
-  comp  := λ A B C f g, g.comp f,
-  id_comp' := λ X Y f, isometric_map.to_linear_map_injective $ linear_map.id_comp _,
-  comp_id' := λ X Y f, isometric_map.to_linear_map_injective $ linear_map.comp_id _,
-  assoc' := λ W X Y Z f g h, isometric_map.to_linear_map_injective $ linear_map.comp_assoc _ _ _ }
+{ hom      := λ M N, M.form.isometric_map N.form,
+  id       := λ M, isometric_map.id M.form,
+  comp     := λ A B C f g, g.comp f,
+  id_comp' := λ X Y, isometric_map.id_comp,
+  comp_id' := λ X Y, isometric_map.comp_id,
+  assoc'   := λ W X Y Z f g h, isometric_map.comp_assoc h g f }
+
+lemma comp_def {M N U : QuadraticModule.{v} R} (f : M ⟶ N) (g : N ⟶ U) :
+  f ≫ g = g.comp f := rfl
 
 instance concrete_category : concrete_category.{v} (QuadraticModule.{v} R) :=
 { forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
@@ -55,7 +58,7 @@ instance concrete_category : concrete_category.{v} (QuadraticModule.{v} R) :=
 instance has_forget_to_Module : has_forget₂ (QuadraticModule R) (Module R) :=
 { forget₂ :=
   { obj := λ M, Module.of R M,
-    map := λ M₁ M₂ f, isometric_map.to_linear_map f } }
+    map := λ M₁ M₂, isometric_map.to_linear_map } }
 
 instance (M N : QuadraticModule R) : linear_map_class (M ⟶ N) R M N :=
 { coe := λ f, f,
@@ -69,17 +72,8 @@ def CliffordAlgebra : QuadraticModule.{u} R ⥤ Algebra.{u} R :=
 { obj := λ M,
   { carrier := clifford_algebra M.form },
   map := λ M N f, clifford_algebra.map _ _ f.to_linear_map f.map_app,
-  map_id' := by { intros X, ext1, simp only [clifford_algebra.map_comp_ι], refl },
-  map_comp' := λ M N P f g, begin
-    ext1,
-    simp only [clifford_algebra.map_comp_ι],
-    ext1,
-    simp_rw [linear_map.comp_apply, alg_hom.to_linear_map_apply, category_theory.comp_apply,
-      clifford_algebra.map_apply_ι, isometric_map.coe_to_linear_map],
-    simp only [free_algebra.lift_ι_apply, category_theory.coe_comp, function.comp_app,
-      types_comp_apply]
-  end }
-.
+  map_id' := λ X, clifford_algebra.map_id _,
+  map_comp' := λ M N P f g, (clifford_algebra.map_comp_map _ _ _ _ _ _ _).symm }
 
 variables {M : Type w} [add_comm_group M] [module R M] (Q : quadratic_form R M)