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 #
Units.map: Turn a homomorphism fromαtoβmonoids into a homomorphism fromαˣtoβˣ.MonoidHom.toHomUnits: Turn a homomorphism from a groupαtoβinto a homomorphism fromαtoβˣ.
TODO #
The results that don't mention homomorphisms should be proved (earlier?) in a different file and be
used to golf the basic Group lemmas.
theorem
IsAddUnit.eq_on_neg
{F : Type u_1}
{G : Type u_2}
{N : Type u_3}
[SubtractionMonoid G]
[AddMonoid N]
[AddMonoidHomClass F G N]
{x : G}
(hx : IsAddUnit x)
(f : F)
(g : F)
(h : ↑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]
[MonoidHomClass F G N]
{x : G}
(hx : IsUnit x)
(f : F)
(g : F)
(h : ↑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
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 =>
{ val := ↑f ↑u, neg := ↑f u.neg, val_neg := (_ : ↑f ↑u + ↑f u.neg = 0), neg_val := (_ : ↑f u.neg + ↑f ↑u = 0) })
(x + y) = (fun u =>
{ val := ↑f ↑u, neg := ↑f u.neg, val_neg := (_ : ↑f ↑u + ↑f u.neg = 0), neg_val := (_ : ↑f u.neg + ↑f ↑u = 0) })
x + (fun u =>
{ val := ↑f ↑u, neg := ↑f u.neg, val_neg := (_ : ↑f ↑u + ↑f u.neg = 0), neg_val := (_ : ↑f u.neg + ↑f ↑u = 0) })
y
@[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
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 (AddMonoidHom.comp g f) = AddMonoidHom.comp (AddUnits.map g) (AddUnits.map f)
@[simp]
@[simp]
@[simp]
theorem
AddUnits.coeHom_apply
{M : Type u}
[AddMonoid M]
(x : AddUnits M)
:
↑(AddUnits.coeHom M) x = ↑x
@[simp]
theorem
AddUnits.val_sub_eq_sub_val
{α : Type u_1}
[SubtractionMonoid α]
(u₁ : AddUnits α)
(u₂ : AddUnits α)
:
@[simp]
@[simp]
theorem
AddUnits.val_zsmul_eq_zsmul_val
{α : Type u_1}
[SubtractionMonoid α]
(u : AddUnits α)
(n : ℤ)
:
@[simp]
@[simp]
theorem
map_addUnits_neg
{α : Type u_1}
{M : Type u}
[AddMonoid M]
[SubtractionMonoid α]
{F : Type u_2}
[AddMonoidHomClass F M α]
(f : F)
(u : AddUnits M)
:
@[simp]
theorem
map_units_inv
{α : Type u_1}
{M : Type u}
[Monoid M]
[DivisionMonoid α]
{F : Type u_2}
[MonoidHomClass F M α]
(f : F)
(u : Mˣ)
:
theorem
AddUnits.liftRight.proof_2
{M : Type u_2}
{N : Type u_1}
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
(g : M → AddUnits N)
(h : ∀ (x : M), ↑(g x) = ↑f x)
(x : M)
(y : M)
:
ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } (x + y) = ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } x + ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } y
def
AddUnits.liftRight
{M : Type u}
{N : Type v}
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
(g : M → AddUnits 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
- One or more equations did not get rendered due to their size.
Instances For
def
Units.liftRight
{M : Type u}
{N : Type v}
[Monoid M]
[Monoid N]
(f : M →* N)
(g : M → Nˣ)
(h : ∀ (x : M), ↑(g x) = ↑f x)
:
If a map g : M → Nˣ agrees with a homomorphism f : M →* N, then
this map is a monoid homomorphism too.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
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 Mˣ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
AddMonoidHom.coe_toHomAddUnits
{G : Type u_1}
{M : Type u_2}
[AddGroup G]
[AddMonoid M]
(f : G →+ M)
(g : G)
:
↑(↑(AddMonoidHom.toHomAddUnits f) 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)
:
↑(↑(MonoidHom.toHomUnits f) g) = ↑f g
theorem
IsAddUnit.map
{F : Type u_1}
{M : Type u_4}
{N : Type u_5}
[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}
[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}
[AddMonoid M]
[AddMonoid N]
[AddMonoidHomClass F M 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}
[Monoid M]
[Monoid N]
[MonoidHomClass F M N]
[MonoidHomClass G N M]
{f : F}
{x : M}
(g : G)
(hfg : Function.LeftInverse ↑g ↑f)
(h : IsUnit (↑f x))
:
IsUnit x
theorem
isAddUnit_map_of_leftInverse
{F : Type u_1}
{G : Type u_2}
{M : Type u_4}
{N : Type u_5}
[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}
[Monoid M]
[Monoid N]
[MonoidHomClass F M N]
[MonoidHomClass G N M]
{f : F}
{x : M}
(g : G)
(hfg : Function.LeftInverse ↑g ↑f)
:
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
- IsAddUnit.liftRight f hf = AddUnits.liftRight f (fun x => IsAddUnit.addUnit (hf x)) (_ : ∀ (x : M), ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x)))
Instances For
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), ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x))
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))
:
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
- IsUnit.liftRight f hf = Units.liftRight f (fun x => IsUnit.unit (hf x)) (_ : ∀ (x : M), ↑(IsUnit.unit (hf x)) = ↑(IsUnit.unit (hf x)))
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
The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. As opposed to IsAddUnit.addUnit, the negation is
computable and comes from the negation on α. This is useful to transfer properties of negation
in AddUnits α to α. See also toAddUnits.
Equations
Instances For
@[simp]
theorem
IsUnit.val_unit'
{α : Type u_3}
[DivisionMonoid α]
{a : α}
(h : IsUnit a)
:
↑(IsUnit.unit' h) = a
@[simp]
theorem
IsAddUnit.val_addUnit'
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
↑(IsAddUnit.addUnit' h) = a
The element of the group of units, corresponding to an element of a monoid which is a unit. As
opposed to IsUnit.unit, the inverse is computable and comes from the inversion on α. This is
useful to transfer properties of inversion in Units α to α. See also toUnits.
Equations
Instances For
theorem
IsAddUnit.val_neg_addUnit'
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
↑(-IsAddUnit.addUnit' h) = -a
theorem
IsUnit.val_inv_unit'
{α : Type u_3}
[DivisionMonoid α]
{a : α}
(h : IsUnit a)
:
↑(IsUnit.unit' h)⁻¹ = a⁻¹
@[simp]
theorem
IsAddUnit.add_neg_cancel_left
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
@[simp]
theorem
IsUnit.mul_inv_cancel_left
{α : Type u_3}
[DivisionMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
@[simp]
theorem
IsAddUnit.neg_add_cancel_left
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
@[simp]
theorem
IsUnit.inv_mul_cancel_left
{α : Type u_3}
[DivisionMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
@[simp]
theorem
IsAddUnit.add_neg_cancel_right
{α : Type u_3}
[SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.mul_inv_cancel_right
{α : Type u_3}
[DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
@[simp]
theorem
IsAddUnit.neg_add_cancel_right
{α : Type u_3}
[SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.inv_mul_cancel_right
{α : Type u_3}
[DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
theorem
IsAddUnit.add_neg_eq_zero
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
theorem
IsAddUnit.neg_add_eq_zero
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsAddUnit.add_eq_zero_iff_eq_neg
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
theorem
IsUnit.mul_eq_one_iff_eq_inv
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
(h : IsUnit b)
:
theorem
IsAddUnit.add_eq_zero_iff_neg_eq
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsUnit.mul_eq_one_iff_inv_eq
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
(h : IsUnit a)
:
@[simp]
theorem
IsAddUnit.sub_add_cancel
{α : Type u_3}
[SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
@[simp]
theorem
IsAddUnit.add_sub_cancel
{α : Type u_3}
[SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsAddUnit.add_zero_sub_cancel
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
theorem
IsAddUnit.zero_sub_add_cancel
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
theorem
IsAddUnit.sub
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(ha : IsAddUnit a)
(hb : IsAddUnit b)
:
theorem
IsUnit.div
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
(ha : IsUnit a)
(hb : IsUnit b)
:
theorem
IsAddUnit.sub_left_inj
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit c)
:
theorem
IsUnit.div_left_inj
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit c)
:
theorem
IsAddUnit.sub_eq_iff
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit b)
:
theorem
IsUnit.div_eq_iff
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit b)
:
theorem
IsAddUnit.eq_sub_iff
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit c)
:
theorem
IsUnit.eq_div_iff
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit c)
:
theorem
IsAddUnit.sub_eq_of_eq_add
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit b)
:
theorem
IsUnit.div_eq_of_eq_mul
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit b)
:
theorem
IsAddUnit.eq_sub_of_add_eq
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit c)
:
theorem
IsUnit.eq_div_of_mul_eq
{α : Type u_3}
[DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit c)
:
theorem
IsAddUnit.sub_eq_zero_iff_eq
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
theorem
IsAddUnit.sub_add_left
{α : Type u_3}
[SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
The AddGroup version of this lemma is sub_add_cancel''
The Group version of this lemma is div_mul_cancel'''
theorem
IsAddUnit.add_sub_add_right
{α : Type u_3}
[SubtractionMonoid α]
{c : α}
(h : IsAddUnit c)
(a : α)
(b : α)
:
theorem
IsUnit.mul_div_mul_right
{α : Type u_3}
[DivisionMonoid α]
{c : α}
(h : IsUnit c)
(a : α)
(b : α)
:
theorem
IsAddUnit.add_add_sub
{α : Type u_3}
[SubtractionMonoid α]
{b : α}
(a : α)
(h : IsAddUnit b)
:
theorem
IsAddUnit.sub_add_right
{α : Type u_3}
[SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsAddUnit.add_sub_cancel_left
{α : Type u_3}
[SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsUnit.mul_div_cancel_left
{α : Type u_3}
[DivisionCommMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
theorem
IsAddUnit.add_sub_cancel'
{α : Type u_3}
[SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsUnit.mul_div_cancel'
{α : Type u_3}
[DivisionCommMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
theorem
IsAddUnit.add_sub_add_left
{α : Type u_3}
[SubtractionCommMonoid α]
{c : α}
(h : IsAddUnit c)
(a : α)
(b : α)
:
theorem
IsUnit.mul_div_mul_left
{α : Type u_3}
[DivisionCommMonoid α]
{c : α}
(h : IsUnit c)
(a : α)
(b : α)
:
theorem
IsAddUnit.sub_sub_cancel
{α : Type u_3}
[SubtractionCommMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsUnit.div_div_cancel
{α : Type u_3}
[DivisionCommMonoid α]
{a : α}
{b : α}
(h : IsUnit a)
:
theorem
IsAddUnit.sub_sub_cancel_left
{α : Type u_3}
[SubtractionCommMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsUnit.div_div_cancel_left
{α : Type u_3}
[DivisionCommMonoid α]
{a : α}
{b : α}
(h : IsUnit a)
: