Documentation

Mathlib.GroupTheory.Congruence.Opposite

Congruences on the opposite of a group #

This file defines the order isomorphism between the congruences on a group G and the congruences on the opposite group Gᵒᵖ.

source
def Con.op {M : Type u_1} [Mul M] (c : Con M) :
Con Mᵐᵒᵖ

If c is a multiplicative congruence on M, then (a, b) ↦ c b.unop a.unop is a multiplicative congruence on Mᵐᵒᵖ.

Equations
    Instances For
      source
      def AddCon.op {M : Type u_1} [Add M] (c : AddCon M) :
      AddCon Mᵃᵒᵖ

      If c is an additive congruence on M, then (a, b) ↦ c b.unop a.unop is an additive congruence on Mᵃᵒᵖ

      Equations
        Instances For
          source
          def Con.unop {M : Type u_1} [Mul M] (c : Con Mᵐᵒᵖ) :
          Con M

          If c is a multiplicative congruence on Mᵐᵒᵖ, then (a, b) ↦ c bᵒᵖ aᵒᵖ is a multiplicative congruence on M.

          Equations
            Instances For
              source
              def AddCon.unop {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) :
              AddCon M

              If c is an additive congruence on Mᵃᵒᵖ, then (a, b) ↦ c bᵒᵖ aᵒᵖ is an additive congruence on M

              Equations
                Instances For
                  source
                  def Con.orderIsoOp {M : Type u_1} [Mul M] :
                  Con M ≃o Con Mᵐᵒᵖ

                  The multiplicative congruences on M bijects to the multiplicative congruences on Mᵐᵒᵖ

                  Equations
                    Instances For
                      source
                      def AddCon.orderIsoOp {M : Type u_1} [Add M] :
                      AddCon M ≃o AddCon Mᵃᵒᵖ

                      The additive congruences on M bijects to the additive congruences on Mᵃᵒᵖ

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem Con.orderIsoOp_apply {M : Type u_1} [Mul M] (c : Con M) :
                          orderIsoOp c = c.op
                          source
                          @[simp]
                          theorem Con.orderIsoOp_symm_apply {M : Type u_1} [Mul M] (c : Con Mᵐᵒᵖ) :
                          (RelIso.symm orderIsoOp) c = c.unop
                          source
                          @[simp]
                          theorem AddCon.orderIsoOp_symm_apply {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) :
                          (RelIso.symm orderIsoOp) c = c.unop
                          source
                          @[simp]
                          theorem AddCon.orderIsoOp_apply {M : Type u_1} [Add M] (c : AddCon M) :
                          orderIsoOp c = c.op