From 3b1e3bcd87004a6afe8ec9f28db4b3c588ab972f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 22 Jul 2023 11:16:42 +0000 Subject: [PATCH 1/8] add notation --- .../quadratic_form/isometric_map.lean | 34 ++++++++++--------- .../from_mathlib/category_theory.lean | 2 +- 2 files changed, 19 insertions(+), 17 deletions(-) diff --git a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean index eae9c6f69..816036721 100644 --- a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean +++ b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean @@ -23,70 +23,72 @@ is a linear equivalence between `M₁` and `M₂` that commutes with the quadrat namespace isometric_map +notation Q₁ ` →qᵢ `:25 Q₂:0 := isometric_map Q₁ Q₂ + 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₂ := +instance : semilinear_map_class (Q₁ →qᵢ 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₂)) := + function.injective (isometric_map.to_linear_map : (Q₁ →qᵢ 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 +@[ext] lemma ext ⦃f g : Q₁ →qᵢ 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 +protected def simps.apply (f : Q₁ →qᵢ 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 map_app (f : Q₁ →qᵢ 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 +@[simp] lemma coe_to_linear_map (f : Q₁ →qᵢ 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 := +def id (Q : quadratic_form R M) : Q →qᵢ 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₃ := +def comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : Q₁ →qᵢ 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₂) : +@[simp] lemma to_linear_map_comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ 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₂) : +@[simp] lemma id_comp (f : Q₁ →qᵢ Q₂) : (id Q₂).comp f = f := ext $ λ _, rfl +@[simp] lemma comp_id (f : Q₁ →qᵢ Q₂) : f.comp (id Q₁) = f := ext $ λ _, rfl +lemma comp_assoc (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ 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₂) : - Q₁.isometric_map Q₂ := { ..g } + Q₁ →qᵢ Q₂ := { ..g } /-- There is a zero map from any module with the zero form. -/ -instance : has_zero ((0 : quadratic_form R M₁).isometric_map Q₂) := +instance : has_zero ((0 : quadratic_form R M₁) →qᵢ Q₂) := { zero := { map_app' := λ m, map_zero _, ..(0 : M₁ →ₗ[R] M₂) } } /-- There is a zero map from the trivial module. -/ -instance [subsingleton M₁] : has_zero (Q₁.isometric_map Q₂) := +instance [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) := { zero := { map_app' := λ m, subsingleton.elim 0 m ▸ (map_zero _).trans (map_zero _).symm, ..(0 : M₁ →ₗ[R] M₂) } } /-- Maps into the zero module are trivial -/ -instance [subsingleton M₂] : subsingleton (Q₁.isometric_map Q₂) := +instance [subsingleton M₂] : subsingleton (Q₁ →qᵢ Q₂) := ⟨λ f g, ext $ λ _, subsingleton.elim _ _⟩ end isometric_map diff --git a/src/geometric_algebra/from_mathlib/category_theory.lean b/src/geometric_algebra/from_mathlib/category_theory.lean index 52daf1ecd..447cfd87f 100644 --- a/src/geometric_algebra/from_mathlib/category_theory.lean +++ b/src/geometric_algebra/from_mathlib/category_theory.lean @@ -41,7 +41,7 @@ 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, +{ hom := λ M N, M.form →qᵢ 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, From f92f012da17f0ad1e6f2ec2ed5c212609ac33d69 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 22 Jul 2023 11:17:28 +0000 Subject: [PATCH 2/8] fix crash --- .../linear_algebra/quadratic_form/isometric_map.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean index 816036721..4595457ef 100644 --- a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean +++ b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean @@ -82,7 +82,7 @@ instance : has_zero ((0 : quadratic_form R M₁) →qᵢ Q₂) := ..(0 : M₁ →ₗ[R] M₂) } } /-- There is a zero map from the trivial module. -/ -instance [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) := +instance has_zero_of_subsingleton [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) := { zero := { map_app' := λ m, subsingleton.elim 0 m ▸ (map_zero _).trans (map_zero _).symm, ..(0 : M₁ →ₗ[R] M₂) } } From a5c2656a7e926c9dae644c1234150b2d0ca46972 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 22 Jul 2023 11:32:45 +0000 Subject: [PATCH 3/8] semilinearity --- .../quadratic_form/isometric_map.lean | 105 +++++++++++------- 1 file changed, 67 insertions(+), 38 deletions(-) diff --git a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean index 4595457ef..073a1fe98 100644 --- a/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean +++ b/src/for_mathlib/linear_algebra/quadratic_form/isometric_map.lean @@ -1,96 +1,125 @@ import linear_algebra.quadratic_form.isometry -/-! # Isometric linear maps +/-! # Isometric (semi)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₃ M₄ : Type*} +variables {ι R R₁ R₂ R₃ R₄ M₁ M₂ M₃ M₄ : Type*} namespace quadratic_form -variables [semiring R] -variables [add_comm_monoid M] +section semilinear + +variables [semiring R₁] [semiring R₂] [semiring R₃] [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₃] [module R 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) +@[nolint has_nonempty_instance] structure isometric_map (σ : R₁ →+* R₂) + (Q₁ : quadratic_form R₁ M₁) (Q₂ : quadratic_form R₂ M₂) extends M₁ →ₛₗ[σ] M₂ := +(map_app' : ∀ m, Q₂ (to_fun m) = σ (Q₁ m)) + + +notation Q₁ ` →qₛₗ[`:25 σ:25 `] `:0 Q₂:0 := isometric_map σ Q₁ Q₂ +notation Q₁ ` →qᵢ `:25 Q₂:0 := isometric_map (ring_hom.id _) Q₁ Q₂ namespace isometric_map -notation Q₁ ` →qᵢ `:25 Q₂:0 := isometric_map Q₁ Q₂ -variables {Q₁ : quadratic_form R M₁} {Q₂ : quadratic_form R M₂} -variables {Q₃ : quadratic_form R M₃} {Q₄ : quadratic_form R M₄} +variables {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₃₄ : R₃ →+* R₄} +variables {σ₁₃ : R₁ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} +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₁ →qᵢ Q₂) (ring_hom.id R) M₁ M₂ := +instance : semilinear_map_class (Q₁ →qₛₗ[σ₁₂] Q₂) σ₁₂ 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 } + map_smulₛₗ := λ f, f.to_linear_map.map_smulₛₗ } lemma to_linear_map_injective : - function.injective (isometric_map.to_linear_map : (Q₁ →qᵢ Q₂) → (M₁ →ₗ[R] M₂)) := + function.injective (isometric_map.to_linear_map : (Q₁ →qₛₗ[σ₁₂] Q₂) → (M₁ →ₛₗ[σ₁₂] M₂)) := λ f g h, fun_like.coe_injective (congr_arg fun_like.coe h : _) -@[ext] lemma ext ⦃f g : Q₁ →qᵢ Q₂⦄ (h : ∀ x, f x = g x) : f = g := fun_like.ext _ _ h +@[ext] lemma ext ⦃f g : Q₁ →qₛₗ[σ₁₂] Q₂⦄ (h : ∀ x, f x = g x) : f = g := fun_like.ext _ _ h /-- See Note [custom simps projection]. -/ -protected def simps.apply (f : Q₁ →qᵢ Q₂) : M₁ → M₂ := f +protected def simps.apply (f : Q₁ →qₛₗ[σ₁₂] Q₂) : M₁ → M₂ := f initialize_simps_projections isometric_map (to_fun → apply) -@[simp] lemma map_app (f : Q₁ →qᵢ Q₂) (m : M₁) : Q₂ (f m) = Q₁ m := f.map_app' m +@[simp] lemma map_appₛₗ (f : Q₁ →qₛₗ[σ₁₂] Q₂) (m : M₁) : Q₂ (f m) = σ₁₂ (Q₁ m) := f.map_app' m -@[simp] lemma coe_to_linear_map (f : Q₁ →qᵢ Q₂) : ⇑f.to_linear_map = f := rfl +@[simp] lemma coe_to_linear_map (f : Q₁ →qₛₗ[σ₁₂] 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 →qᵢ Q := +def id (Q : quadratic_form R₁ M₁) : Q →qᵢ Q := { map_app' := λ m, rfl, .. linear_map.id } /-- The composition of two isometries between quadratic forms. -/ @[simps] -def comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : Q₁ →qᵢ Q₃ := +def comp [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : Q₂ →qₛₗ[σ₂₃] Q₃) (f : Q₁ →qₛₗ[σ₁₂] Q₂) : Q₁ →qₛₗ[σ₁₃] 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₂) } + map_app' := λ m, + by rw [←@ring_hom_comp_triple.comp_apply _ _ _ _ _ _ σ₁₂ σ₂₃ σ₁₃, ← f.map_appₛₗ, ← g.map_appₛₗ], + .. (g.to_linear_map : M₂ →ₛₗ[σ₂₃] M₃).comp (f.to_linear_map : M₁ →ₛₗ[σ₁₂] M₂) } -@[simp] lemma to_linear_map_comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : +@[simp] lemma to_linear_map_comp [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] (g : Q₂ →qₛₗ[σ₂₃] Q₃) (f : Q₁ →qₛₗ[σ₁₂] Q₂) : (g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl -@[simp] lemma id_comp (f : Q₁ →qᵢ Q₂) : (id Q₂).comp f = f := ext $ λ _, rfl -@[simp] lemma comp_id (f : Q₁ →qᵢ Q₂) : f.comp (id Q₁) = f := ext $ λ _, rfl -lemma comp_assoc (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : +@[simp] lemma id_comp (f : Q₁ →qₛₗ[σ₁₂] Q₂) : (id Q₂).comp f = f := ext $ λ _, rfl +@[simp] lemma comp_id (f : Q₁ →qₛₗ[σ₁₂] Q₂) : f.comp (id Q₁) = f := ext $ λ _, rfl +lemma comp_assoc + [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] + [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] + (h : Q₃ →qₛₗ[σ₃₄] Q₄) (g : Q₂ →qₛₗ[σ₂₃] Q₃) (f : Q₁ →qₛₗ[σ₁₂] 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₂) : - Q₁ →qᵢ Q₂ := { ..g } - /-- There is a zero map from any module with the zero form. -/ -instance : has_zero ((0 : quadratic_form R M₁) →qᵢ Q₂) := +instance : has_zero ((0 : quadratic_form R₁ M₁) →qₛₗ[σ₁₂] Q₂) := { zero := - { map_app' := λ m, map_zero _, - ..(0 : M₁ →ₗ[R] M₂) } } + { map_app' := λ m, (map_zero _).trans (_root_.map_zero _).symm, + ..(0 : M₁ →ₛₗ[σ₁₂] M₂) } } /-- There is a zero map from the trivial module. -/ -instance has_zero_of_subsingleton [subsingleton M₁] : has_zero (Q₁ →qᵢ Q₂) := +instance has_zero_of_subsingleton [subsingleton M₁] : has_zero (Q₁ →qₛₗ[σ₁₂] Q₂) := { zero := - { map_app' := λ m, subsingleton.elim 0 m ▸ (map_zero _).trans (map_zero _).symm, - ..(0 : M₁ →ₗ[R] M₂) } } + { map_app' := λ m, subsingleton.elim 0 m ▸ (map_zero _).trans $ + (_root_.map_zero σ₁₂).symm.trans $ σ₁₂.congr_arg (map_zero _).symm, + ..(0 : M₁ →ₛₗ[σ₁₂] M₂) } } /-- Maps into the zero module are trivial -/ -instance [subsingleton M₂] : subsingleton (Q₁ →qᵢ Q₂) := +instance [subsingleton M₂] : subsingleton (Q₁ →qₛₗ[σ₁₂] Q₂) := ⟨λ f g, ext $ λ _, subsingleton.elim _ _⟩ end isometric_map +end semilinear + +section linear + +namespace isometric_map + +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 {Q₁ : quadratic_form R M₁} {Q₂ : quadratic_form R M₂} + +/-- Isometries are isometric maps -/ +@[simps] +def _root_.quadratic_form.isometry.to_isometric_map (g : Q₁.isometry Q₂) : + Q₁ →qᵢ Q₂ := { ..g } + +@[simp] lemma map_app (f : Q₁ →qᵢ Q₂) (m : M₁) : Q₂ (f m) = Q₁ m := f.map_app' m + +end isometric_map + +end linear + end quadratic_form From 57042230559b27c3adb6f7ce298bc50c6419c78f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 27 Jul 2023 12:23:29 +0000 Subject: [PATCH 4/8] fix build error --- .../linear_algebra/quadratic_form/prod.lean | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/for_mathlib/linear_algebra/quadratic_form/prod.lean b/src/for_mathlib/linear_algebra/quadratic_form/prod.lean index 9c9a56f9f..2a00e40e8 100644 --- a/src/for_mathlib/linear_algebra/quadratic_form/prod.lean +++ b/src/for_mathlib/linear_algebra/quadratic_form/prod.lean @@ -22,12 +22,12 @@ variables [fintype ι] (QM₁ : quadratic_form R M₁) (QM₂ : quadratic_form R variables (QN₁ : quadratic_form R N₁) (QN₂ : quadratic_form R N₂) /-- `linear_map.inl` as an `isometric_map`. -/ -@[simps] def inl [decidable_eq ι] (i : ι) : QM₁.isometric_map (QM₁.prod QM₂) := +@[simps] def inl [decidable_eq ι] (i : ι) : QM₁ →qᵢ QM₁.prod QM₂ := { map_app' := λ x, by simp, .. linear_map.inl R M₁ M₂ } /-- `linear_map.inl` as an `isometric_map`. -/ -@[simps] def inr [decidable_eq ι] (i : ι) : QM₂.isometric_map (QM₁.prod QM₂) := +@[simps] def inr [decidable_eq ι] (i : ι) : QM₂ →qᵢ QM₁.prod QM₂ := { map_app' := λ x, by simp, .. linear_map.inr R M₁ M₂ } @@ -36,16 +36,16 @@ variables {QM₁ QM₂ QN₁ QN₂} /-- `pi.prod` of two isometric maps. -/ @[simps] def prod {fQM₁ gQM₁ : quadratic_form R M₁} - (f : fQM₁.isometric_map QN₁) (g : gQM₁.isometric_map QN₂) : - (fQM₁ + gQM₁).isometric_map (QN₁.prod QN₂) := + (f : fQM₁ →qᵢ QN₁) (g : gQM₁ →qᵢ QN₂) : + (fQM₁ + gQM₁) →qᵢ QN₁.prod QN₂ := { to_fun := pi.prod f g, map_app' := λ x, congr_arg2 (+) (f.map_app _) (g.map_app _), .. linear_map.prod f.to_linear_map g.to_linear_map } /-- `prod.map` of two isometric maps. -/ @[simps] -def prod_map (f : QM₁.isometric_map QN₁) (g : QM₂.isometric_map QN₂) : - (QM₁.prod QM₂).isometric_map (QN₁.prod QN₂) := +def prod_map (f : QM₁ →qᵢ QN₁) (g : QM₂ →qᵢ QN₂) : + QM₁.prod QM₂ →qᵢ QN₁.prod QN₂ := { map_app' := λ x, congr_arg2 (+) (f.map_app _) (g.map_app _), .. linear_map.prod_map f.to_linear_map g.to_linear_map } @@ -56,9 +56,10 @@ variables [fintype ι] (QM₁ : ι → quadratic_form R M₁) (QMᵢ : Π i, qua /-- `linear_map.single` as an `isometric_map`. -/ @[simps] -def single [decidable_eq ι] (i : ι) : (QMᵢ i).isometric_map (quadratic_form.pi QMᵢ) := +def single [decidable_eq ι] (i : ι) : QMᵢ i →qᵢ quadratic_form.pi QMᵢ := { to_fun := pi.single i, map_app' := λ x, (pi_apply QMᵢ _).trans $ begin + rw ring_hom.id_apply, refine (fintype.sum_eq_single i $ λ j hij, _).trans _, { rw [pi.single_eq_of_ne hij, map_zero] }, { rw [pi.single_eq_same] } @@ -66,10 +67,11 @@ def single [decidable_eq ι] (i : ι) : (QMᵢ i).isometric_map (quadratic_form. .. (linear_map.single i : Mᵢ i →ₗ[R] (Π i, Mᵢ i))} /-- `linear_map.pi` for `isometric_map`. -/ -def pi (f : Π i, (QM₁ i).isometric_map (QMᵢ i)) : - (∑ i, QM₁ i).isometric_map (quadratic_form.pi QMᵢ) := +def pi (f : Π i, QM₁ i →qᵢ QMᵢ i) : + (∑ i, QM₁ i) →qᵢ quadratic_form.pi QMᵢ := { to_fun := λ c i, f i c, - map_app' := λ c, (pi_apply QMᵢ _).trans $ by simp_rw [λ i, (f i).map_app, sum_apply], + map_app' := λ c, (pi_apply QMᵢ _).trans $ + by simp_rw [λ i, (f i).map_app, sum_apply, ring_hom.id_apply], .. linear_map.pi (λ i, (f i).to_linear_map) } end pi From 7657a75d5b33879ee9c768694b65b9a78e450e40 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 27 Jul 2023 13:26:21 +0000 Subject: [PATCH 5/8] add terminal object --- src/geometric_algebra/from_mathlib/basic.lean | 9 +++++ .../from_mathlib/category_theory.lean | 40 ++++++++++++++++--- 2 files changed, 43 insertions(+), 6 deletions(-) diff --git a/src/geometric_algebra/from_mathlib/basic.lean b/src/geometric_algebra/from_mathlib/basic.lean index 537e61c25..1fe51804f 100644 --- a/src/geometric_algebra/from_mathlib/basic.lean +++ b/src/geometric_algebra/from_mathlib/basic.lean @@ -19,6 +19,15 @@ example : ring (clifford_algebra Q) := infer_instance variables (Q) abbreviation clifford_hom (A : Type*) [semiring A] [algebra R A] := { f : M →ₗ[R] A // ∀ m, f m * f m = ↑ₐ(Q m) } + +instance {A : Type*} [ring A] [algebra R A] : + has_zero (clifford_hom (0 : quadratic_form R M) A) := +{ zero := ⟨0, λ m, by simp⟩ } + +instance has_zero_of_subsingleton {A : Type*} [ring A] [algebra R A] [subsingleton A] : + has_zero (clifford_hom Q A) := +{ zero := ⟨0, λ m, subsingleton.elim _ _⟩ } + variables {Q} /-- TODO: work out what the necessary conditions are here, then make this an instance -/ diff --git a/src/geometric_algebra/from_mathlib/category_theory.lean b/src/geometric_algebra/from_mathlib/category_theory.lean index 447cfd87f..ecbc9c964 100644 --- a/src/geometric_algebra/from_mathlib/category_theory.lean +++ b/src/geometric_algebra/from_mathlib/category_theory.lean @@ -9,7 +9,7 @@ import for_mathlib.linear_algebra.quadratic_form.isometric_map * `QuadraticModule R`: the category of quadratic modules * `CliffordAlgebra`: the functor from quadratic modules to algebras -* `clifford_algebra.is_initial`: the clifford algebra is initial in the category of pairs +* `Cliff.is_initial_clifford_algebra`: the clifford algebra is initial in the category of pairs `(A, clifford_hom Q A)`. -/ @@ -18,6 +18,16 @@ open category_theory open quadratic_form open clifford_algebra +instance _root_.alg_hom.has_zero_of_subsingleton (R A B : Type*) + [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [subsingleton A] : + has_zero (B →ₐ[R] A) := +{ zero := + { to_fun := 0, + map_one' := subsingleton.elim _ _, + map_mul' := λ _ _, subsingleton.elim _ _, + commutes' := λ _, subsingleton.elim _ _, + ..(0 : B →+ A) } } + universes v u w set_option old_structure_cmd true @@ -66,7 +76,10 @@ instance (M N : QuadraticModule R) : linear_map_class (M ⟶ N) R M N := end QuadraticModule -/-- The "clifford algebra" functor, sending a quadratic R-module V to the clifford algebra on `V`. -/ +/-- The "clifford algebra" functor, sending a quadratic `R`-module `V` to the clifford algebra on +`V`. + +This is `clifford_algebra.map` through the lens of category theory. -/ @[simps] def CliffordAlgebra : QuadraticModule.{u} R ⥤ Algebra.{u} R := { obj := λ M, @@ -90,7 +103,10 @@ namespace Cliff /-- Convert a `clifford_hom Q A` to an element of `Cliff Q`. -/ def of {A : Type v} [ring A] [algebra R A] (f : clifford_hom Q A) : Cliff.{v} Q := -{ alg := Algebra.of R A, hom := f } +{ alg := Algebra.of R A, hom := f } + +/-- `clifford_algebra Q` as an element of `Cliff Q` -/ +@[reducible] protected def clifford_algebra : Cliff Q := Cliff.of Q ⟨ι Q, ι_sq_scalar Q⟩ instance : category (Cliff Q) := { hom := λ f g, {h : f.alg ⟶ g.alg // (alg_hom.to_linear_map h).comp f.hom.val = g.hom.val }, @@ -111,15 +127,27 @@ instance has_forget_to_Algebra : has_forget₂ (Cliff Q) (Algebra R) := { obj := λ x, x.alg, map := λ x y f, f.val } } -instance (Y : Cliff Q) : unique (Cliff.of Q ⟨ι Q, ι_sq_scalar Q⟩ ⟶ Y) := +instance unique_from (Y : Cliff Q) : unique (Cliff.clifford_algebra Q ⟶ Y) := { default := ⟨clifford_algebra.lift Q Y.hom, let ⟨A, ι, hι⟩ := Y in ι_comp_lift ι hι⟩, uniq := λ f, subtype.ext begin obtain ⟨A, ι, hι⟩ := Y, exact (clifford_algebra.lift_unique _ hι f.val).mp f.prop, end } -end Cliff +instance unique_to (X : Cliff Q) {A : Type v} [ring A] [algebra R A] [subsingleton A] + (f : clifford_hom Q A): + unique (X ⟶ Cliff.of Q f) := +{ default := ⟨(0 : X.alg →ₐ[R] A), linear_map.ext $ λ x, @subsingleton.elim A _ _ _⟩, + uniq := λ f, subtype.ext $ alg_hom.ext (λ x, @subsingleton.elim A _ _ _) } /-- The clifford algebra is the initial object in `Cliff`. -/ -def clifford_algebra.is_initial : limits.is_initial (Cliff.of Q ⟨ι Q, ι_sq_scalar Q⟩) := +def is_initial_clifford_algebra : limits.is_initial (Cliff.clifford_algebra Q) := limits.is_initial.of_unique _ + +/-- A trivial algebra is a terminal object in `Cliff`. -/ +def is_terminal_of_subsingleton + {A : Type v} [ring A] [algebra R A] [subsingleton A] : + limits.is_terminal (Cliff.of Q (0 : clifford_hom _ A)) := +limits.is_terminal.of_unique _ + +end Cliff From 5a4d578666cdff64bce0ce12c0316986187597e0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 18:30:49 +0000 Subject: [PATCH 6/8] add the exterior algebra functor too for good measure --- .../from_mathlib/category_theory.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/geometric_algebra/from_mathlib/category_theory.lean b/src/geometric_algebra/from_mathlib/category_theory.lean index ecbc9c964..f7454b1b0 100644 --- a/src/geometric_algebra/from_mathlib/category_theory.lean +++ b/src/geometric_algebra/from_mathlib/category_theory.lean @@ -1,5 +1,6 @@ import algebra.category.Algebra.basic import linear_algebra.clifford_algebra.basic +import linear_algebra.exterior_algebra.basic import geometric_algebra.from_mathlib.basic import for_mathlib.linear_algebra.quadratic_form.isometric_map @@ -88,6 +89,17 @@ def CliffordAlgebra : QuadraticModule.{u} R ⥤ Algebra.{u} R := map_id' := λ X, clifford_algebra.map_id _, map_comp' := λ M N P f g, (clifford_algebra.map_comp_map _ _ _ _ _ _ _).symm } +/-- The "exterior algebra" functor, sending an `R`-module `V` to the exterior algebra on `V`. + +In the language of geometric algebra, `(ExteriorAlgebra R).map f` is the outermorphism. -/ +@[simps] +def ExteriorAlgebra : Module.{u} R ⥤ Algebra.{u} R := +{ obj := λ M, + { carrier := exterior_algebra R M }, + map := λ M N f, clifford_algebra.map _ _ f (by simp), + 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) /-- From 3a06d0505ef88047a93b59958a45c59eb2a83b67 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 20 Aug 2023 11:47:07 +0000 Subject: [PATCH 7/8] expand the laurents example --- .../translations/laurents.lean | 141 ++++++++++++++++-- 1 file changed, 131 insertions(+), 10 deletions(-) diff --git a/src/geometric_algebra/translations/laurents.lean b/src/geometric_algebra/translations/laurents.lean index 1a5e1617e..e0cdabd0d 100644 --- a/src/geometric_algebra/translations/laurents.lean +++ b/src/geometric_algebra/translations/laurents.lean @@ -6,6 +6,7 @@ Authors: Eric Wieser import algebra.field.basic import algebra.module.prod import algebra.punit_instances +import data.finset.sort import data.vector import tactic @@ -58,25 +59,145 @@ def conj : Π {n}, Gₙ α n → Gₙ α n | (n + 1) ⟨x₁, x₂⟩ := (-conj x₁, conj x₂) def conj_d : Π {n}, Gₙ α n → Gₙ α n | 0 x := x -| (n + 1) ⟨x₁, x₂⟩ := (conj x₁, -conj x₂) +| (n + 1) ⟨x₁, x₂⟩ := (conj_d x₁, -conj_d x₂) prefix (name := laurent.conj) `̅`:max := conj -- this unicode is probably a bad idea... notation (name := laurent.conj_d) `̅`:max x `ᵈ` := conj_d x -- this unicode is definitly a bad idea! -- vee and wedge -reserve infix `⋎`:70 -def vee : Π {n}, Gₙ α n → Gₙ α n → Gₙ α n -| 0 x y := (x * y : α) -| (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ := let infix ` ⋎ ` := vee in - (x₁ ⋎ y₂ + ̅x₂ ⋎ y₁, x₂ ⋎ y₂) -infix (name := laurent.vee) ` ⋎ ` := vee reserve infix `⋏`:70 def wedge : Π {n}, Gₙ α n → Gₙ α n → Gₙ α n | 0 x y := (x * y : α) | (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ := let infix ` ⋏ ` := wedge in - (x₂ ⋏ y₂, x₁ ⋏ y₂ + x₂ ⋏ ̅y₁ᵈ) + (x₁ ⋏ y₂ + ̅x₂ ⋏ y₁, x₂ ⋏ y₂) infix (name := laurent.wedge) ` ⋏ ` := wedge +reserve infix `⋎`:70 +def vee : Π {n}, Gₙ α n → Gₙ α n → Gₙ α n +| 0 x y := (x * y : α) +| (n + 1) ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ := let infix ` ⋎ ` := vee in + (x₂ ⋎ y₂, x₁ ⋎ y₂ + x₂ ⋎ ̅y₁ᵈ) +infix (name := laurent.vee) ` ⋎ ` := vee + +instance {n} : has_one (Gₙ α n):= ⟨(1 : α)⟩ + +section theorems + +lemma conj_zero : Π {n}, conj (0 : Gₙ α n) = 0 +| 0 := rfl +| (n + 1) := prod.ext + ((congr_arg has_neg.neg conj_zero).trans neg_zero) + conj_zero + +lemma conj_add : Π {n} (x y : Gₙ α n), conj (x + y) = conj x + conj y +| 0 (x : α) y := rfl +| (n + 1) (x₁, x₂) (y₁, y₂) := prod.ext + ((congr_arg _ $ conj_add x₁ y₁).trans $ neg_add _ _) + (conj_add x₂ y₂) + +lemma conj_d_zero : Π {n}, conj_d (0 : Gₙ α n) = 0 +| 0 := rfl +| (n + 1) := prod.ext + conj_d_zero + ((congr_arg has_neg.neg conj_d_zero).trans neg_zero) + +lemma conj_d_add : Π {n} (x y : Gₙ α n), conj_d (x + y) = conj_d x + conj_d y +| 0 (x : α) y := rfl +| (n + 1) (x₁, x₂) (y₁, y₂) := prod.ext + (conj_d_add x₁ y₁) + ((congr_arg _ $ conj_d_add x₂ y₂).trans $ neg_add _ _) + +lemma wedge_add : Π {n} (x y z : Gₙ α n), x ⋏ (y + z) = x ⋏ y + x ⋏ z +| 0 (x : α) y z := mul_add x y z +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + ((congr_arg2 (+) (wedge_add _ _ _) (wedge_add _ _ _)).trans (add_add_add_comm _ _ _ _)) + (wedge_add _ _ _) + +lemma add_wedge : Π {n} (x y z : Gₙ α n), (x + y) ⋏ z = x ⋏ z + y ⋏ z +| 0 (x : α) y z := add_mul x y z +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + ((congr_arg2 (+) (add_wedge _ _ _) $ + eq.trans (by rw [conj_add]) (add_wedge _ _ _)).trans (add_add_add_comm _ _ _ _)) + (add_wedge _ _ _) + +lemma vee_add : Π {n} (x y z : Gₙ α n), x ⋎ (y + z) = x ⋎ y + x ⋎ z +| 0 (x : α) y z := mul_add x y z +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + (vee_add _ _ _) + ((congr_arg2 (+) (vee_add _ _ _) $ + (congr_arg _ (conj_d_add _ _)).trans (vee_add _ _ _)).trans (add_add_add_comm _ _ _ _)) + +lemma add_vee : Π {n} (x y z : Gₙ α n), (x + y) ⋎ z = x ⋎ z + y ⋎ z +| 0 (x : α) y z := add_mul x y z +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + (add_vee _ _ _) + (eq.trans (congr_arg2 (+) (add_vee _ _ _) (add_vee _ _ _)) (add_add_add_comm _ _ _ _)) + +lemma wedge_zero : Π {n} (x : Gₙ α n), x ⋏ 0 = 0 +| 0 (x : α) := mul_zero x +| (n + 1) (x₁, x₂) := prod.ext + ((congr_arg2 _ (wedge_zero _) (wedge_zero _)).trans $ add_zero _) (wedge_zero _) + +lemma zero_wedge : Π {n} (x : Gₙ α n), 0 ⋏ x = 0 +| 0 (x : α) := zero_mul x +| (n + 1) (x₁, x₂) := prod.ext + ((congr_arg2 (+) (zero_wedge _) + (by rw [conj_zero, zero_wedge])).trans $ add_zero _) (zero_wedge _) + +lemma wedge_one : Π {n} (x : Gₙ α n), x ⋏ 1 = x +| 0 (x : α) := mul_one x +| (n + 1) (x₁, x₂) := prod.ext (show x₁ ⋏ 1 + _ ⋏ _ = _, by rw [wedge_one]; sorry) (wedge_one _) + +lemma wedge_assoc : Π {n} (x y z : Gₙ α n), (x ⋏ y) ⋏ z = x ⋏ (y ⋏ z) +| 0 (x : α) y z := mul_assoc x y z +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + (by { + simp_rw [wedge, add_wedge, wedge_add, ←wedge_assoc, add_assoc], + congr' 2, + sorry }) + (wedge_assoc _ _ _) + +end theorems + +def Gₙ.coeff : Π {n}, Gₙ α n → finset (fin n) → α +| 0 x s := x +| (n + 1) (xi, yi) s := + let s' : finset (fin n) := s.bUnion (λ i : fin n.succ, fin.cases ∅ singleton i) in + (if (0 : fin n.succ) ∈ s then xi else yi).coeff s' + +instance has_repr [has_repr α] {n} : has_repr (Gₙ α n) := +{ repr := λ x, + let basis : list (finset (fin n)) := + (list.range (n + 1)).bind (λ k, + ((list.fin_range n).sublists_len k).map list.to_finset) in + let parts := basis.filter_map $ λ s, + let c := repr (x.coeff s) in + if c = "0" then + none + else + some $ c ++ + if s.card = 0 then + "" + else + "•e" ++ string.join ((s.sort (≤)).map repr) in + match parts with + | [] := "0" + | _ := string.intercalate " + " parts + end } + +section example_3d + +def x : Kₙ ℚ 3 := (1, 0, 0, ()) +def y : Kₙ ℚ 3 := (0, 1, 0, ()) +def z : Kₙ ℚ 3 := (0, 0, 1, ()) + +#eval (0 : Gₙ ℚ 3) +#eval [(x : Gₙ ℚ 3), (y : Gₙ ℚ 3), (z : Gₙ ℚ 3)] +#eval [(x ⋏ y : Gₙ ℚ 3), (y ⋏ z : Gₙ ℚ 3), (x ⋏ z : Gₙ ℚ 3)] +#eval [(x ⋎ y : Gₙ ℚ 3), (y ⋎ z : Gₙ ℚ 3), (x ⋎ z : Gₙ ℚ 3)] +#eval [((x ⋏ y) ⋏ z : Gₙ ℚ 3), (x ⋏ (y ⋏ z) : Gₙ ℚ 3)] +#eval [((x ⋏ y) ⋏ z : Gₙ ℚ 3), (x ⋏ (y ⋏ z) : Gₙ ℚ 3)] +#eval [((x ⋎ y) ⋎ z : Gₙ ℚ 3), (x ⋎ (y ⋎ z) : Gₙ ℚ 3)] +#eval show Gₙ ℚ 3, from (x + y) ⋎ (x ⋏ y) -variables {a b : Gₙ α 2} -#check (a + b) ⋎ (a ⋏ b) +end example_3d end laurent From 0947a6d21cf5a724732c29dabbc7f543edb66d4e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 20 Aug 2023 12:50:38 +0000 Subject: [PATCH 8/8] sorry-free --- .../translations/laurents.lean | 179 ++++++++++++++---- 1 file changed, 138 insertions(+), 41 deletions(-) diff --git a/src/geometric_algebra/translations/laurents.lean b/src/geometric_algebra/translations/laurents.lean index e0cdabd0d..8419191ed 100644 --- a/src/geometric_algebra/translations/laurents.lean +++ b/src/geometric_algebra/translations/laurents.lean @@ -5,6 +5,7 @@ Authors: Eric Wieser -/ import algebra.field.basic import algebra.module.prod +import algebra.algebra.basic import algebra.punit_instances import data.finset.sort import data.vector @@ -40,6 +41,9 @@ def Gₙ : ℕ → Type instance : Π n, add_comm_group (Gₙ α n) | 0 := by {unfold Gₙ, apply_instance} | (n + 1) := by {unfold Gₙ, haveI := Gₙ.add_comm_group n, apply_instance} +instance : Π n, module α (Gₙ α n) +| 0 := by {dunfold Gₙ, apply_instance} +| (n + 1) := by {dunfold Gₙ, haveI := Gₙ.module n, apply_instance} variables {α} @@ -79,31 +83,42 @@ infix (name := laurent.vee) ` ⋎ ` := vee instance {n} : has_one (Gₙ α n):= ⟨(1 : α)⟩ -section theorems +section ring_theorems +@[simp] +lemma coe_α_zero : Π {n}, coe_α 0 = (0 : Gₙ α n) +| 0 := rfl +| (n + 1) := prod.ext coe_α_zero coe_α_zero + +@[simp] +lemma coe_α_add : Π {n} (a b : α), coe_α (a + b) = (coe_α a + coe_α b : Gₙ α n) +| 0 a b := rfl +| (n + 1) a b:= prod.ext (by simp [coe_α]) (coe_α_add _ _) + +@[simp] lemma conj_zero : Π {n}, conj (0 : Gₙ α n) = 0 | 0 := rfl | (n + 1) := prod.ext ((congr_arg has_neg.neg conj_zero).trans neg_zero) conj_zero -lemma conj_add : Π {n} (x y : Gₙ α n), conj (x + y) = conj x + conj y -| 0 (x : α) y := rfl -| (n + 1) (x₁, x₂) (y₁, y₂) := prod.ext - ((congr_arg _ $ conj_add x₁ y₁).trans $ neg_add _ _) - (conj_add x₂ y₂) +@[simp] +lemma conj_coe_α : Π {n} a, conj (coe_α a) = (coe_α a : Gₙ α n) +| 0 a := rfl +| (n + 1) a := prod.ext (by simp [conj, coe_α]) (conj_coe_α _) -lemma conj_d_zero : Π {n}, conj_d (0 : Gₙ α n) = 0 +@[simp] +lemma conj_one : Π {n}, conj (1 : Gₙ α n) = 1 | 0 := rfl | (n + 1) := prod.ext - conj_d_zero - ((congr_arg has_neg.neg conj_d_zero).trans neg_zero) + (show -conj _ = coe_α _, by rw [coe_α_zero, conj_zero, neg_zero]) + conj_one -lemma conj_d_add : Π {n} (x y : Gₙ α n), conj_d (x + y) = conj_d x + conj_d y +lemma conj_add : Π {n} (x y : Gₙ α n), conj (x + y) = conj x + conj y | 0 (x : α) y := rfl | (n + 1) (x₁, x₂) (y₁, y₂) := prod.ext - (conj_d_add x₁ y₁) - ((congr_arg _ $ conj_d_add x₂ y₂).trans $ neg_add _ _) + ((congr_arg _ $ conj_add x₁ y₁).trans $ neg_add _ _) + (conj_add x₂ y₂) lemma wedge_add : Π {n} (x y z : Gₙ α n), x ⋏ (y + z) = x ⋏ y + x ⋏ z | 0 (x : α) y z := mul_add x y z @@ -118,44 +133,126 @@ lemma add_wedge : Π {n} (x y z : Gₙ α n), (x + y) ⋏ z = x ⋏ z + y ⋏ z eq.trans (by rw [conj_add]) (add_wedge _ _ _)).trans (add_add_add_comm _ _ _ _)) (add_wedge _ _ _) -lemma vee_add : Π {n} (x y z : Gₙ α n), x ⋎ (y + z) = x ⋎ y + x ⋎ z -| 0 (x : α) y z := mul_add x y z -| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext - (vee_add _ _ _) - ((congr_arg2 (+) (vee_add _ _ _) $ - (congr_arg _ (conj_d_add _ _)).trans (vee_add _ _ _)).trans (add_add_add_comm _ _ _ _)) - -lemma add_vee : Π {n} (x y z : Gₙ α n), (x + y) ⋎ z = x ⋎ z + y ⋎ z -| 0 (x : α) y z := add_mul x y z -| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext - (add_vee _ _ _) - (eq.trans (congr_arg2 (+) (add_vee _ _ _) (add_vee _ _ _)) (add_add_add_comm _ _ _ _)) - +@[simp] lemma wedge_zero : Π {n} (x : Gₙ α n), x ⋏ 0 = 0 | 0 (x : α) := mul_zero x | (n + 1) (x₁, x₂) := prod.ext ((congr_arg2 _ (wedge_zero _) (wedge_zero _)).trans $ add_zero _) (wedge_zero _) +@[simp] lemma zero_wedge : Π {n} (x : Gₙ α n), 0 ⋏ x = 0 | 0 (x : α) := zero_mul x | (n + 1) (x₁, x₂) := prod.ext ((congr_arg2 (+) (zero_wedge _) (by rw [conj_zero, zero_wedge])).trans $ add_zero _) (zero_wedge _) +@[simp] lemma wedge_one : Π {n} (x : Gₙ α n), x ⋏ 1 = x | 0 (x : α) := mul_one x -| (n + 1) (x₁, x₂) := prod.ext (show x₁ ⋏ 1 + _ ⋏ _ = _, by rw [wedge_one]; sorry) (wedge_one _) +| (n + 1) (x₁, x₂) := prod.ext + (show x₁ ⋏ 1 + _ ⋏ _ = _, by rw [wedge_one, coe_α_zero, wedge_zero, add_zero]) + (wedge_one _) + +@[simp] +lemma one_wedge : Π {n} (x : Gₙ α n), 1 ⋏ x = x +| 0 (x : α) := one_mul x +| (n + 1) (x₁, x₂) := prod.ext + (show _ ⋏ _ + (conj 1) ⋏ _ = _, by rw [conj_one, one_wedge, coe_α_zero, zero_wedge, zero_add]) + (one_wedge _) + +instance {n} : non_assoc_ring (Gₙ α n) := +{ mul := (⋏), + one := 1, + zero_mul := zero_wedge, + mul_zero := wedge_zero, + one_mul := one_wedge, + mul_one := wedge_one, + left_distrib := wedge_add, + right_distrib := add_wedge, + .. (by apply_instance : add_comm_group (Gₙ α n)) } + +@[simp] +lemma wedge_neg {n} (x y : Gₙ α n) : x ⋏ (-y) = -(x ⋏ y) := +mul_neg _ _ + +@[simp] +lemma neg_wedge {n} (x y : Gₙ α n) : (-x) ⋏ y = -(x ⋏ y) := +neg_mul _ _ + +lemma conj_wedge : Π {n} (x y : Gₙ α n), conj (x ⋏ y) = conj x ⋏ conj y +| 0 (x : α) y := by simp [wedge, conj] +| (n + 1) (x₁, x₂) (y₁, y₂) := by simp [wedge, conj, conj_wedge, conj_add, add_comm] lemma wedge_assoc : Π {n} (x y z : Gₙ α n), (x ⋏ y) ⋏ z = x ⋏ (y ⋏ z) | 0 (x : α) y z := mul_assoc x y z | (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext - (by { - simp_rw [wedge, add_wedge, wedge_add, ←wedge_assoc, add_assoc], - congr' 2, - sorry }) + (by simp_rw [wedge, add_wedge, wedge_add, ←wedge_assoc, add_assoc, conj_wedge]) (wedge_assoc _ _ _) -end theorems +lemma coe_α_wedge : Π {n} (a : α) (x : Gₙ α n), coe_α a ⋏ x = a • x +| 0 a (x : α) := rfl +| (n + 1) a (x₁, x₂) := prod.ext + (by simp_rw [coe_α, wedge, prod.smul_fst, coe_α_zero, zero_wedge, zero_add, conj_coe_α, + coe_α_wedge]) + (coe_α_wedge _ _) + +lemma wedge_coe_α : Π {n} (x : Gₙ α n) (a : α), x ⋏ coe_α a = a • x +| 0 (x : α) a := mul_comm x a +| (n + 1) (x₁, x₂) a := prod.ext + (by simp [coe_α, wedge, wedge_coe_α]) + (by simp [coe_α, wedge, wedge_coe_α]) + +lemma coe_α_mul : Π {n} (a b : α), coe_α (a * b) = (coe_α a ⋏ coe_α b : Gₙ α n) +| 0 a b := rfl +| (n + 1) a b := prod.ext (by simp [coe_α, wedge]) (by simp [coe_α, wedge, @coe_α_mul n]) + +instance {n} : ring (Gₙ α n) := +{ mul := (⋏), + one := 1, + mul_assoc := wedge_assoc, + .. (by apply_instance : non_assoc_ring (Gₙ α n)) } + +instance {n} : algebra α (Gₙ α n) := +{ smul := (•), + to_fun := coe_α, + map_one' := rfl, + map_mul' := coe_α_mul, + map_zero' := coe_α_zero, + map_add' := coe_α_add, + commutes' := λ r x, (coe_α_wedge r x).trans (wedge_coe_α _ _).symm, + smul_def' := λ r x, (coe_α_wedge r x).symm } + +end ring_theorems + +section vee_theorems + +@[simp] +lemma conj_d_zero : Π {n}, conj_d (0 : Gₙ α n) = 0 +| 0 := rfl +| (n + 1) := prod.ext + conj_d_zero + ((congr_arg has_neg.neg conj_d_zero).trans neg_zero) + +lemma conj_d_add : Π {n} (x y : Gₙ α n), conj_d (x + y) = conj_d x + conj_d y +| 0 (x : α) y := rfl +| (n + 1) (x₁, x₂) (y₁, y₂) := prod.ext + (conj_d_add x₁ y₁) + ((congr_arg _ $ conj_d_add x₂ y₂).trans $ neg_add _ _) + +lemma vee_add : Π {n} (x y z : Gₙ α n), x ⋎ (y + z) = x ⋎ y + x ⋎ z +| 0 (x : α) y z := (mul_add x y z :_) +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + (vee_add _ _ _) + ((congr_arg2 (+) (vee_add _ _ _) $ + (congr_arg _ (conj_d_add _ _)).trans (vee_add _ _ _)).trans (add_add_add_comm _ _ _ _)) + +lemma add_vee : Π {n} (x y z : Gₙ α n), (x + y) ⋎ z = x ⋎ z + y ⋎ z +| 0 (x : α) y z := (add_mul x y z : _) +| (n + 1) (x₁, x₂) (y₁, y₂) (z₁, z₂) := prod.ext + (add_vee _ _ _) + (eq.trans (congr_arg2 (+) (add_vee _ _ _) (add_vee _ _ _)) (add_add_add_comm _ _ _ _)) + +end vee_theorems def Gₙ.coeff : Π {n}, Gₙ α n → finset (fin n) → α | 0 x s := x @@ -185,18 +282,18 @@ instance has_repr [has_repr α] {n} : has_repr (Gₙ α n) := section example_3d -def x : Kₙ ℚ 3 := (1, 0, 0, ()) -def y : Kₙ ℚ 3 := (0, 1, 0, ()) -def z : Kₙ ℚ 3 := (0, 0, 1, ()) +def x : Gₙ ℚ 3 := coe_Kₙ (1, 0, 0, ()) +def y : Gₙ ℚ 3 := coe_Kₙ (0, 1, 0, ()) +def z : Gₙ ℚ 3 := coe_Kₙ (0, 0, 1, ()) #eval (0 : Gₙ ℚ 3) -#eval [(x : Gₙ ℚ 3), (y : Gₙ ℚ 3), (z : Gₙ ℚ 3)] -#eval [(x ⋏ y : Gₙ ℚ 3), (y ⋏ z : Gₙ ℚ 3), (x ⋏ z : Gₙ ℚ 3)] -#eval [(x ⋎ y : Gₙ ℚ 3), (y ⋎ z : Gₙ ℚ 3), (x ⋎ z : Gₙ ℚ 3)] -#eval [((x ⋏ y) ⋏ z : Gₙ ℚ 3), (x ⋏ (y ⋏ z) : Gₙ ℚ 3)] -#eval [((x ⋏ y) ⋏ z : Gₙ ℚ 3), (x ⋏ (y ⋏ z) : Gₙ ℚ 3)] -#eval [((x ⋎ y) ⋎ z : Gₙ ℚ 3), (x ⋎ (y ⋎ z) : Gₙ ℚ 3)] -#eval show Gₙ ℚ 3, from (x + y) ⋎ (x ⋏ y) +#eval [x, y, z] +#eval [x ⋏ y, y ⋏ z, x ⋏ z] +#eval [x ⋎ y, y ⋎ z, x ⋎ z] +#eval [(x ⋏ y) ⋏ z, x ⋏ (y ⋏ z)] +#eval [(x ⋏ y) ⋏ z, x ⋏ (y ⋏ z)] +#eval [(x ⋎ y) ⋎ z, x ⋎ (y ⋎ z)] +#eval (x + y) ⋎ (x ⋏ y) end example_3d