Documentation

Mathlib.Algebra.Group.Units.Hom

Monoid homomorphisms and units #

This file allows to lift monoid homomorphisms to group homomorphisms of their units subgroups. It also contains unrelated results about Units that depend on MonoidHom.

Main declarations #

theorem IsAddUnit.eq_on_neg {F : Type u_1} {G : Type u_2} {N : Type u_3} [SubtractionMonoid G] [AddMonoid N] [FunLike F G N] [AddMonoidHomClass F G N] {x : G} (hx : IsAddUnit x) (f : F) (g : F) (h : f x = g x) :
f (-x) = g (-x)

If two homomorphisms from a subtraction monoid to an additive monoid are equal at an additive unit x, then they are equal at -x.

theorem IsUnit.eq_on_inv {F : Type u_1} {G : Type u_2} {N : Type u_3} [DivisionMonoid G] [Monoid N] [FunLike F G N] [MonoidHomClass F G N] {x : G} (hx : IsUnit x) (f : F) (g : F) (h : f x = g x) :
f x⁻¹ = g x⁻¹

If two homomorphisms from a division monoid to a monoid are equal at a unit x, then they are equal at x⁻¹.

theorem eq_on_neg {F : Type u_1} {G : Type u_2} {M : Type u_3} [AddGroup G] [AddMonoid M] [FunLike F G M] [AddMonoidHomClass F G M] (f : F) (g : F) {x : G} (h : f x = g x) :
f (-x) = g (-x)

If two homomorphism from an additive group to an additive monoid are equal at x, then they are equal at -x.

theorem eq_on_inv {F : Type u_1} {G : Type u_2} {M : Type u_3} [Group G] [Monoid M] [FunLike F G M] [MonoidHomClass F G M] (f : F) (g : F) {x : G} (h : f x = g x) :
f x⁻¹ = g x⁻¹

If two homomorphism from a group to a monoid are equal at x, then they are equal at x⁻¹.

theorem AddUnits.map.proof_3 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddUnits M) (y : AddUnits M) :
(fun (u : AddUnits M) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) (x + y) = (fun (u : AddUnits M) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) x + (fun (u : AddUnits M) => { val := f u, neg := f u.neg, val_neg := , neg_val := }) y
theorem AddUnits.map.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) :
f u.neg + f u = 0
theorem AddUnits.map.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) :
f u + f u.neg = 0
def AddUnits.map {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) :

The additive homomorphism on AddUnits induced by an AddMonoidHom.

