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ᵒᵖ.

theorem AddCon.op.proof_1 {M : Type u_1} [Add M] (c : AddCon M) :
def AddCon.op {M : Type u_1} [Add M] (c : 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
    theorem AddCon.op.proof_2 {M : Type u_1} [Add M] (c : AddCon M) :
    def Con.op {M : Type u_1} [Mul M] (c : 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
      theorem AddCon.unop.proof_1 {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) :
      Equivalence fun (a b : M) => c (AddOpposite.op b) (AddOpposite.op a)
      def AddCon.unop {M : Type u_1} [Add M] (c : 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
        theorem AddCon.unop.proof_2 {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) :
        ∀ {w x y z : M}, Setoid.r w xSetoid.r y zc ({ unop' := z } + { unop' := x }) ({ unop' := y } + { unop' := w })
        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
          theorem AddCon.orderIsoOp.proof_3 {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
          { toFun := AddCon.op, invFun := AddCon.unop, left_inv := , right_inv := } c { toFun := AddCon.op, invFun := AddCon.unop, left_inv := , right_inv := } d c d
          theorem AddCon.orderIsoOp.proof_2 {M : Type u_1} [Add M] :
          ∀ (x : AddCon Mᵃᵒᵖ), x.unop.op = x.unop.op

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

          Equations
          • AddCon.orderIsoOp = { toFun := AddCon.op, invFun := AddCon.unop, left_inv := , right_inv := , map_rel_iff' := }
          Instances For
            theorem AddCon.orderIsoOp.proof_1 {M : Type u_1} [Add M] :
            ∀ (x : AddCon M), x.op.unop = x.op.unop
            @[simp]
            theorem Con.orderIsoOp_apply {M : Type u_1} [Mul M] (c : Con M) :
            Con.orderIsoOp c = c.op
            @[simp]
            theorem AddCon.orderIsoOp_symm_apply {M : Type u_1} [Add M] (c : AddCon Mᵃᵒᵖ) :
            (RelIso.symm AddCon.orderIsoOp) c = c.unop
            @[simp]
            theorem Con.orderIsoOp_symm_apply {M : Type u_1} [Mul M] (c : Con Mᵐᵒᵖ) :
            (RelIso.symm Con.orderIsoOp) c = c.unop
            @[simp]
            theorem AddCon.orderIsoOp_apply {M : Type u_1} [Add M] (c : AddCon M) :
            AddCon.orderIsoOp c = c.op
            def Con.orderIsoOp {M : Type u_1} [Mul M] :

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

            Equations
            • Con.orderIsoOp = { toFun := Con.op, invFun := Con.unop, left_inv := , right_inv := , map_rel_iff' := }
            Instances For