Documentation

Mathlib.Deprecated.Group

Unbundled monoid and group homomorphisms #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines predicates for unbundled monoid and group homomorphisms. Instead of using this file, please use MonoidHom, defined in Algebra.Hom.Group, with notation →*, for morphisms between monoids or groups. For example use φ : G →* H to represent a group homomorphism between multiplicative groups, and ψ : A →+ B to represent a group homomorphism between additive groups.

Main Definitions #

IsMonoidHom (deprecated), IsGroupHom (deprecated)

Tags #

IsGroupHom, IsMonoidHom

structure IsAddHom {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αβ) :

Predicate for maps which preserve an addition.

  • map_add : ∀ (x y : α), f (x + y) = f x + f y

    The proposition that f preserves addition.

Instances For
    theorem IsAddHom.map_add {α : Type u_1} {β : Type u_2} [Add α] [Add β] {f : αβ} (self : IsAddHom f) (x : α) (y : α) :
    f (x + y) = f x + f y

    The proposition that f preserves addition.

    structure IsMulHom {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] (f : αβ) :

    Predicate for maps which preserve a multiplication.

    • map_mul : ∀ (x y : α), f (x * y) = f x * f y

      The proposition that f preserves multiplication.

    Instances For
      theorem IsMulHom.map_mul {α : Type u_1} {β : Type u_2} [Mul α] [Mul β] {f : αβ} (self : IsMulHom f) (x : α) (y : α) :
      f (x * y) = f x * f y

      The proposition that f preserves multiplication.

      theorem IsAddHom.id {α : Type u} [Add α] :

      The identity map preserves addition

      theorem IsMulHom.id {α : Type u} [Mul α] :

      The identity map preserves multiplication.

      theorem IsAddHom.comp {α : Type u} {β : Type v} [Add α] [Add β] {γ : Type u_1} [Add γ] {f : αβ} {g : βγ} (hf : IsAddHom f) (hg : IsAddHom g) :

      The composition of addition preserving maps also preserves addition

      theorem IsMulHom.comp {α : Type u} {β : Type v} [Mul α] [Mul β] {γ : Type u_1} [Mul γ] {f : αβ} {g : βγ} (hf : IsMulHom f) (hg : IsMulHom g) :

      The composition of maps which preserve multiplication, also preserves multiplication.

      theorem IsAddHom.add {α : Type u_2} {β : Type u_3} [AddSemigroup α] [AddCommSemigroup β] {f : αβ} {g : αβ} (hf : IsAddHom f) (hg : IsAddHom g) :
      IsAddHom fun (a : α) => f a + g a

      A sum of maps which preserves addition, preserves addition when the target is commutative.

      theorem IsMulHom.mul {α : Type u_2} {β : Type u_3} [Semigroup α] [CommSemigroup β] {f : αβ} {g : αβ} (hf : IsMulHom f) (hg : IsMulHom g) :
      IsMulHom fun (a : α) => f a * g a

      A product of maps which preserve multiplication, preserves multiplication when the target is commutative.

      theorem IsAddHom.neg {α : Type u_2} {β : Type u_3} [Add α] [AddCommGroup β] {f : αβ} (hf : IsAddHom f) :
      IsAddHom fun (a : α) => -f a

      The negation of a map which preserves addition, preserves addition when the target is commutative.

      theorem IsMulHom.inv {α : Type u_2} {β : Type u_3} [Mul α] [CommGroup β] {f : αβ} (hf : IsMulHom f) :
      IsMulHom fun (a : α) => (f a)⁻¹

      The inverse of a map which preserves multiplication, preserves multiplication when the target is commutative.

      structure IsAddMonoidHom {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : αβ) extends IsAddHom :

      Predicate for additive monoid homomorphisms (deprecated -- use the bundled MonoidHom version).

      • map_add : ∀ (x y : α), f (x + y) = f x + f y
      • map_zero : f 0 = 0

        The proposition that f preserves the additive identity.

      Instances For
        theorem IsAddMonoidHom.map_zero {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] {f : αβ} (self : IsAddMonoidHom f) :
        f 0 = 0

        The proposition that f preserves the additive identity.

        structure IsMonoidHom {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : αβ) extends IsMulHom :

        Predicate for monoid homomorphisms (deprecated -- use the bundled MonoidHom version).

        • map_mul : ∀ (x y : α), f (x * y) = f x * f y
        • map_one : f 1 = 1

          The proposition that f preserves the multiplicative identity.

        Instances For
          theorem IsMonoidHom.map_one {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] {f : αβ} (self : IsMonoidHom f) :
          f 1 = 1

          The proposition that f preserves the multiplicative identity.

          theorem AddMonoidHom.of.proof_1 {M : Type u_2} {N : Type u_1} {mM : AddZeroClass M} {mN : AddZeroClass N} {f : MN} (h : IsAddMonoidHom f) (x : M) (y : M) :
          f (x + y) = f x + f y
          def AddMonoidHom.of {M : Type u_1} {N : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {f : MN} (h : IsAddMonoidHom f) :
          M →+ N

          Interpret a map f : M → N as a homomorphism M →+ N.

          Equations
          Instances For
            def MonoidHom.of {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} {f : MN} (h : IsMonoidHom f) :
            M →* N

            Interpret a map f : M → N as a homomorphism M →* N.

            Equations
            • MonoidHom.of h = { toFun := f, map_one' := , map_mul' := }
            Instances For
              @[simp]
              theorem AddMonoidHom.coe_of {M : Type u_1} {N : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {f : MN} (hf : IsAddMonoidHom f) :
              (AddMonoidHom.of hf) = f
              @[simp]
              theorem MonoidHom.coe_of {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} {f : MN} (hf : IsMonoidHom f) :
              (MonoidHom.of hf) = f
              theorem AddMonoidHom.isAddMonoidHom_coe {M : Type u_1} {N : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} (f : M →+ N) :
              theorem MonoidHom.isMonoidHom_coe {M : Type u_1} {N : Type u_2} {mM : MulOneClass M} {mN : MulOneClass N} (f : M →* N) :
              theorem AddEquiv.isAddHom {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :

              An additive isomorphism preserves addition (deprecated).

              theorem MulEquiv.isMulHom {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :

              A multiplicative isomorphism preserves multiplication (deprecated).

              theorem AddEquiv.isAddMonoidHom {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :

              An additive bijection between two additive monoids is an additive monoid hom (deprecated).

              theorem MulEquiv.isMonoidHom {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :

              A multiplicative bijection between two monoids is a monoid hom (deprecated -- use MulEquiv.toMonoidHom).

              theorem IsAddMonoidHom.map_add' {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] {f : αβ} (hf : IsAddMonoidHom f) (x : α) (y : α) :
              f (x + y) = f x + f y

              An additive monoid homomorphism preserves addition.

              theorem IsMonoidHom.map_mul' {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] {f : αβ} (hf : IsMonoidHom f) (x : α) (y : α) :
              f (x * y) = f x * f y

              A monoid homomorphism preserves multiplication.

              theorem IsAddMonoidHom.neg {α : Type u_1} {β : Type u_2} [AddZeroClass α] [AddCommGroup β] {f : αβ} (hf : IsAddMonoidHom f) :
              IsAddMonoidHom fun (a : α) => -f a

              The negation of a map which preserves addition, preserves addition when the target is commutative.

              theorem IsMonoidHom.inv {α : Type u_1} {β : Type u_2} [MulOneClass α] [CommGroup β] {f : αβ} (hf : IsMonoidHom f) :
              IsMonoidHom fun (a : α) => (f a)⁻¹

              The inverse of a map which preserves multiplication, preserves multiplication when the target is commutative.

              theorem IsAddHom.to_isAddMonoidHom {α : Type u} {β : Type v} [AddZeroClass α] [AddGroup β] {f : αβ} (hf : IsAddHom f) :

              A map to an additive group preserving addition is an additive monoid homomorphism.

              theorem IsMulHom.to_isMonoidHom {α : Type u} {β : Type v} [MulOneClass α] [Group β] {f : αβ} (hf : IsMulHom f) :

              A map to a group preserving multiplication is a monoid homomorphism.

              The identity map is an additive monoid homomorphism.

              theorem IsMonoidHom.id {α : Type u} [MulOneClass α] :

              The identity map is a monoid homomorphism.

              theorem IsAddMonoidHom.comp {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] {f : αβ} (hf : IsAddMonoidHom f) {γ : Type u_1} [AddZeroClass γ] {g : βγ} (hg : IsAddMonoidHom g) :

              The composite of two additive monoid homomorphisms is an additive monoid homomorphism.

              theorem IsMonoidHom.comp {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] {f : αβ} (hf : IsMonoidHom f) {γ : Type u_1} [MulOneClass γ] {g : βγ} (hg : IsMonoidHom g) :

              The composite of two monoid homomorphisms is a monoid homomorphism.

              theorem IsAddMonoidHom.isAddMonoidHom_mul_left {γ : Type u_1} [NonUnitalNonAssocSemiring γ] (x : γ) :
              IsAddMonoidHom fun (y : γ) => x * y

              Left multiplication in a ring is an additive monoid morphism.

              theorem IsAddMonoidHom.isAddMonoidHom_mul_right {γ : Type u_1} [NonUnitalNonAssocSemiring γ] (x : γ) :
              IsAddMonoidHom fun (y : γ) => y * x

              Right multiplication in a ring is an additive monoid morphism.

              structure IsAddGroupHom {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] (f : αβ) extends IsAddHom :

              Predicate for additive group homomorphism (deprecated -- use bundled MonoidHom).

                Instances For
                  structure IsGroupHom {α : Type u} {β : Type v} [Group α] [Group β] (f : αβ) extends IsMulHom :

                  Predicate for group homomorphisms (deprecated -- use bundled MonoidHom).

                    Instances For
                      theorem AddMonoidHom.isAddGroupHom {G : Type u_1} {H : Type u_2} :
                      ∀ {x : AddGroup G} {x_1 : AddGroup H} (f : G →+ H), IsAddGroupHom f
                      theorem MonoidHom.isGroupHom {G : Type u_1} {H : Type u_2} :
                      ∀ {x : Group G} {x_1 : Group H} (f : G →* H), IsGroupHom f
                      theorem AddEquiv.isAddGroupHom {G : Type u_1} {H : Type u_2} :
                      ∀ {x : AddGroup G} {x_1 : AddGroup H} (h : G ≃+ H), IsAddGroupHom h
                      theorem MulEquiv.isGroupHom {G : Type u_1} {H : Type u_2} :
                      ∀ {x : Group G} {x_1 : Group H} (h : G ≃* H), IsGroupHom h
                      theorem IsAddGroupHom.mk' {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : ∀ (x y : α), f (x + y) = f x + f y) :

                      Construct IsAddGroupHom from its only hypothesis.

                      theorem IsGroupHom.mk' {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : ∀ (x y : α), f (x * y) = f x * f y) :

                      Construct IsGroupHom from its only hypothesis.

                      theorem IsGroupHom.map_mul' {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) (x : α) (y : α) :
                      f (x * y) = f x * f y
                      theorem IsAddGroupHom.to_isAddMonoidHom {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) :

                      An additive group homomorphism is an additive monoid homomorphism.

                      theorem IsGroupHom.to_isMonoidHom {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) :

                      A group homomorphism is a monoid homomorphism.

                      theorem IsAddGroupHom.map_zero {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) :
                      f 0 = 0

                      An additive group homomorphism sends 0 to 0.

                      theorem IsGroupHom.map_one {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) :
                      f 1 = 1

                      A group homomorphism sends 1 to 1.

                      theorem IsAddGroupHom.map_neg {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) (a : α) :
                      f (-a) = -f a

                      An additive group homomorphism sends negations to negations.

                      theorem IsGroupHom.map_inv {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) (a : α) :
                      f a⁻¹ = (f a)⁻¹

                      A group homomorphism sends inverses to inverses.

                      theorem IsAddGroupHom.map_sub {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) (a : α) (b : α) :
                      f (a - b) = f a - f b
                      theorem IsGroupHom.map_div {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) (a : α) (b : α) :
                      f (a / b) = f a / f b
                      theorem IsAddGroupHom.id {α : Type u} [AddGroup α] :

                      The identity is an additive group homomorphism.

                      theorem IsGroupHom.id {α : Type u} [Group α] :

                      The identity is a group homomorphism.

                      theorem IsAddGroupHom.comp {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) {γ : Type u_1} [AddGroup γ] {g : βγ} (hg : IsAddGroupHom g) :

                      The composition of two additive group homomorphisms is an additive group homomorphism.

                      theorem IsGroupHom.comp {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) {γ : Type u_1} [Group γ] {g : βγ} (hg : IsGroupHom g) :

                      The composition of two group homomorphisms is a group homomorphism.

                      theorem IsAddGroupHom.injective_iff {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) :
                      Function.Injective f ∀ (a : α), f a = 0a = 0

                      An additive group homomorphism is injective if its kernel is trivial.

                      theorem IsGroupHom.injective_iff {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) :
                      Function.Injective f ∀ (a : α), f a = 1a = 1

                      A group homomorphism is injective iff its kernel is trivial.

                      theorem IsAddGroupHom.add {α : Type u_1} {β : Type u_2} [AddGroup α] [AddCommGroup β] {f : αβ} {g : αβ} (hf : IsAddGroupHom f) (hg : IsAddGroupHom g) :
                      IsAddGroupHom fun (a : α) => f a + g a

                      The sum of two additive group homomorphisms is an additive group homomorphism if the target is commutative.

                      theorem IsGroupHom.mul {α : Type u_1} {β : Type u_2} [Group α] [CommGroup β] {f : αβ} {g : αβ} (hf : IsGroupHom f) (hg : IsGroupHom g) :
                      IsGroupHom fun (a : α) => f a * g a

                      The product of group homomorphisms is a group homomorphism if the target is commutative.

                      theorem IsAddGroupHom.neg {α : Type u_1} {β : Type u_2} [AddGroup α] [AddCommGroup β] {f : αβ} (hf : IsAddGroupHom f) :
                      IsAddGroupHom fun (a : α) => -f a

                      The negation of an additive group homomorphism is an additive group homomorphism if the target is commutative.

                      theorem IsGroupHom.inv {α : Type u_1} {β : Type u_2} [Group α] [CommGroup β] {f : αβ} (hf : IsGroupHom f) :
                      IsGroupHom fun (a : α) => (f a)⁻¹

                      The inverse of a group homomorphism is a group homomorphism if the target is commutative.

                      These instances look redundant, because Deprecated.Ring provides IsRingHom for a →+*. Nevertheless these are harmless, and helpful for stripping out dependencies on Deprecated.Ring.

                      theorem RingHom.to_isMonoidHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) :
                      theorem RingHom.to_isAddGroupHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) :
                      theorem Neg.isAddGroupHom {α : Type u} [AddCommGroup α] :

                      Negation is an AddGroup homomorphism if the AddGroup is commutative.

                      theorem Inv.isGroupHom {α : Type u} [CommGroup α] :
                      IsGroupHom Inv.inv

                      Inversion is a group homomorphism if the group is commutative.

                      theorem IsAddGroupHom.sub {α : Type u_1} {β : Type u_2} [AddGroup α] [AddCommGroup β] {f : αβ} {g : αβ} (hf : IsAddGroupHom f) (hg : IsAddGroupHom g) :
                      IsAddGroupHom fun (a : α) => f a - g a

                      The difference of two additive group homomorphisms is an additive group homomorphism if the target is commutative.

                      @[reducible, inline]
                      abbrev Units.map' {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {f : MN} (hf : IsMonoidHom f) :

                      The group homomorphism on units induced by a multiplicative morphism.

                      Equations
                      Instances For
                        @[simp]
                        theorem Units.coe_map' {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {f : MN} (hf : IsMonoidHom f) (x : Mˣ) :
                        ((Units.map' hf) x) = f x
                        theorem Units.coe_isMonoidHom {M : Type u_1} [Monoid M] :
                        IsMonoidHom fun (x : Mˣ) => x
                        theorem IsUnit.map' {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {f : MN} (hf : IsMonoidHom f) {x : M} (h : IsUnit x) :
                        IsUnit (f x)
                        theorem Additive.isAddHom {α : Type u} {β : Type v} [Mul α] [Mul β] {f : αβ} (hf : IsMulHom f) :
                        theorem Multiplicative.isMulHom {α : Type u} {β : Type v} [Add α] [Add β] {f : αβ} (hf : IsAddHom f) :
                        theorem Additive.isAddMonoidHom {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] {f : αβ} (hf : IsMonoidHom f) :
                        theorem Multiplicative.isMonoidHom {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] {f : αβ} (hf : IsAddMonoidHom f) :
                        theorem Additive.isAddGroupHom {α : Type u} {β : Type v} [Group α] [Group β] {f : αβ} (hf : IsGroupHom f) :
                        theorem Multiplicative.isGroupHom {α : Type u} {β : Type v} [AddGroup α] [AddGroup β] {f : αβ} (hf : IsAddGroupHom f) :