From 4dea920be8dc6b9aa65716930a30458a24e99ec1 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Tue, 8 Jun 2021 18:12:25 +0100 Subject: [PATCH 1/7] feat(algebra/non_unital_alg_hom): define `non_unital_alg_hom` The motivation is to be able to state the universal property for a magma algebra using bundled morphisms. --- src/algebra/non_unital_alg_hom.lean | 171 ++++++++++++++++++++++++++++ 1 file changed, 171 insertions(+) create mode 100644 src/algebra/non_unital_alg_hom.lean diff --git a/src/algebra/non_unital_alg_hom.lean b/src/algebra/non_unital_alg_hom.lean new file mode 100644 index 0000000000000..fdca577c1dbe3 --- /dev/null +++ b/src/algebra/non_unital_alg_hom.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2021 Oliver Nash. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Oliver Nash +-/ +import algebra.algebra.basic + +/-! +# Morphisms of non-unital algebras + +This file defines morphisms between two modules, each of which also carries a multiplication that is +compatible with the additive structure. The multiplications are not assumed to be associative or +unital, or even compatible with the scalar multiplication. In a typical application, the +multiplications and scalar multiplications will satisfy compatibility conditions making them into +algebras (albeit possibly non-associative and/or non-unital) but such conditions are not required to +make this definition. + +## Main definitions + + * `non_unital_alg_hom` + * `alg_hom.non_unital_alg_hom.has_coe` + +## Tags + +non-unital, algebra, morphism +-/ + +universes u v w w₁ w₂ w₃ + +variables (R : Type u) (A : Type v) (B : Type w) (C : Type w₁) + +set_option old_structure_cmd true + +/-- A morphism respecting addition, multiplication, and scalar multiplication. When these arise from +algebra structures, this is the same as a not-necessarily-unital morphism of algebras. -/ +structure non_unital_alg_hom [semiring R] + [non_unital_non_assoc_semiring A] [module R A] + [non_unital_non_assoc_semiring B] [module R B] + extends A →ₗ[R] B, mul_hom A B + +attribute [nolint doc_blame] non_unital_alg_hom.to_linear_map +attribute [nolint doc_blame] non_unital_alg_hom.to_mul_hom + +initialize_simps_projections non_unital_alg_hom (to_fun → apply) + +namespace non_unital_alg_hom + +variables {R A B C} [semiring R] +variables [non_unital_non_assoc_semiring A] [module R A] +variables [non_unital_non_assoc_semiring B] [module R B] +variables [non_unital_non_assoc_semiring C] [module R C] + +/-- see Note [function coercion] -/ +instance : has_coe_to_fun (non_unital_alg_hom R A B) := ⟨_, to_fun⟩ + +lemma coe_injective : + @function.injective (non_unital_alg_hom R A B) (A → B) coe_fn := +by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr + +@[ext] lemma ext {f g : non_unital_alg_hom R A B} (h : ∀ x, f x = g x) : f = g := +coe_injective $ funext h + +lemma ext_iff {f g : non_unital_alg_hom R A B} : f = g ↔ ∀ x, f x = g x := +⟨by { rintro rfl x, refl }, ext⟩ + +@[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃) : + ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : A → B) = f := +rfl + +@[simp] lemma mk_coe (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : + (⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) = f := +by { ext, refl, } + +instance : has_coe (non_unital_alg_hom R A B) (A →ₗ[R] B) := ⟨to_linear_map⟩ + +instance : has_coe (non_unital_alg_hom R A B) (mul_hom A B) := ⟨to_mul_hom⟩ + +@[simp] lemma to_linear_map_eq_coe (f : non_unital_alg_hom R A B) : f.to_linear_map = ↑f := +rfl + +@[simp] lemma to_mul_hom_eq_coe (f : non_unital_alg_hom R A B) : f.to_mul_hom = ↑f := +rfl + +@[simp, norm_cast] lemma coe_to_linear_map (f : non_unital_alg_hom R A B) : + ((f : A →ₗ[R] B) : A → B) = f := +rfl + +@[simp, norm_cast] lemma coe_to_mul_hom (f : non_unital_alg_hom R A B) : + ((f : mul_hom A B) : A → B) = f := +rfl + +@[norm_cast] lemma coe_linear_map_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : + ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : A →ₗ[R] B) = ⟨f, h₁, h₂⟩ := +by { ext, refl, } + +@[norm_cast] lemma coe_mul_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : + ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : mul_hom A B) = ⟨f, h₃⟩ := +by { ext, refl, } + +@[simp] lemma map_smul (f : non_unital_alg_hom R A B) (c : R) (x : A) : + f (c • x) = c • f x := +f.to_linear_map.map_smul c x + +@[simp] lemma map_add (f : non_unital_alg_hom R A B) (x y : A) : + f (x + y) = (f x) + (f y) := +f.to_linear_map.map_add x y + +@[simp] lemma map_mul (f : non_unital_alg_hom R A B) (x y : A) : + f (x * y) = (f x) * (f y) := +f.to_mul_hom.map_mul x y + +@[simp] lemma map_zero (f : non_unital_alg_hom R A B) : f 0 = 0 := +f.to_linear_map.map_zero + +instance : has_zero (non_unital_alg_hom R A B) := +⟨{ map_mul' := by simp, + .. (0 : A →ₗ[R] B)}⟩ + +instance : has_one (non_unital_alg_hom R A A) := +⟨{ map_mul' := by simp, + .. (1 : A →ₗ[R] A) }⟩ + +@[simp] lemma coe_zero : ((0 : non_unital_alg_hom R A B) : A → B) = 0 := rfl + +@[simp] lemma coe_one : ((1 : non_unital_alg_hom R A A) : A → A) = id := rfl + +lemma zero_apply (a : A) : (0 : non_unital_alg_hom R A B) a = 0 := rfl + +lemma one_apply (a : A) : (1 : non_unital_alg_hom R A A) a = a := rfl + +instance : inhabited (non_unital_alg_hom R A B) := ⟨0⟩ + +/-- The composition of morphisms is a morphism. -/ +def comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : non_unital_alg_hom R A C := +{ .. mul_hom.comp (f : mul_hom B C) (g : mul_hom A B), + .. linear_map.comp (f : B →ₗ[R] C) (g : A →ₗ[R] B) } + +@[simp, norm_cast] lemma coe_comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : + (f.comp g : A → C) = (f : B → C) ∘ (g : A → B) := +rfl + +lemma comp_apply (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) (x : A) : + f.comp g x = f (g x) := +rfl + +/-- The inverse of a bijective morphism is a morphism. -/ +def inverse (f : non_unital_alg_hom R A B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + non_unital_alg_hom R B A := +{ .. mul_hom.inverse (f : mul_hom A B) g h₁ h₂, + .. linear_map.inverse (f : A →ₗ[R] B) g h₁ h₂ } + +@[simp] lemma coe_inverse (f : non_unital_alg_hom R A B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + (inverse f g h₁ h₂ : B → A) = g := +rfl + +end non_unital_alg_hom + +namespace alg_hom + +variables [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] + +instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (non_unital_alg_hom R A B) := +⟨λ f, { map_smul' := f.map_smul, .. f, }⟩ + +@[simp, norm_cast] lemma coe_to_non_unital_alg_hom (f : A →ₐ[R] B) : + ((f : non_unital_alg_hom R A B) : A → B) = f := +rfl + +end alg_hom From f7a90714b913828c40b98da6f0fc3918a07ba263 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Tue, 8 Jun 2021 19:05:38 +0100 Subject: [PATCH 2/7] Add `to_non_unital_alg_hom` --- src/algebra/non_unital_alg_hom.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/algebra/non_unital_alg_hom.lean b/src/algebra/non_unital_alg_hom.lean index fdca577c1dbe3..f946d4772b956 100644 --- a/src/algebra/non_unital_alg_hom.lean +++ b/src/algebra/non_unital_alg_hom.lean @@ -18,7 +18,7 @@ make this definition. ## Main definitions * `non_unital_alg_hom` - * `alg_hom.non_unital_alg_hom.has_coe` + * `alg_hom.to_non_unital_alg_hom` ## Tags @@ -159,10 +159,17 @@ end non_unital_alg_hom namespace alg_hom -variables [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] +variables {R A B} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] + +/-- A unital morphism of algebras is a `non_unital_alg_hom`. -/ +def to_non_unital_alg_hom (f : A →ₐ[R] B) : non_unital_alg_hom R A B := +{ map_smul' := f.map_smul, .. f, } instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (non_unital_alg_hom R A B) := -⟨λ f, { map_smul' := f.map_smul, .. f, }⟩ +⟨to_non_unital_alg_hom⟩ + +@[simp] lemma to_non_unital_alg_hom_eq_coe (f : A →ₐ[R] B) : f.to_non_unital_alg_hom = f := +rfl @[simp, norm_cast] lemma coe_to_non_unital_alg_hom (f : A →ₐ[R] B) : ((f : non_unital_alg_hom R A B) : A → B) = f := From c3299ea8bca06f3221ed6188bd61f4680083372f Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Tue, 8 Jun 2021 22:13:28 +0100 Subject: [PATCH 3/7] Generalise from `module` to just `distrib_mul_action` --- src/algebra/group_action_hom.lean | 57 +++++++++++++++++++++++- src/algebra/non_unital_alg_hom.lean | 68 +++++++++++++++-------------- 2 files changed, 91 insertions(+), 34 deletions(-) diff --git a/src/algebra/group_action_hom.lean b/src/algebra/group_action_hom.lean index 0a468163f8ea3..5f5e66e38a2f5 100644 --- a/src/algebra/group_action_hom.lean +++ b/src/algebra/group_action_hom.lean @@ -93,6 +93,18 @@ ext $ λ x, by rw [comp_apply, id_apply] @[simp] lemma comp_id (f : X →[M'] Y) : f.comp (mul_action_hom.id M') = f := ext $ λ x, by rw [comp_apply, id_apply] +variables {A B} + +/-- The inverse of a bijective equivariant map is equivariant. -/ +def inverse (f : A →[M] B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + B →[M] A := +{ to_fun := g, + map_smul' := λ m x, + calc g (m • x) = g (m • (f (g x))) : by rw h₂ + ... = g (f (m • (g x))) : by rw f.map_smul + ... = m • g x : by rw h₁, } + variables {G} (H) /-- The canonical map to the left cosets. -/ @@ -103,8 +115,22 @@ def to_quotient : G →[G] quotient_group.quotient H := end mul_action_hom +-- TODO Is this _really_ missing!!? Where should it go? +/-- The inverse of a bijective `monoid_hom` is a `monoid_hom`. -/ +@[to_additive "The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`."] +def monoid_hom.inverse {A B : Type*} [monoid A] [monoid B] (f : A →* B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + B →* A := +{ to_fun := g, + map_one' := + calc g 1 = g (f 1) : by rw f.map_one + ... = 1 : by rw h₁, + map_mul' := λ x y, + calc g (x * y) = g ((f (g x)) * (f (g y))) : by rw [h₂, h₂] + ... = g (f ((g x) * (g y))) : by rw f.map_mul + ... = (g x) * (g y) : by rw h₁, } + /-- Equivariant additive monoid homomorphisms. -/ -@[nolint has_inhabited_instance] structure distrib_mul_action_hom extends A →[M] B, A →+ B. /-- Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism. -/ @@ -124,10 +150,12 @@ instance has_coe' : has_coe (A →+[M] B) (A →[M] B) := ⟨to_mul_action_hom⟩ instance : has_coe_to_fun (A →+[M] B) := -⟨_, λ c, c.to_fun⟩ +⟨_, to_fun⟩ variables {M A B} +@[simp] lemma to_fun_eq_coe (f : A →+[M] B) : f.to_fun = ⇑f := rfl + @[norm_cast] lemma coe_fn_coe (f : A →+[M] B) : ((f : A →+ B) : A → B) = f := rfl @[norm_cast] lemma coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f := rfl @@ -137,6 +165,24 @@ variables {M A B} theorem ext_iff {f g : A →+[M] B} : f = g ↔ ∀ x, f x = g x := ⟨λ H x, by rw H, ext⟩ +instance : has_zero (A →+[M] B) := +⟨{ map_smul' := by simp, + .. (0 : A →+ B) }⟩ + +instance : has_one (A →+[M] A) := +⟨{ map_smul' := by simp, + .. add_monoid_hom.id A }⟩ + +@[simp] lemma coe_zero : ((0 : A →+[M] B) : A → B) = 0 := rfl + +@[simp] lemma coe_one : ((1 : A →+[M] A) : A → A) = id := rfl + +lemma zero_apply (a : A) : (0 : A →+[M] B) a = 0 := rfl + +lemma one_apply (a : A) : (1 : A →+[M] A) a = a := rfl + +instance : inhabited (A →+[M] B) := ⟨0⟩ + @[simp] lemma map_zero (f : A →+[M] B) : f 0 = 0 := f.map_zero' @@ -175,6 +221,13 @@ ext $ λ x, by rw [comp_apply, id_apply] @[simp] lemma comp_id (f : A →+[M] B) : f.comp (distrib_mul_action_hom.id M) = f := ext $ λ x, by rw [comp_apply, id_apply] +/-- The inverse of a bijective `distrib_mul_action_hom` is a `distrib_mul_action_hom`. -/ +def inverse (f : A →+[M] B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + B →+[M] A := +{ .. (f : A →+ B).inverse g h₁ h₂, + .. (f : A →[M] B).inverse g h₁ h₂ } + end distrib_mul_action_hom /-- Equivariant ring homomorphisms. -/ diff --git a/src/algebra/non_unital_alg_hom.lean b/src/algebra/non_unital_alg_hom.lean index f946d4772b956..a46642ff208bc 100644 --- a/src/algebra/non_unital_alg_hom.lean +++ b/src/algebra/non_unital_alg_hom.lean @@ -8,12 +8,11 @@ import algebra.algebra.basic /-! # Morphisms of non-unital algebras -This file defines morphisms between two modules, each of which also carries a multiplication that is -compatible with the additive structure. The multiplications are not assumed to be associative or -unital, or even compatible with the scalar multiplication. In a typical application, the -multiplications and scalar multiplications will satisfy compatibility conditions making them into -algebras (albeit possibly non-associative and/or non-unital) but such conditions are not required to -make this definition. +This file defines morphisms between two types, each of which carries an addition, additive zero, +multiplication, and scalar action. The multiplications are not assumed to be associative or +unital, or even to be compatible with the scalar multiplications. In a typical application, the +operations will satisfy compatibility conditions making them into algebras (albeit possibly +non-associative and/or non-unital) but such conditions are not required to make this definition. ## Main definitions @@ -33,12 +32,12 @@ set_option old_structure_cmd true /-- A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras. -/ -structure non_unital_alg_hom [semiring R] - [non_unital_non_assoc_semiring A] [module R A] - [non_unital_non_assoc_semiring B] [module R B] - extends A →ₗ[R] B, mul_hom A B +structure non_unital_alg_hom [monoid R] + [non_unital_non_assoc_semiring A] [distrib_mul_action R A] + [non_unital_non_assoc_semiring B] [distrib_mul_action R B] + extends A →+[R] B, mul_hom A B -attribute [nolint doc_blame] non_unital_alg_hom.to_linear_map +attribute [nolint doc_blame] non_unital_alg_hom.to_distrib_mul_action_hom attribute [nolint doc_blame] non_unital_alg_hom.to_mul_hom initialize_simps_projections non_unital_alg_hom (to_fun → apply) @@ -53,6 +52,8 @@ variables [non_unital_non_assoc_semiring C] [module R C] /-- see Note [function coercion] -/ instance : has_coe_to_fun (non_unital_alg_hom R A B) := ⟨_, to_fun⟩ +@[simp] lemma to_fun_eq_coe (f : non_unital_alg_hom R A B) : f.to_fun = ⇑f := rfl + lemma coe_injective : @function.injective (non_unital_alg_hom R A B) (A → B) coe_fn := by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr @@ -63,62 +64,65 @@ coe_injective $ funext h lemma ext_iff {f g : non_unital_alg_hom R A B} : f = g ↔ ∀ x, f x = g x := ⟨by { rintro rfl x, refl }, ext⟩ -@[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃) : - ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : A → B) = f := +@[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : + ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A → B) = f := rfl -@[simp] lemma mk_coe (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : - (⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) = f := +@[simp] lemma mk_coe (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : + (⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) = f := by { ext, refl, } -instance : has_coe (non_unital_alg_hom R A B) (A →ₗ[R] B) := ⟨to_linear_map⟩ +instance : has_coe (non_unital_alg_hom R A B) (A →+[R] B) := +⟨to_distrib_mul_action_hom⟩ instance : has_coe (non_unital_alg_hom R A B) (mul_hom A B) := ⟨to_mul_hom⟩ -@[simp] lemma to_linear_map_eq_coe (f : non_unital_alg_hom R A B) : f.to_linear_map = ↑f := +@[simp] lemma to_distrib_mul_action_hom_eq_coe (f : non_unital_alg_hom R A B) : + f.to_distrib_mul_action_hom = ↑f := rfl @[simp] lemma to_mul_hom_eq_coe (f : non_unital_alg_hom R A B) : f.to_mul_hom = ↑f := rfl -@[simp, norm_cast] lemma coe_to_linear_map (f : non_unital_alg_hom R A B) : - ((f : A →ₗ[R] B) : A → B) = f := +@[simp, norm_cast] lemma coe_to_distrib_mul_action_hom (f : non_unital_alg_hom R A B) : + ((f : A →+[R] B) : A → B) = f := rfl @[simp, norm_cast] lemma coe_to_mul_hom (f : non_unital_alg_hom R A B) : ((f : mul_hom A B) : A → B) = f := rfl -@[norm_cast] lemma coe_linear_map_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : - ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : A →ₗ[R] B) = ⟨f, h₁, h₂⟩ := +@[norm_cast] lemma coe_linear_map_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : + ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A →+[R] B) = + ⟨f, h₁, h₂, h₃⟩ := by { ext, refl, } -@[norm_cast] lemma coe_mul_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃) : - ((⟨f, h₁, h₂, h₃⟩ : non_unital_alg_hom R A B) : mul_hom A B) = ⟨f, h₃⟩ := +@[norm_cast] lemma coe_mul_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : + ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : mul_hom A B) = ⟨f, h₄⟩ := by { ext, refl, } @[simp] lemma map_smul (f : non_unital_alg_hom R A B) (c : R) (x : A) : f (c • x) = c • f x := -f.to_linear_map.map_smul c x +f.to_distrib_mul_action_hom.map_smul c x @[simp] lemma map_add (f : non_unital_alg_hom R A B) (x y : A) : f (x + y) = (f x) + (f y) := -f.to_linear_map.map_add x y +f.to_distrib_mul_action_hom.map_add x y @[simp] lemma map_mul (f : non_unital_alg_hom R A B) (x y : A) : f (x * y) = (f x) * (f y) := f.to_mul_hom.map_mul x y @[simp] lemma map_zero (f : non_unital_alg_hom R A B) : f 0 = 0 := -f.to_linear_map.map_zero +f.to_distrib_mul_action_hom.map_zero instance : has_zero (non_unital_alg_hom R A B) := ⟨{ map_mul' := by simp, - .. (0 : A →ₗ[R] B)}⟩ + .. (0 : A →+[R] B) }⟩ instance : has_one (non_unital_alg_hom R A A) := ⟨{ map_mul' := by simp, - .. (1 : A →ₗ[R] A) }⟩ + .. (1 : A →+[R] A) }⟩ @[simp] lemma coe_zero : ((0 : non_unital_alg_hom R A B) : A → B) = 0 := rfl @@ -132,8 +136,8 @@ instance : inhabited (non_unital_alg_hom R A B) := ⟨0⟩ /-- The composition of morphisms is a morphism. -/ def comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : non_unital_alg_hom R A C := -{ .. mul_hom.comp (f : mul_hom B C) (g : mul_hom A B), - .. linear_map.comp (f : B →ₗ[R] C) (g : A →ₗ[R] B) } +{ .. (f : mul_hom B C).comp (g : mul_hom A B), + .. (f : B →+[R] C).comp (g : A →+[R] B) } @[simp, norm_cast] lemma coe_comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : (f.comp g : A → C) = (f : B → C) ∘ (g : A → B) := @@ -147,8 +151,8 @@ rfl def inverse (f : non_unital_alg_hom R A B) (g : B → A) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : non_unital_alg_hom R B A := -{ .. mul_hom.inverse (f : mul_hom A B) g h₁ h₂, - .. linear_map.inverse (f : A →ₗ[R] B) g h₁ h₂ } +{ .. (f : mul_hom A B).inverse g h₁ h₂, + .. (f : A →+[R] B).inverse g h₁ h₂ } @[simp] lemma coe_inverse (f : non_unital_alg_hom R A B) (g : B → A) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : From dc031481c66e55b7a9df4bfdd36a753dcfd82e45 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Wed, 9 Jun 2021 09:03:22 +0100 Subject: [PATCH 4/7] Golf and move `monoid_hom.inverse` --- src/algebra/group_action_hom.lean | 15 --------------- src/data/equiv/mul_add.lean | 8 ++++++++ 2 files changed, 8 insertions(+), 15 deletions(-) diff --git a/src/algebra/group_action_hom.lean b/src/algebra/group_action_hom.lean index 5f5e66e38a2f5..47e744c245fb5 100644 --- a/src/algebra/group_action_hom.lean +++ b/src/algebra/group_action_hom.lean @@ -115,21 +115,6 @@ def to_quotient : G →[G] quotient_group.quotient H := end mul_action_hom --- TODO Is this _really_ missing!!? Where should it go? -/-- The inverse of a bijective `monoid_hom` is a `monoid_hom`. -/ -@[to_additive "The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`."] -def monoid_hom.inverse {A B : Type*} [monoid A] [monoid B] (f : A →* B) (g : B → A) - (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : - B →* A := -{ to_fun := g, - map_one' := - calc g 1 = g (f 1) : by rw f.map_one - ... = 1 : by rw h₁, - map_mul' := λ x y, - calc g (x * y) = g ((f (g x)) * (f (g y))) : by rw [h₂, h₂] - ... = g (f ((g x) * (g y))) : by rw f.map_mul - ... = (g x) * (g y) : by rw h₁, } - /-- Equivariant additive monoid homomorphisms. -/ structure distrib_mul_action_hom extends A →[M] B, A →+ B. diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean index 634ad40d2061e..cad02aaa342f9 100644 --- a/src/data/equiv/mul_add.lean +++ b/src/data/equiv/mul_add.lean @@ -45,6 +45,14 @@ def mul_hom.inverse [has_mul M] [has_mul N] (f : mul_hom M N) (g : N → M) ... = g (f (g x * g y)) : by rw f.map_mul ... = g x * g y : h₁ _, } +/-- The inverse of a bijective `monoid_hom` is a `monoid_hom`. -/ +@[to_additive "The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`."] +def monoid_hom.inverse {A B : Type*} [monoid A] [monoid B] (f : A →* B) (g : B → A) + (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : + B →* A := +{ map_one' := show g 1 = 1, by rw [← f.map_one, h₁], + .. (f : mul_hom A B).inverse g h₁ h₂, } + set_option old_structure_cmd true /-- add_equiv α β is the type of an equiv α ≃ β which preserves addition. -/ From 880e44bc0b8f11151f7df2f40b3540633c407a40 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Wed, 9 Jun 2021 20:01:08 +0100 Subject: [PATCH 5/7] Drop addition of `non_unital_alg_hom.lean` The plan is to split this PR in two since the other changes are deep and cause long build times. --- src/algebra/non_unital_alg_hom.lean | 182 ---------------------------- 1 file changed, 182 deletions(-) delete mode 100644 src/algebra/non_unital_alg_hom.lean diff --git a/src/algebra/non_unital_alg_hom.lean b/src/algebra/non_unital_alg_hom.lean deleted file mode 100644 index a46642ff208bc..0000000000000 --- a/src/algebra/non_unital_alg_hom.lean +++ /dev/null @@ -1,182 +0,0 @@ -/- -Copyright (c) 2021 Oliver Nash. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Oliver Nash --/ -import algebra.algebra.basic - -/-! -# Morphisms of non-unital algebras - -This file defines morphisms between two types, each of which carries an addition, additive zero, -multiplication, and scalar action. The multiplications are not assumed to be associative or -unital, or even to be compatible with the scalar multiplications. In a typical application, the -operations will satisfy compatibility conditions making them into algebras (albeit possibly -non-associative and/or non-unital) but such conditions are not required to make this definition. - -## Main definitions - - * `non_unital_alg_hom` - * `alg_hom.to_non_unital_alg_hom` - -## Tags - -non-unital, algebra, morphism --/ - -universes u v w w₁ w₂ w₃ - -variables (R : Type u) (A : Type v) (B : Type w) (C : Type w₁) - -set_option old_structure_cmd true - -/-- A morphism respecting addition, multiplication, and scalar multiplication. When these arise from -algebra structures, this is the same as a not-necessarily-unital morphism of algebras. -/ -structure non_unital_alg_hom [monoid R] - [non_unital_non_assoc_semiring A] [distrib_mul_action R A] - [non_unital_non_assoc_semiring B] [distrib_mul_action R B] - extends A →+[R] B, mul_hom A B - -attribute [nolint doc_blame] non_unital_alg_hom.to_distrib_mul_action_hom -attribute [nolint doc_blame] non_unital_alg_hom.to_mul_hom - -initialize_simps_projections non_unital_alg_hom (to_fun → apply) - -namespace non_unital_alg_hom - -variables {R A B C} [semiring R] -variables [non_unital_non_assoc_semiring A] [module R A] -variables [non_unital_non_assoc_semiring B] [module R B] -variables [non_unital_non_assoc_semiring C] [module R C] - -/-- see Note [function coercion] -/ -instance : has_coe_to_fun (non_unital_alg_hom R A B) := ⟨_, to_fun⟩ - -@[simp] lemma to_fun_eq_coe (f : non_unital_alg_hom R A B) : f.to_fun = ⇑f := rfl - -lemma coe_injective : - @function.injective (non_unital_alg_hom R A B) (A → B) coe_fn := -by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr - -@[ext] lemma ext {f g : non_unital_alg_hom R A B} (h : ∀ x, f x = g x) : f = g := -coe_injective $ funext h - -lemma ext_iff {f g : non_unital_alg_hom R A B} : f = g ↔ ∀ x, f x = g x := -⟨by { rintro rfl x, refl }, ext⟩ - -@[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : - ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A → B) = f := -rfl - -@[simp] lemma mk_coe (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : - (⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) = f := -by { ext, refl, } - -instance : has_coe (non_unital_alg_hom R A B) (A →+[R] B) := -⟨to_distrib_mul_action_hom⟩ - -instance : has_coe (non_unital_alg_hom R A B) (mul_hom A B) := ⟨to_mul_hom⟩ - -@[simp] lemma to_distrib_mul_action_hom_eq_coe (f : non_unital_alg_hom R A B) : - f.to_distrib_mul_action_hom = ↑f := -rfl - -@[simp] lemma to_mul_hom_eq_coe (f : non_unital_alg_hom R A B) : f.to_mul_hom = ↑f := -rfl - -@[simp, norm_cast] lemma coe_to_distrib_mul_action_hom (f : non_unital_alg_hom R A B) : - ((f : A →+[R] B) : A → B) = f := -rfl - -@[simp, norm_cast] lemma coe_to_mul_hom (f : non_unital_alg_hom R A B) : - ((f : mul_hom A B) : A → B) = f := -rfl - -@[norm_cast] lemma coe_linear_map_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : - ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A →+[R] B) = - ⟨f, h₁, h₂, h₃⟩ := -by { ext, refl, } - -@[norm_cast] lemma coe_mul_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) : - ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : mul_hom A B) = ⟨f, h₄⟩ := -by { ext, refl, } - -@[simp] lemma map_smul (f : non_unital_alg_hom R A B) (c : R) (x : A) : - f (c • x) = c • f x := -f.to_distrib_mul_action_hom.map_smul c x - -@[simp] lemma map_add (f : non_unital_alg_hom R A B) (x y : A) : - f (x + y) = (f x) + (f y) := -f.to_distrib_mul_action_hom.map_add x y - -@[simp] lemma map_mul (f : non_unital_alg_hom R A B) (x y : A) : - f (x * y) = (f x) * (f y) := -f.to_mul_hom.map_mul x y - -@[simp] lemma map_zero (f : non_unital_alg_hom R A B) : f 0 = 0 := -f.to_distrib_mul_action_hom.map_zero - -instance : has_zero (non_unital_alg_hom R A B) := -⟨{ map_mul' := by simp, - .. (0 : A →+[R] B) }⟩ - -instance : has_one (non_unital_alg_hom R A A) := -⟨{ map_mul' := by simp, - .. (1 : A →+[R] A) }⟩ - -@[simp] lemma coe_zero : ((0 : non_unital_alg_hom R A B) : A → B) = 0 := rfl - -@[simp] lemma coe_one : ((1 : non_unital_alg_hom R A A) : A → A) = id := rfl - -lemma zero_apply (a : A) : (0 : non_unital_alg_hom R A B) a = 0 := rfl - -lemma one_apply (a : A) : (1 : non_unital_alg_hom R A A) a = a := rfl - -instance : inhabited (non_unital_alg_hom R A B) := ⟨0⟩ - -/-- The composition of morphisms is a morphism. -/ -def comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : non_unital_alg_hom R A C := -{ .. (f : mul_hom B C).comp (g : mul_hom A B), - .. (f : B →+[R] C).comp (g : A →+[R] B) } - -@[simp, norm_cast] lemma coe_comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : - (f.comp g : A → C) = (f : B → C) ∘ (g : A → B) := -rfl - -lemma comp_apply (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) (x : A) : - f.comp g x = f (g x) := -rfl - -/-- The inverse of a bijective morphism is a morphism. -/ -def inverse (f : non_unital_alg_hom R A B) (g : B → A) - (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : - non_unital_alg_hom R B A := -{ .. (f : mul_hom A B).inverse g h₁ h₂, - .. (f : A →+[R] B).inverse g h₁ h₂ } - -@[simp] lemma coe_inverse (f : non_unital_alg_hom R A B) (g : B → A) - (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : - (inverse f g h₁ h₂ : B → A) = g := -rfl - -end non_unital_alg_hom - -namespace alg_hom - -variables {R A B} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] - -/-- A unital morphism of algebras is a `non_unital_alg_hom`. -/ -def to_non_unital_alg_hom (f : A →ₐ[R] B) : non_unital_alg_hom R A B := -{ map_smul' := f.map_smul, .. f, } - -instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (non_unital_alg_hom R A B) := -⟨to_non_unital_alg_hom⟩ - -@[simp] lemma to_non_unital_alg_hom_eq_coe (f : A →ₐ[R] B) : f.to_non_unital_alg_hom = f := -rfl - -@[simp, norm_cast] lemma coe_to_non_unital_alg_hom (f : A →ₐ[R] B) : - ((f : non_unital_alg_hom R A B) : A → B) = f := -rfl - -end alg_hom From 1322b50f77d47cc82aab052da43a68cea08cd0df Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 10 Jun 2021 10:35:19 +0100 Subject: [PATCH 6/7] Define `distrib_mul_action_hom.has_one` via `id`. --- src/algebra/group_action_hom.lean | 34 +++++++++++++++---------------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/src/algebra/group_action_hom.lean b/src/algebra/group_action_hom.lean index 47e744c245fb5..989c5c733246a 100644 --- a/src/algebra/group_action_hom.lean +++ b/src/algebra/group_action_hom.lean @@ -150,24 +150,6 @@ variables {M A B} theorem ext_iff {f g : A →+[M] B} : f = g ↔ ∀ x, f x = g x := ⟨λ H x, by rw H, ext⟩ -instance : has_zero (A →+[M] B) := -⟨{ map_smul' := by simp, - .. (0 : A →+ B) }⟩ - -instance : has_one (A →+[M] A) := -⟨{ map_smul' := by simp, - .. add_monoid_hom.id A }⟩ - -@[simp] lemma coe_zero : ((0 : A →+[M] B) : A → B) = 0 := rfl - -@[simp] lemma coe_one : ((1 : A →+[M] A) : A → A) = id := rfl - -lemma zero_apply (a : A) : (0 : A →+[M] B) a = 0 := rfl - -lemma one_apply (a : A) : (1 : A →+[M] A) a = a := rfl - -instance : inhabited (A →+[M] B) := ⟨0⟩ - @[simp] lemma map_zero (f : A →+[M] B) : f 0 = 0 := f.map_zero' @@ -193,6 +175,22 @@ protected def id : A →+[M] A := variables {M A B C} +instance : has_zero (A →+[M] B) := +⟨{ map_smul' := by simp, + .. (0 : A →+ B) }⟩ + +instance : has_one (A →+[M] A) := ⟨distrib_mul_action_hom.id M⟩ + +@[simp] lemma coe_zero : ((0 : A →+[M] B) : A → B) = 0 := rfl + +@[simp] lemma coe_one : ((1 : A →+[M] A) : A → A) = id := rfl + +lemma zero_apply (a : A) : (0 : A →+[M] B) a = 0 := rfl + +lemma one_apply (a : A) : (1 : A →+[M] A) a = a := rfl + +instance : inhabited (A →+[M] B) := ⟨0⟩ + /-- Composition of two equivariant additive monoid homomorphisms. -/ def comp (g : B →+[M] C) (f : A →+[M] B) : A →+[M] C := { .. mul_action_hom.comp (g : B →[M] C) (f : A →[M] B), From 8c61bd645e71bc0fdad7893459034813325104d3 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 10 Jun 2021 15:16:59 +0100 Subject: [PATCH 7/7] Add simps decorators --- src/algebra/group_action_hom.lean | 7 ++++--- src/data/equiv/mul_add.lean | 5 +++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/algebra/group_action_hom.lean b/src/algebra/group_action_hom.lean index 989c5c733246a..98799e613a40b 100644 --- a/src/algebra/group_action_hom.lean +++ b/src/algebra/group_action_hom.lean @@ -96,7 +96,7 @@ ext $ λ x, by rw [comp_apply, id_apply] variables {A B} /-- The inverse of a bijective equivariant map is equivariant. -/ -def inverse (f : A →[M] B) (g : B → A) +@[simps] def inverse (f : A →[M] B) (g : B → A) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : B →[M] A := { to_fun := g, @@ -205,10 +205,11 @@ ext $ λ x, by rw [comp_apply, id_apply] ext $ λ x, by rw [comp_apply, id_apply] /-- The inverse of a bijective `distrib_mul_action_hom` is a `distrib_mul_action_hom`. -/ -def inverse (f : A →+[M] B) (g : B → A) +@[simps] def inverse (f : A →+[M] B) (g : B → A) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : B →+[M] A := -{ .. (f : A →+ B).inverse g h₁ h₂, +{ to_fun := g, + .. (f : A →+ B).inverse g h₁ h₂, .. (f : A →[M] B).inverse g h₁ h₂ } end distrib_mul_action_hom diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean index cad02aaa342f9..4701f976cf4a6 100644 --- a/src/data/equiv/mul_add.lean +++ b/src/data/equiv/mul_add.lean @@ -46,11 +46,12 @@ def mul_hom.inverse [has_mul M] [has_mul N] (f : mul_hom M N) (g : N → M) ... = g x * g y : h₁ _, } /-- The inverse of a bijective `monoid_hom` is a `monoid_hom`. -/ -@[to_additive "The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`."] +@[to_additive "The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`.", simps] def monoid_hom.inverse {A B : Type*} [monoid A] [monoid B] (f : A →* B) (g : B → A) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : B →* A := -{ map_one' := show g 1 = 1, by rw [← f.map_one, h₁], +{ to_fun := g, + map_one' := by rw [← f.map_one, h₁], .. (f : mul_hom A B).inverse g h₁ h₂, } set_option old_structure_cmd true