Equations
Instances For
    def Units.map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) :

    The group homomorphism on units induced by a MonoidHom.

    Equations
    Instances For
      @[simp]
      theorem AddUnits.coe_map {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddUnits M) :
      ((AddUnits.map f) x) = f x
      @[simp]
      theorem Units.coe_map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (x : Mˣ) :
      ((Units.map f) x) = f x
      @[simp]
      theorem AddUnits.coe_map_neg {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (u : AddUnits M) :
      (-(AddUnits.map f) u) = f (-u)
      @[simp]
      theorem Units.coe_map_inv {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (u : Mˣ) :
      ((Units.map f) u)⁻¹ = f u⁻¹
      @[simp]
      theorem AddUnits.map_comp {M : Type u} {N : Type v} {P : Type w} [AddMonoid M] [AddMonoid N] [AddMonoid P] (f : M →+ N) (g : N →+ P) :
      AddUnits.map (g.comp f) = (AddUnits.map g).comp (AddUnits.map f)
      @[simp]
      theorem Units.map_comp {M : Type u} {N : Type v} {P : Type w} [Monoid M] [Monoid N] [Monoid P] (f : M →* N) (g : N →* P) :
      Units.map (g.comp f) = (Units.map g).comp (Units.map f)
      theorem Units.map_injective {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} (hf : Function.Injective f) :

      Coercion AddUnits M → M as an AddMonoid homomorphism.

      Equations
      • AddUnits.coeHom M = { toFun := AddUnits.val, map_zero' := , map_add' := }
      Instances For
        def Units.coeHom (M : Type u) [Monoid M] :
        Mˣ →* M

        Coercion Mˣ → M as a monoid homomorphism.

        Equations
        • Units.coeHom M = { toFun := Units.val, map_one' := , map_mul' := }
        Instances For
          @[simp]
          theorem AddUnits.coeHom_apply {M : Type u} [AddMonoid M] (x : AddUnits M) :
          (AddUnits.coeHom M) x = x
          @[simp]
          theorem Units.coeHom_apply {M : Type u} [Monoid M] (x : Mˣ) :
          (Units.coeHom M) x = x
          @[simp]
          theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} [SubtractionMonoid α] (u : AddUnits α) (n : ) :
          (n u) = n u
          @[simp]
          theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [DivisionMonoid α] (u : αˣ) (n : ) :
          (u ^ n) = u ^ n
          @[simp]
          theorem map_addUnits_neg {α : Type u_1} {M : Type u} [AddMonoid M] [SubtractionMonoid α] {F : Type u_2} [FunLike F M α] [AddMonoidHomClass F M α] (f : F) (u : AddUnits M) :
          f (-u) = -f u
          @[simp]
          theorem map_units_inv {α : Type u_1} {M : Type u} [Monoid M] [DivisionMonoid α] {F : Type u_2} [FunLike F M α] [MonoidHomClass F M α] (f : F) (u : Mˣ) :
          f u⁻¹ = (f u)⁻¹
          def AddUnits.liftRight {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : MAddUnits N) (h : ∀ (x : M), (g x) = f x) :

          If a map g : M → AddUnits N agrees with a homomorphism f : M →+ N, then this map is an AddMonoid homomorphism too.

          Equations
          Instances For
            theorem AddUnits.liftRight.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : MAddUnits N) (h : ∀ (x : M), (g x) = f x) (x : M) (y : M) :
            { toFun := g, map_zero' := }.toFun (x + y) = { toFun := g, map_zero' := }.toFun x + { toFun := g, map_zero' := }.toFun y
            theorem AddUnits.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (g : MAddUnits N) (h : ∀ (x : M), (g x) = f x) :
            g 0 = 0
            def Units.liftRight {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) (g : MNˣ) (h : ∀ (x : M), (g x) = f x) :
            M →* Nˣ

            If a map g : M → Nˣ agrees with a homomorphism f : M →* N, then this map is a monoid homomorphism too.

            Equations
            Instances For
              @[simp]
              theorem AddUnits.coe_liftRight {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), (g x) = f x) (x : M) :
              ((AddUnits.liftRight f g h) x) = f x
              @[simp]
              theorem Units.coe_liftRight {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
              ((Units.liftRight f g h) x) = f x
              @[simp]
              theorem AddUnits.add_liftRight_neg {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), (g x) = f x) (x : M) :
              f x + (-(AddUnits.liftRight f g h) x) = 0
              @[simp]
              theorem Units.mul_liftRight_inv {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
              f x * ((Units.liftRight f g h) x)⁻¹ = 1
              @[simp]
              theorem AddUnits.liftRight_neg_add {M : Type u} {N : Type v} [AddMonoid M] [AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), (g x) = f x) (x : M) :
              (-(AddUnits.liftRight f g h) x) + f x = 0
              @[simp]
              theorem Units.liftRight_inv_mul {M : Type u} {N : Type v} [Monoid M] [Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), (g x) = f x) (x : M) :
              ((Units.liftRight f g h) x)⁻¹ * f x = 1
              theorem AddMonoidHom.toHomAddUnits.proof_3 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (f : G →+ M) :
              ∀ (x : G), ((fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := }) x) = ((fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := }) x)
              def AddMonoidHom.toHomAddUnits {G : Type u_1} {M : Type u_2} [AddGroup G] [AddMonoid M] (f : G →+ M) :

              If f is a homomorphism from an additive group G to an additive monoid M, then its image lies in the AddUnits of M, and f.toHomUnits is the corresponding homomorphism from G to AddUnits M.

              Equations
              • f.toHomAddUnits = AddUnits.liftRight f (fun (g : G) => { val := f g, neg := f (-g), val_neg := , neg_val := })
              Instances For
                theorem AddMonoidHom.toHomAddUnits.proof_2 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) :
                f (-g) + f g = 0
                theorem AddMonoidHom.toHomAddUnits.proof_1 {G : Type u_2} {M : Type u_1} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) :
                f g + f (-g) = 0
                def MonoidHom.toHomUnits {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] (f : G →* M) :
                G →* Mˣ

                If f is a homomorphism from a group G to a monoid M, then its image lies in the units of M, and f.toHomUnits is the corresponding monoid homomorphism from G to .

                Equations
                • f.toHomUnits = Units.liftRight f (fun (g : G) => { val := f g, inv := f g⁻¹, val_inv := , inv_val := })
                Instances For
                  @[simp]
                  theorem AddMonoidHom.coe_toHomAddUnits {G : Type u_1} {M : Type u_2} [AddGroup G] [AddMonoid M] (f : G →+ M) (g : G) :
                  (f.toHomAddUnits g) = f g
                  @[simp]
                  theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] (f : G →* M) (g : G) :
                  (f.toHomUnits g) = f g
                  theorem IsAddUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [FunLike F M N] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x) :
                  IsAddUnit (f x)
                  theorem IsUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [FunLike F M N] [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) :
                  IsUnit (f x)
                  theorem IsAddUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) (h : IsAddUnit (f x)) :
                  theorem IsUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [Monoid M] [Monoid N] [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) :
                  theorem isAddUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [AddMonoid M] [AddMonoid N] [AddMonoidHomClass F M N] [AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
                  theorem isUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [FunLike F M N] [FunLike G N M] [Monoid M] [Monoid N] [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
                  IsUnit (f x) IsUnit x
                  theorem IsAddUnit.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
                  ∀ (x : M), .addUnit = .addUnit
                  noncomputable def IsAddUnit.liftRight {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :

                  If a homomorphism f : M →+ N sends each element to an IsAddUnit, then it can be lifted to f : M →+ AddUnits N. See also AddUnits.liftRight for a computable version.

                  Equations
                  Instances For
                    noncomputable def IsUnit.liftRight {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) :
                    M →* Nˣ

                    If a homomorphism f : M →* N sends each element to an IsUnit, then it can be lifted to f : M →* Nˣ. See also Units.liftRight for a computable version.

                    Equations
                    Instances For
                      theorem IsAddUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) (x : M) :
                      ((IsAddUnit.liftRight f hf) x) = f x
                      theorem IsUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) (x : M) :
                      ((IsUnit.liftRight f hf) x) = f x
                      @[simp]
                      theorem IsAddUnit.add_liftRight_neg {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
                      f x + (-(IsAddUnit.liftRight f h) x) = 0
                      @[simp]
                      theorem IsUnit.mul_liftRight_inv {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
                      f x * ((IsUnit.liftRight f h) x)⁻¹ = 1
                      @[simp]
                      theorem IsAddUnit.liftRight_neg_add {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
                      (-(IsAddUnit.liftRight f h) x) + f x = 0
                      @[simp]
                      theorem IsUnit.liftRight_inv_mul {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
                      ((IsUnit.liftRight f h) x)⁻¹ * f x = 1