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 an homomorphism fromαtoβmonoids into an homomorphism fromαˣtoβˣ.MonoidHom.toHomUnits: Turn an homomorphism from a groupαtoβinto an 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}
[inst : SubtractionMonoid G]
[inst : AddMonoid N]
[inst : 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}
[inst : DivisionMonoid G]
[inst : Monoid N]
[inst : 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⁻¹⁻¹.
def
AddUnits.map.proof_3
{M : Type u_1}
{N : Type u_2}
[inst : AddMonoid M]
[inst : 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
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AddUnits.map_comp
{M : Type u}
{N : Type v}
{P : Type w}
[inst : AddMonoid M]
[inst : AddMonoid N]
[inst : 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}
[inst : AddMonoid M]
(x : AddUnits M)
:
↑(AddUnits.coeHom M) x = ↑x
@[simp]
@[simp]
theorem
AddUnits.val_sub_eq_sub_val
{α : Type u_1}
[inst : SubtractionMonoid α]
(u₁ : AddUnits α)
(u₂ : AddUnits α)
:
@[simp]
@[simp]
theorem
AddUnits.val_zsmul_eq_zsmul_val
{α : Type u_1}
[inst : SubtractionMonoid α]
(u : AddUnits α)
(n : ℤ)
:
@[simp]
@[simp]
theorem
map_addUnits_neg
{α : Type u_2}
{M : Type u}
[inst : AddMonoid M]
[inst : SubtractionMonoid α]
{F : Type u_1}
[inst : AddMonoidHomClass F M α]
(f : F)
(u : AddUnits M)
:
@[simp]
theorem
map_units_inv
{α : Type u_2}
{M : Type u}
[inst : Monoid M]
[inst : DivisionMonoid α]
{F : Type u_1}
[inst : MonoidHomClass F M α]
(f : F)
(u : Mˣ)
:
def
AddUnits.liftRight.proof_2
{M : Type u_2}
{N : Type u_1}
[inst : AddMonoid M]
[inst : 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
Equations
- One or more equations did not get rendered due to their size.
def
AddUnits.liftRight
{M : Type u}
{N : Type v}
[inst : AddMonoid M]
[inst : AddMonoid N]
(f : M →+ N)
(g : M → AddUnits N)
(h : ∀ (x : M), ↑(g x) = ↑f x)
:
If a map g : M → AddUnits N→ AddUnits N agrees with a homomorphism f : M →+ N→+ N, then this map
is an AddMonoid homomorphism too.
Equations
- One or more equations did not get rendered due to their size.
def
Units.liftRight
{M : Type u}
{N : Type v}
[inst : Monoid M]
[inst : Monoid N]
(f : M →* N)
(g : M → Nˣ)
(h : ∀ (x : M), ↑(g x) = ↑f x)
:
If a map g : M → Nˣ→ Nˣ agrees with a homomorphism f : M →* N→* N, then
this map is a monoid homomorphism too.
Equations
- One or more equations did not get rendered due to their size.
def
AddMonoidHom.toHomAddUnits
{G : Type u_1}
{M : Type u_2}
[inst : AddGroup G]
[inst : 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.
def
MonoidHom.toHomUnits
{G : Type u_1}
{M : Type u_2}
[inst : Group G]
[inst : Monoid M]
(f : 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 Mˣ.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AddMonoidHom.coe_toHomAddUnits
{G : Type u_1}
{M : Type u_2}
[inst : AddGroup G]
[inst : 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}
[inst : Group G]
[inst : Monoid M]
(f : G →* M)
(g : G)
:
↑(↑(MonoidHom.toHomUnits f) g) = ↑f g
theorem
IsAddUnit.of_leftInverse
{F : Type u_1}
{G : Type u_4}
{M : Type u_2}
{N : Type u_3}
[inst : AddMonoid M]
[inst : AddMonoid N]
[inst : AddMonoidHomClass F M N]
[inst : 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_4}
{M : Type u_2}
{N : Type u_3}
[inst : Monoid M]
[inst : Monoid N]
[inst : MonoidHomClass F M N]
[inst : 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_4}
{M : Type u_2}
{N : Type u_3}
[inst : AddMonoid M]
[inst : AddMonoid N]
[inst : AddMonoidHomClass F M N]
[inst : 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_4}
{M : Type u_2}
{N : Type u_3}
[inst : Monoid M]
[inst : Monoid N]
[inst : MonoidHomClass F M N]
[inst : MonoidHomClass G N M]
{f : F}
{x : M}
(g : G)
(hfg : Function.LeftInverse ↑g ↑f)
:
noncomputable def
IsAddUnit.liftRight
{M : Type u_1}
{N : Type u_2}
[inst : AddMonoid M]
[inst : AddMonoid N]
(f : M →+ N)
(hf : ∀ (x : M), IsAddUnit (↑f x))
:
If a homomorphism f : M →+ N→+ N sends each element to an IsAddUnit, then it can be
lifted to f : M →+ AddUnits N→+ 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)))
def
IsAddUnit.liftRight.proof_1
{M : Type u_2}
{N : Type u_1}
[inst : AddMonoid M]
[inst : AddMonoid N]
(f : M →+ N)
(hf : ∀ (x : M), IsAddUnit (↑f x))
:
∀ (x : M), ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x))
Equations
- (_ : ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x))) = (_ : ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x)))
noncomputable def
IsUnit.liftRight
{M : Type u_1}
{N : Type u_2}
[inst : Monoid M]
[inst : Monoid N]
(f : M →* N)
(hf : ∀ (x : M), IsUnit (↑f x))
:
If a homomorphism f : M →* N→* N sends each element to an IsUnit, then it can be lifted
to f : M →* Nˣ→* 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)))
def
IsAddUnit.addUnit'
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
AddUnits α
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.
@[simp]
theorem
IsAddUnit.addUnit'_neg
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
(IsAddUnit.addUnit' h).neg = -a
@[simp]
theorem
IsUnit.unit'_val
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
(h : IsUnit a)
:
↑(IsUnit.unit' h) = a
@[simp]
theorem
IsUnit.unit'_inv
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
(h : IsUnit a)
:
(IsUnit.unit' h).inv = a⁻¹
@[simp]
theorem
IsAddUnit.addUnit'_val
{α : Type u_1}
[inst : 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.
@[simp]
theorem
IsAddUnit.add_neg_cancel_left
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
@[simp]
theorem
IsUnit.mul_inv_cancel_left
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
@[simp]
theorem
IsAddUnit.neg_add_cancel_left
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
@[simp]
theorem
IsUnit.inv_mul_cancel_left
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
@[simp]
theorem
IsAddUnit.add_neg_cancel_right
{α : Type u_1}
[inst : SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.mul_inv_cancel_right
{α : Type u_1}
[inst : DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
@[simp]
theorem
IsAddUnit.neg_add_cancel_right
{α : Type u_1}
[inst : SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.inv_mul_cancel_right
{α : Type u_1}
[inst : DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
@[simp]
theorem
IsAddUnit.sub_add_cancel
{α : Type u_1}
[inst : SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.div_mul_cancel
{α : Type u_1}
[inst : DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
@[simp]
theorem
IsAddUnit.add_sub_cancel
{α : Type u_1}
[inst : SubtractionMonoid α]
{b : α}
(h : IsAddUnit b)
(a : α)
:
@[simp]
theorem
IsUnit.mul_div_cancel
{α : Type u_1}
[inst : DivisionMonoid α]
{b : α}
(h : IsUnit b)
(a : α)
:
theorem
IsAddUnit.add_zero_sub_cancel
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
theorem
IsAddUnit.zero_sub_add_cancel
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
(h : IsAddUnit a)
:
theorem
IsAddUnit.sub
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
{b : α}
(ha : IsAddUnit a)
(hb : IsAddUnit b)
:
theorem
IsUnit.div
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
{b : α}
(ha : IsUnit a)
(hb : IsUnit b)
:
theorem
IsAddUnit.sub_eq_of_eq_add
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit b)
:
theorem
IsUnit.div_eq_of_eq_mul
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit b)
:
theorem
IsAddUnit.eq_sub_of_add_eq
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsAddUnit c)
:
theorem
IsUnit.eq_div_of_mul_eq
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
{b : α}
{c : α}
(h : IsUnit c)
:
theorem
IsAddUnit.sub_eq_zero_iff_eq
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
theorem
IsUnit.div_eq_one_iff_eq
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
{b : α}
(h : IsUnit b)
:
theorem
IsAddUnit.sub_add_left
{α : Type u_1}
[inst : SubtractionMonoid α]
{a : α}
{b : α}
(h : IsAddUnit b)
:
theorem
IsUnit.div_mul_left
{α : Type u_1}
[inst : DivisionMonoid α]
{a : α}
{b : α}
(h : IsUnit b)
:
theorem
IsAddUnit.add_add_sub
{α : Type u_1}
[inst : SubtractionMonoid α]
{b : α}
(a : α)
(h : IsAddUnit b)
:
theorem
IsUnit.mul_mul_div
{α : Type u_1}
[inst : DivisionMonoid α]
{b : α}
(a : α)
(h : IsUnit b)
:
theorem
IsAddUnit.sub_add_right
{α : Type u_1}
[inst : SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsUnit.div_mul_right
{α : Type u_1}
[inst : DivisionCommMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
theorem
IsAddUnit.add_sub_cancel_left
{α : Type u_1}
[inst : SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsUnit.mul_div_cancel_left
{α : Type u_1}
[inst : DivisionCommMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
theorem
IsAddUnit.add_sub_cancel'
{α : Type u_1}
[inst : SubtractionCommMonoid α]
{a : α}
(h : IsAddUnit a)
(b : α)
:
theorem
IsUnit.mul_div_cancel'
{α : Type u_1}
[inst : DivisionCommMonoid α]
{a : α}
(h : IsUnit a)
(b : α)
:
theorem
IsAddUnit.sub_sub_cancel
{α : Type u_1}
[inst : SubtractionCommMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsUnit.div_div_cancel
{α : Type u_1}
[inst : DivisionCommMonoid α]
{a : α}
{b : α}
(h : IsUnit a)
:
theorem
IsAddUnit.sub_sub_cancel_left
{α : Type u_1}
[inst : SubtractionCommMonoid α]
{a : α}
{b : α}
(h : IsAddUnit a)
:
theorem
IsUnit.div_div_cancel_left
{α : Type u_1}
[inst : DivisionCommMonoid α]
{a : α}
{b : α}
(h : IsUnit a)
: