Documentation

Mathlib.Algebra.Group.Subsemigroup.Defs

Subsemigroups: definition #

This file defines bundled multiplicative and additive subsemigroups.

Main definitions #

For each of the following definitions in the Subsemigroup namespace, there is a corresponding definition in the AddSubsemigroup namespace.

Similarly, for each of these definitions in the MulHom namespace, there is a corresponding definition in the AddHom namespace.

Implementation notes #

Subsemigroup inclusion is denoted rather than , although is defined as membership of a subsemigroup's underlying set.

Note that Subsemigroup M does not actually require Semigroup M, instead requiring only the weaker Mul M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

Tags #

subsemigroup, subsemigroups

class MulMemClass (S : Type u_3) (M : outParam (Type u_4)) [Mul M] [SetLike S M] :

MulMemClass S M says S is a type of sets s : Set M that are closed under (*)

  • mul_mem : ∀ {s : S} {a b : M}, a sb sa * b s

    A substructure satisfying MulMemClass is closed under multiplication.

Instances
    theorem MulMemClass.mul_mem {S : Type u_3} {M : outParam (Type u_4)} :
    ∀ {inst : Mul M} {inst_1 : SetLike S M} [self : MulMemClass S M] {s : S} {a b : M}, a sb sa * b s

    A substructure satisfying MulMemClass is closed under multiplication.

    class AddMemClass (S : Type u_3) (M : outParam (Type u_4)) [Add M] [SetLike S M] :

    AddMemClass S M says S is a type of sets s : Set M that are closed under (+)

    • add_mem : ∀ {s : S} {a b : M}, a sb sa + b s

      A substructure satisfying AddMemClass is closed under addition.

    Instances
      theorem AddMemClass.add_mem {S : Type u_3} {M : outParam (Type u_4)} :
      ∀ {inst : Add M} {inst_1 : SetLike S M} [self : AddMemClass S M] {s : S} {a b : M}, a sb sa + b s

      A substructure satisfying AddMemClass is closed under addition.

      structure Subsemigroup (M : Type u_3) [Mul M] :
      Type u_3

      A subsemigroup of a magma M is a subset closed under multiplication.

      • carrier : Set M

        The carrier of a subsemigroup.

      • mul_mem' : ∀ {a b : M}, a self.carrierb self.carriera * b self.carrier

        The product of two elements of a subsemigroup belongs to the subsemigroup.

      Instances For
        theorem Subsemigroup.mul_mem' {M : Type u_3} [Mul M] (self : Subsemigroup M) {a : M} {b : M} :
        a self.carrierb self.carriera * b self.carrier

        The product of two elements of a subsemigroup belongs to the subsemigroup.

        structure AddSubsemigroup (M : Type u_3) [Add M] :
        Type u_3

        An additive subsemigroup of an additive magma M is a subset closed under addition.

        • carrier : Set M

          The carrier of an additive subsemigroup.

        • add_mem' : ∀ {a b : M}, a self.carrierb self.carriera + b self.carrier

          The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

        Instances For
          theorem AddSubsemigroup.add_mem' {M : Type u_3} [Add M] (self : AddSubsemigroup M) {a : M} {b : M} :
          a self.carrierb self.carriera + b self.carrier

          The sum of two elements of an additive subsemigroup belongs to the subsemigroup.

          Equations
          • AddSubsemigroup.instSetLike = { coe := AddSubsemigroup.carrier, coe_injective' := }
          instance Subsemigroup.instSetLike {M : Type u_1} [Mul M] :
          Equations
          • Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective' := }
          Equations
          • =
          Equations
          • =
          @[simp]
          theorem AddSubsemigroup.mem_carrier {M : Type u_1} [Add M] {s : AddSubsemigroup M} {x : M} :
          x s.carrier x s
          @[simp]
          theorem Subsemigroup.mem_carrier {M : Type u_1} [Mul M] {s : Subsemigroup M} {x : M} :
          x s.carrier x s
          @[simp]
          theorem AddSubsemigroup.mem_mk {M : Type u_1} [Add M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa + b s) :
          x { carrier := s, add_mem' := h_mul } x s
          @[simp]
          theorem Subsemigroup.mem_mk {M : Type u_1} [Mul M] {s : Set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa * b s) :
          x { carrier := s, mul_mem' := h_mul } x s
          @[simp]
          theorem AddSubsemigroup.coe_set_mk {M : Type u_1} [Add M] (s : Set M) (h_mul : ∀ {a b : M}, a sb sa + b s) :
          { carrier := s, add_mem' := h_mul } = s
          @[simp]
          theorem Subsemigroup.coe_set_mk {M : Type u_1} [Mul M] (s : Set M) (h_mul : ∀ {a b : M}, a sb sa * b s) :
          { carrier := s, mul_mem' := h_mul } = s
          @[simp]
          theorem AddSubsemigroup.mk_le_mk {M : Type u_1} [Add M] {s : Set M} {t : Set M} (h_mul : ∀ {a b : M}, a sb sa + b s) (h_mul' : ∀ {a b : M}, a tb ta + b t) :
          { carrier := s, add_mem' := h_mul } { carrier := t, add_mem' := h_mul' } s t
          @[simp]
          theorem Subsemigroup.mk_le_mk {M : Type u_1} [Mul M] {s : Set M} {t : Set M} (h_mul : ∀ {a b : M}, a sb sa * b s) (h_mul' : ∀ {a b : M}, a tb ta * b t) :
          { carrier := s, mul_mem' := h_mul } { carrier := t, mul_mem' := h_mul' } s t
          theorem AddSubsemigroup.ext {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : ∀ (x : M), x S x T) :
          S = T

          Two AddSubsemigroups are equal if they have the same elements.

          theorem AddSubsemigroup.ext_iff {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} :
          S = T ∀ (x : M), x S x T
          theorem Subsemigroup.ext_iff {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} :
          S = T ∀ (x : M), x S x T
          theorem Subsemigroup.ext {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : ∀ (x : M), x S x T) :
          S = T

          Two subsemigroups are equal if they have the same elements.

          def AddSubsemigroup.copy {M : Type u_1} [Add M] (S : AddSubsemigroup M) (s : Set M) (hs : s = S) :

          Copy an additive subsemigroup replacing carrier with a set that is equal to it.

          Equations
          • S.copy s hs = { carrier := s, add_mem' := }
          Instances For
            def Subsemigroup.copy {M : Type u_1} [Mul M] (S : Subsemigroup M) (s : Set M) (hs : s = S) :

            Copy a subsemigroup replacing carrier with a set that is equal to it.

            Equations
            • S.copy s hs = { carrier := s, mul_mem' := }
            Instances For
              @[simp]
              theorem AddSubsemigroup.coe_copy {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = S) :
              (S.copy s hs) = s
              @[simp]
              theorem Subsemigroup.coe_copy {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = S) :
              (S.copy s hs) = s
              theorem AddSubsemigroup.copy_eq {M : Type u_1} [Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = S) :
              S.copy s hs = S
              theorem Subsemigroup.copy_eq {M : Type u_1} [Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = S) :
              S.copy s hs = S
              theorem AddSubsemigroup.add_mem {M : Type u_1} [Add M] (S : AddSubsemigroup M) {x : M} {y : M} :
              x Sy Sx + y S

              An AddSubsemigroup is closed under addition.

              theorem Subsemigroup.mul_mem {M : Type u_1} [Mul M] (S : Subsemigroup M) {x : M} {y : M} :
              x Sy Sx * y S

              A subsemigroup is closed under multiplication.

              instance AddSubsemigroup.instTop {M : Type u_1} [Add M] :

              The additive subsemigroup M of the magma M.

              Equations
              • AddSubsemigroup.instTop = { top := { carrier := Set.univ, add_mem' := } }
              instance Subsemigroup.instTop {M : Type u_1} [Mul M] :

              The subsemigroup M of the magma M.

              Equations
              • Subsemigroup.instTop = { top := { carrier := Set.univ, mul_mem' := } }
              instance AddSubsemigroup.instBot {M : Type u_1} [Add M] :

              The trivial AddSubsemigroup of an additive magma M.

              Equations
              • AddSubsemigroup.instBot = { bot := { carrier := , add_mem' := } }
              instance Subsemigroup.instBot {M : Type u_1} [Mul M] :

              The trivial subsemigroup of a magma M.

              Equations
              • Subsemigroup.instBot = { bot := { carrier := , mul_mem' := } }
              Equations
              • AddSubsemigroup.instInhabited = { default := }
              Equations
              • Subsemigroup.instInhabited = { default := }
              theorem AddSubsemigroup.not_mem_bot {M : Type u_1} [Add M] {x : M} :
              x
              theorem Subsemigroup.not_mem_bot {M : Type u_1} [Mul M] {x : M} :
              x
              @[simp]
              theorem AddSubsemigroup.mem_top {M : Type u_1} [Add M] (x : M) :
              @[simp]
              theorem Subsemigroup.mem_top {M : Type u_1} [Mul M] (x : M) :
              @[simp]
              theorem AddSubsemigroup.coe_top {M : Type u_1} [Add M] :
              = Set.univ
              @[simp]
              theorem Subsemigroup.coe_top {M : Type u_1} [Mul M] :
              = Set.univ
              @[simp]
              theorem AddSubsemigroup.coe_bot {M : Type u_1} [Add M] :
              =
              @[simp]
              theorem Subsemigroup.coe_bot {M : Type u_1} [Mul M] :
              =
              instance AddSubsemigroup.instInf {M : Type u_1} [Add M] :

              The inf of two AddSubsemigroups is their intersection.

              Equations
              • AddSubsemigroup.instInf = { inf := fun (S₁ S₂ : AddSubsemigroup M) => { carrier := S₁ S₂, add_mem' := } }
              instance Subsemigroup.instInf {M : Type u_1} [Mul M] :

              The inf of two subsemigroups is their intersection.

              Equations
              • Subsemigroup.instInf = { inf := fun (S₁ S₂ : Subsemigroup M) => { carrier := S₁ S₂, mul_mem' := } }
              @[simp]
              theorem AddSubsemigroup.coe_inf {M : Type u_1} [Add M] (p : AddSubsemigroup M) (p' : AddSubsemigroup M) :
              (p p') = p p'
              @[simp]
              theorem Subsemigroup.coe_inf {M : Type u_1} [Mul M] (p : Subsemigroup M) (p' : Subsemigroup M) :
              (p p') = p p'
              @[simp]
              theorem AddSubsemigroup.mem_inf {M : Type u_1} [Add M] {p : AddSubsemigroup M} {p' : AddSubsemigroup M} {x : M} :
              x p p' x p x p'
              @[simp]
              theorem Subsemigroup.mem_inf {M : Type u_1} [Mul M] {p : Subsemigroup M} {p' : Subsemigroup M} {x : M} :
              x p p' x p x p'
              Equations
              • =
              Equations
              • =
              def AddHom.eqLocus {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : AddHom M N) :

              The additive subsemigroup of elements x : M such that f x = g x

              Equations
              • f.eqLocus g = { carrier := {x : M | f x = g x}, add_mem' := }
              Instances For
                def MulHom.eqLocus {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (g : M →ₙ* N) :

                The subsemigroup of elements x : M such that f x = g x

                Equations
                • f.eqLocus g = { carrier := {x : M | f x = g x}, mul_mem' := }
                Instances For
                  theorem AddHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn f g ) :
                  f = g
                  theorem MulHom.eq_of_eqOn_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn f g ) :
                  f = g