add some basic category theory

src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean

@@ -0,0 +1,65 @@
+import linear_algebra.quadratic_form.isometry
+
+/-! # Isometric linear maps
+
+Note that `quadratic_form.isometry` is already taken for isometric equivalences.
+-/
+set_option old_structure_cmd true
+
+variables {ι R 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₃]
+
+/-- 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. -/
+@[nolint has_nonempty_instance] structure isometric_map
+  (Q₁ : quadratic_form R M₁) (Q₂ : quadratic_form R M₂) extends M₁ →ₗ[R] M₂ :=
+(map_app' : ∀ m, Q₂ (to_fun m) = Q₁ m)
+
+namespace isometric_map
+
+variables {Q₁ : quadratic_form R M₁} {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,
+  coe_injective' := λ f g h, by cases f; cases g; congr',
+  map_add := λ f, f.to_linear_map.map_add,
+  map_smulₛₗ := λ f, f.to_linear_map.map_smul }
+
+lemma to_linear_map_injective :
+  function.injective (isometric_map.to_linear_map : (Q₁.isometric_map Q₂) → (M₁ →ₗ[R] M₂)) :=
+λ f g h, fun_like.coe_injective (congr_arg fun_like.coe h : _)
+
+@[ext] lemma ext ⦃f g : Q₁.isometric_map Q₂⦄ (h : ∀ x, f x = g x) : f = g := fun_like.ext _ _ h
+
+/-- See Note [custom simps projection]. -/
+protected def simps.apply (f : Q₁.isometric_map Q₂) : M₁ → M₂ := f
+
+initialize_simps_projections isometric_map (to_fun → apply)
+
+@[simp] lemma map_app (f : Q₁.isometric_map Q₂) (m : M₁) : Q₂ (f m) = Q₁ m := f.map_app' m
+
+@[simp] lemma coe_to_linear_map (f : Q₁.isometric_map Q₂) : ⇑f.to_linear_map = f := rfl
+
+/-- The identity isometry from a quadratic form to itself. -/
+@[simps]
+def id (Q : quadratic_form R M) : Q.isometric_map Q :=
+{ map_app' := λ m, rfl,
+  .. linear_map.id  }
+
+/-- The composition of two isometries between quadratic forms. -/
+@[simps]
+def comp (g : Q₂.isometric_map Q₃) (f : Q₁.isometric_map Q₂) : Q₁.isometric_map Q₃ :=
+{ to_fun := λ x, g (f x),
+  map_app' := by { intro m, rw [← f.map_app, ← g.map_app] },
+  .. (g.to_linear_map : M₂ →ₗ[R] M₃).comp (f.to_linear_map : M₁ →ₗ[R] M₂) }
+
+@[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
+
+end isometric_map
+end quadratic_form

src/geometric_algebra/from_mathlib/category_theory.lean

@@ -0,0 +1,71 @@
+import algebra.category.Algebra.basic
+import linear_algebra.clifford_algebra.basic
+import geometric_algebra.from_mathlib.basic
+import for_mathlib.linear_algebra.quadratic_form.isometric_map
+
+open category_theory
+
+/-! # Category-theoretic interpretations of `clifford_algebra` -/
+
+universes v u
+
+set_option old_structure_cmd true
+
+variables (R : Type u) [comm_ring R]
+
+structure QuadraticModule extends Module.{v} R :=
+(form' : quadratic_form R carrier)
+
+
+variables {R}
+
+namespace QuadraticModule
+open quadratic_form
+
+instance : has_coe_to_sort (QuadraticModule.{v} R) (Type v) := ⟨QuadraticModule.carrier⟩
+
+
+instance (V : QuadraticModule.{v} R) : add_comm_group V := V.is_add_comm_group
+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 _ _ _ }
+
+instance concrete_category : concrete_category.{v} (QuadraticModule.{v} R) :=
+{ forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
+  forget_faithful := { } }
+
+instance has_forget_to_AddCommGroup : has_forget₂ (QuadraticModule R) (Module R) :=
+{ forget₂ :=
+  { obj := λ M, Module.of R M,
+    map := λ M₁ M₂ f, isometric_map.to_linear_map f } }
+
+instance (M N : QuadraticModule R) : linear_map_class (M ⟶ N) R M N :=
+{ coe := λ f, f,
+  .. isometric_map.semilinear_map_class }
+
+/-- The "clifford algebra" functor, sending a quadratic R-module V to the clifford algebra on `V`. -/
+@[simps]
+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 }
+
+end QuadraticModule