Documentation

Mathlib.GroupTheory.Congruence.Hom

Congruence relations and homomorphisms #

This file contains elementary definitions involving congruence relations and morphisms.

Main definitions #

Tags #

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid

def AddCon.ker {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) :

The kernel of an AddMonoid homomorphism as an additive congruence relation.

Equations
Instances For
    def Con.ker {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) :
    Con M

    The kernel of a monoid homomorphism as a congruence relation.

    Equations
    Instances For
      @[simp]
      theorem AddCon.ker_rel {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) {x : M} {y : M} :
      (AddCon.ker f) x y f x = f y

      The definition of the additive congruence relation defined by an AddMonoid homomorphism's kernel.

      @[simp]
      theorem Con.ker_rel {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) {x : M} {y : M} :
      (Con.ker f) x y f x = f y

      The definition of the congruence relation defined by a monoid homomorphism's kernel.

      def AddCon.mk' {M : Type u_1} [AddZeroClass M] (c : AddCon M) :
      M →+ c.Quotient

      The natural homomorphism from an AddMonoid to its quotient by an additive congruence relation.

      Equations
      • c.mk' = { toFun := AddCon.toQuotient, map_zero' := , map_add' := }
      Instances For
        def Con.mk' {M : Type u_1} [MulOneClass M] (c : Con M) :
        M →* c.Quotient

        The natural homomorphism from a monoid to its quotient by a congruence relation.

        Equations
        • c.mk' = { toFun := Con.toQuotient, map_one' := , map_mul' := }
        Instances For
          @[simp]
          theorem AddCon.mk'_ker {M : Type u_1} [AddZeroClass M] (c : AddCon M) :
          AddCon.ker c.mk' = c

          The kernel of the natural homomorphism from an AddMonoid to its quotient by an additive congruence relation c equals c.

          @[simp]
          theorem Con.mk'_ker {M : Type u_1} [MulOneClass M] (c : Con M) :
          Con.ker c.mk' = c

          The kernel of the natural homomorphism from a monoid to its quotient by a congruence relation c equals c.

          theorem AddCon.mk'_surjective {M : Type u_1} [AddZeroClass M] {c : AddCon M} :

          The natural homomorphism from an AddMonoid to its quotient by a congruence relation is surjective.

          theorem Con.mk'_surjective {M : Type u_1} [MulOneClass M] {c : Con M} :

          The natural homomorphism from a monoid to its quotient by a congruence relation is surjective.

          @[simp]
          theorem AddCon.coe_mk' {M : Type u_1} [AddZeroClass M] {c : AddCon M} :
          c.mk' = AddCon.toQuotient
          @[simp]
          theorem Con.coe_mk' {M : Type u_1} [MulOneClass M] {c : Con M} :
          c.mk' = Con.toQuotient
          theorem AddCon.ker_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} {x : M} {y : M} :
          (AddCon.ker f) x y f x = f y
          theorem Con.ker_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} {x : M} {y : M} :
          (Con.ker f) x y f x = f y
          theorem AddCon.comap_eq {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {c : AddCon M} {f : N →+ M} :
          AddCon.comap f c = AddCon.ker (c.mk'.comp f)

          Given an AddMonoid homomorphism f : N → M and an additive congruence relation c on M, the additive congruence relation induced on N by f equals the kernel of c's quotient homomorphism composed with f.

          theorem Con.comap_eq {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {c : Con M} {f : N →* M} :
          Con.comap f c = Con.ker (c.mk'.comp f)

          Given a monoid homomorphism f : N → M and a congruence relation c on M, the congruence relation induced on N by f equals the kernel of c's quotient homomorphism composed with f.

          def AddCon.lift {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c AddCon.ker f) :
          c.Quotient →+ P

          The homomorphism on the quotient of an AddMonoid by an additive congruence relation c induced by a homomorphism constant on c's equivalence classes.

          Equations
          • c.lift f H = { toFun := fun (x : c.Quotient) => AddCon.liftOn x f , map_zero' := , map_add' := }
          Instances For
            def Con.lift {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (c : Con M) (f : M →* P) (H : c Con.ker f) :
            c.Quotient →* P

            The homomorphism on the quotient of a monoid by a congruence relation c induced by a homomorphism constant on c's equivalence classes.

            Equations
            • c.lift f H = { toFun := fun (x : c.Quotient) => Con.liftOn x f , map_one' := , map_mul' := }
            Instances For
              theorem AddCon.lift_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c AddCon.ker f) (x : M) :
              (c.lift f H) (c.mk' x) = f x

              The diagram describing the universal property for quotients of AddMonoids commutes.

              theorem Con.lift_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c Con.ker f) (x : M) :
              (c.lift f H) (c.mk' x) = f x

              The diagram describing the universal property for quotients of monoids commutes.

              @[simp]
              theorem AddCon.lift_coe {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c AddCon.ker f) (x : M) :
              (c.lift f H) x = f x

              The diagram describing the universal property for quotients of AddMonoids commutes.

              @[simp]
              theorem Con.lift_coe {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c Con.ker f) (x : M) :
              (c.lift f H) x = f x

              The diagram describing the universal property for quotients of monoids commutes.

              @[simp]
              theorem AddCon.lift_comp_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c AddCon.ker f) :
              (c.lift f H).comp c.mk' = f

              The diagram describing the universal property for quotients of AddMonoids commutes.

              @[simp]
              theorem Con.lift_comp_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c Con.ker f) :
              (c.lift f H).comp c.mk' = f

              The diagram describing the universal property for quotients of monoids commutes.

              @[simp]
              theorem AddCon.lift_apply_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} (f : c.Quotient →+ P) :
              c.lift (f.comp c.mk') = f

              Given a homomorphism f from the quotient of an AddMonoid by an additive congruence relation, f equals the homomorphism on the quotient induced by f composed with the natural map from the AddMonoid to the quotient.

              @[simp]
              theorem Con.lift_apply_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} (f : c.Quotient →* P) :
              c.lift (f.comp c.mk') = f

              Given a homomorphism f from the quotient of a monoid by a congruence relation, f equals the homomorphism on the quotient induced by f composed with the natural map from the monoid to the quotient.

              theorem AddCon.lift_funext {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} (f : c.Quotient →+ P) (g : c.Quotient →+ P) (h : ∀ (a : M), f a = g a) :
              f = g

              Homomorphisms on the quotient of an AddMonoid by an additive congruence relation are equal if they are equal on elements that are coercions from the AddMonoid.

              theorem Con.lift_funext {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} (f : c.Quotient →* P) (g : c.Quotient →* P) (h : ∀ (a : M), f a = g a) :
              f = g

              Homomorphisms on the quotient of a monoid by a congruence relation are equal if they are equal on elements that are coercions from the monoid.

              theorem AddCon.lift_unique {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c AddCon.ker f) (g : c.Quotient →+ P) (Hg : g.comp c.mk' = f) :
              g = c.lift f H

              The uniqueness part of the universal property for quotients of AddMonoids.

              theorem Con.lift_unique {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c Con.ker f) (g : c.Quotient →* P) (Hg : g.comp c.mk' = f) :
              g = c.lift f H

              The uniqueness part of the universal property for quotients of monoids.

              theorem AddCon.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (h : c AddCon.ker f) (hf : Function.Surjective f) :
              Function.Surjective (c.lift f h)

              Surjective AddMonoid homomorphisms constant on an additive congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

              theorem Con.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (h : c Con.ker f) (hf : Function.Surjective f) :
              Function.Surjective (c.lift f h)

              Surjective monoid homomorphisms constant on a congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

              theorem AddCon.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c AddCon.ker f) (h : Function.Injective (c.lift f H)) :

              Given an AddMonoid homomorphism f from M to P, the kernel of f is the unique additive congruence relation on M whose induced map from the quotient of M to P is injective.

              theorem Con.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (c : Con M) (f : M →* P) (H : c Con.ker f) (h : Function.Injective (c.lift f H)) :

              Given a monoid homomorphism f from M to P, the kernel of f is the unique congruence relation on M whose induced map from the quotient of M to P is injective.

              def AddCon.kerLift {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) :
              (AddCon.ker f).Quotient →+ P

              The homomorphism induced on the quotient of an AddMonoid by the kernel of an AddMonoid homomorphism.

              Equations
              Instances For
                def Con.kerLift {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) :
                (Con.ker f).Quotient →* P

                The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.

                Equations
                Instances For
                  @[simp]
                  theorem AddCon.kerLift_mk {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} (x : M) :
                  (AddCon.kerLift f) x = f x

                  The diagram described by the universal property for quotients of AddMonoids, when the additive congruence relation is the kernel of the homomorphism, commutes.

                  @[simp]
                  theorem Con.kerLift_mk {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} (x : M) :
                  (Con.kerLift f) x = f x

                  The diagram described by the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, commutes.

                  An AddMonoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

                  theorem Con.kerLift_injective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) :

                  A monoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

                  def AddCon.map {M : Type u_1} [AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c d) :
                  c.Quotient →+ d.Quotient

                  Given additive congruence relations c, d on an AddMonoid such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

                  Equations
                  • c.map d h = c.lift d.mk'
                  Instances For
                    def Con.map {M : Type u_1} [MulOneClass M] (c : Con M) (d : Con M) (h : c d) :
                    c.Quotient →* d.Quotient

                    Given congruence relations c, d on a monoid such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

                    Equations
                    • c.map d h = c.lift d.mk'
                    Instances For
                      theorem AddCon.map_apply {M : Type u_1} [AddZeroClass M] {c : AddCon M} {d : AddCon M} (h : c d) (x : c.Quotient) :
                      (c.map d h) x = (c.lift d.mk' ) x

                      Given additive congruence relations c, d on an AddMonoid such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

                      theorem Con.map_apply {M : Type u_1} [MulOneClass M] {c : Con M} {d : Con M} (h : c d) (x : c.Quotient) :
                      (c.map d h) x = (c.lift d.mk' ) x

                      Given congruence relations c, d on a monoid such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.