Submonoid of units

Given a submonoid S of a monoid M, we define the subgroup S.units as the units of S as a subgroup of Mˣ. That is to say, S.units contains all members of S which have a two-sided inverse within S, as terms of type Mˣ.

We also define, for subgroups S of Mˣ, S.ofUnits, which is S considered as a submonoid of M. Submonoid.units and Subgroup.ofUnits form a Galois coinsertion.

We also make the equivalent additive definitions.

Implementation details

There are a number of other constructions which are multiplicatively equivalent to S.units but which have a different type.

Definition	Type
S.units	Subgroup Mˣ
Sˣ	Type u
IsUnit.submonoid S	Submonoid S
S.units.ofUnits	Submonoid M

All of these are distinct from S.leftInv, which is the submonoid of M which contains every member of M with a right inverse in S.

def AddSubmonoid.addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubgroup (AddUnits M)

The additive units of S, packaged as an additive subgroup of AddUnits M.

Equations

• S.addUnits = { toAddSubmonoid := AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S, neg_mem' := ⋯ }

theorem AddSubmonoid.addUnits.proof_1 {M : Type u_1} [AddMonoid M] : AddMonoidHomClass (AddUnits M →+ M) (AddUnits M) M

theorem AddSubmonoid.addUnits.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ {x : AddUnits M}, x ∈ (AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S).carrier → -x ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) S) ∧ -x ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) S)

def Submonoid.units {M : Type u_1} [Monoid M] (S : Submonoid M) : Subgroup Mˣ

The units of S, packaged as a subgroup of Mˣ.

Equations

• S.units = { toSubmonoid := Submonoid.comap (Units.coeHom M) S ⊓ (Submonoid.comap (Units.coeHom M) S)⁻¹, inv_mem' := ⋯ }

def AddSubgroup.ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : AddSubmonoid M

A additive subgroup of additive units represented as a additive submonoid of M.

Equations

• S.ofAddUnits = AddSubmonoid.map (AddUnits.coeHom M) S.toAddSubmonoid

theorem AddSubgroup.ofAddUnits.proof_1 {M : Type u_1} [AddMonoid M] : AddMonoidHomClass (AddUnits M →+ M) (AddUnits M) M

def Subgroup.ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) : Submonoid M

A subgroup of units represented as a submonoid of M.

Equations

• S.ofUnits = Submonoid.map (Units.coeHom M) S.toSubmonoid

theorem AddSubmonoid.addUnits_mono {M : Type u_1} [AddMonoid M] : Monotone AddSubmonoid.addUnits

theorem Submonoid.units_mono {M : Type u_1} [Monoid M] : Monotone Submonoid.units

@[simp]

theorem AddSubmonoid.ofAddUnits_addUnits_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : S.addUnits.ofAddUnits ≤ S

@[simp]

theorem Submonoid.ofUnits_units_le {M : Type u_1} [Monoid M] (S : Submonoid M) : S.units.ofUnits ≤ S

theorem AddSubgroup.ofAddUnits_mono {M : Type u_1} [AddMonoid M] : Monotone AddSubgroup.ofAddUnits

theorem Subgroup.ofUnits_mono {M : Type u_1} [Monoid M] : Monotone Subgroup.ofUnits

@[simp]

theorem AddSubgroup.addUnits_ofAddUnits_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : S.ofAddUnits.addUnits = S

@[simp]

theorem Subgroup.units_ofUnits_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) : S.ofUnits.units = S

def ofAddUnits_addUnits_gci {M : Type u_1} [AddMonoid M] : GaloisCoinsertion AddSubgroup.ofAddUnits AddSubmonoid.addUnits

A Galois coinsertion exists between the coercion from a additive subgroup of additive units to a additive submonoid and the reduction from a additive submonoid to its unit group.

Equations

• ofAddUnits_addUnits_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

def ofUnits_units_gci {M : Type u_1} [Monoid M] : GaloisCoinsertion Subgroup.ofUnits Submonoid.units

A Galois coinsertion exists between the coercion from a subgroup of units to a submonoid and the reduction from a submonoid to its unit group.

Equations

• ofUnits_units_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

theorem ofAddUnits_addUnits_gc {M : Type u_1} [AddMonoid M] : GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits

theorem ofUnits_units_gc {M : Type u_1} [Monoid M] : GaloisConnection Subgroup.ofUnits Submonoid.units

theorem ofAddUnits_le_iff_le_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (H : AddSubgroup (AddUnits M)) : H.ofAddUnits ≤ S ↔ H ≤ S.addUnits

theorem ofUnits_le_iff_le_units {M : Type u_1} [Monoid M] (S : Submonoid M) (H : Subgroup Mˣ) : H.ofUnits ≤ S ↔ H ≤ S.units

theorem AddSubmonoid.mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) : x ∈ S.addUnits ↔ ↑x ∈ S ∧ ↑(-x) ∈ S

theorem Submonoid.mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) : x ∈ S.units ↔ ↑x ∈ S ∧ ↑x⁻¹ ∈ S

theorem AddSubmonoid.mem_addUnits_of_val_mem_neg_val_mem {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h₁ : ↑x ∈ S) (h₂ : ↑(-x) ∈ S) : x ∈ S.addUnits

theorem Submonoid.mem_units_of_val_mem_inv_val_mem {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h₁ : ↑x ∈ S) (h₂ : ↑x⁻¹ ∈ S) : x ∈ S.units

theorem AddSubmonoid.val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits) : ↑x ∈ S

theorem Submonoid.val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : ↑x ∈ S

theorem AddSubmonoid.neg_val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits) : ↑(-x) ∈ S

theorem Submonoid.inv_val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : ↑x⁻¹ ∈ S

theorem AddSubmonoid.coe_neg_val_add_coe_val {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits { x : M // x ∈ S }} : ↑↑(-x) + ↑↑x = 0

theorem Submonoid.coe_inv_val_mul_coe_val {M : Type u_1} [Monoid M] (S : Submonoid M) {x : { x : M // x ∈ S }ˣ} : ↑↑x⁻¹ * ↑↑x = 1

theorem AddSubmonoid.coe_val_add_coe_neg_val {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits { x : M // x ∈ S }} : ↑↑x + ↑↑(-x) = 0

theorem Submonoid.coe_val_mul_coe_inv_val {M : Type u_1} [Monoid M] (S : Submonoid M) {x : { x : M // x ∈ S }ˣ} : ↑↑x * ↑↑x⁻¹ = 1

theorem AddSubmonoid.mk_neg_add_mk_eq_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits) : ⟨(AddUnits.coeHom M) (-x), ⋯⟩ + ⟨(AddUnits.coeHom M) x, ⋯⟩ = 0

theorem Submonoid.mk_inv_mul_mk_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : ⟨(Units.coeHom M) x⁻¹, ⋯⟩ * ⟨(Units.coeHom M) x, ⋯⟩ = 1

theorem AddSubmonoid.mk_add_mk_neg_eq_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits) : ⟨(AddUnits.coeHom M) x, ⋯⟩ + ⟨(AddUnits.coeHom M) (-x), ⋯⟩ = 0

theorem Submonoid.mk_mul_mk_inv_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : ⟨(Units.coeHom M) x, ⋯⟩ * ⟨(Units.coeHom M) x⁻¹, ⋯⟩ = 1

theorem AddSubmonoid.add_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} {y : AddUnits M} (h₁ : x ∈ S.addUnits) (h₂ : y ∈ S.addUnits) : x + y ∈ S.addUnits

theorem Submonoid.mul_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} {y : Mˣ} (h₁ : x ∈ S.units) (h₂ : y ∈ S.units) : x * y ∈ S.units

theorem AddSubmonoid.neg_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits) : -x ∈ S.addUnits

theorem Submonoid.inv_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : x⁻¹ ∈ S.units

theorem AddSubmonoid.neg_mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} : -x ∈ S.addUnits ↔ x ∈ S.addUnits

theorem Submonoid.inv_mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} : x⁻¹ ∈ S.units ↔ x ∈ S.units

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : { x : AddUnits M // x ∈ S.addUnits }), (fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩) ((fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }) x) = (fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩) ((fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }) x)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits { x : M // x ∈ S }) : { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ } ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) S) ∧ { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ } ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) S)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : AddUnits { x : M // x ∈ S }), (fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }) ((fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩) x) = (fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }) ((fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩) x)

def AddSubmonoid.addUnitsEquivAddUnitsType {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : { x : AddUnits M // x ∈ S.addUnits } ≃+ AddUnits { x : M // x ∈ S }

The equivalence between the additive subgroup of additive units of S and the type of additive units of S.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ val ∈ S.addUnits, val ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) S)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ val ∈ S.addUnits, val ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) S)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x : AddUnits M // x ∈ S.addUnits }), { toFun := fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : { x : AddUnits M // x ∈ S.addUnits }) => match x with | ⟨val, h⟩ => { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits { x : M // x ∈ S }) => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1)

def Submonoid.unitsEquivUnitsType {M : Type u_1} [Monoid M] (S : Submonoid M) : { x : Mˣ // x ∈ S.units } ≃* { x : M // x ∈ S }ˣ

The equivalence between the subgroup of units of S and the type of units of S.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubmonoid.addUnits_top {M : Type u_1} [AddMonoid M] : ⊤.addUnits = ⊤

@[simp]

theorem Submonoid.units_top {M : Type u_1} [Monoid M] : ⊤.units = ⊤

theorem AddSubmonoid.addUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (T : AddSubmonoid M) : (S ⊓ T).addUnits = S.addUnits ⊓ T.addUnits

theorem Submonoid.units_inf {M : Type u_1} [Monoid M] (S : Submonoid M) (T : Submonoid M) : (S ⊓ T).units = S.units ⊓ T.units

theorem AddSubmonoid.addUnits_sInf {M : Type u_1} [AddMonoid M] {s : Set (AddSubmonoid M)} : (sInf s).addUnits = ⨅ S ∈ s, S.addUnits

theorem Submonoid.units_sInf {M : Type u_1} [Monoid M] {s : Set (Submonoid M)} : (sInf s).units = ⨅ S ∈ s, S.units

theorem AddSubmonoid.addUnits_iInf {M : Type u_1} [AddMonoid M] {ι : Sort u_2} (f : ι → AddSubmonoid M) : (iInf f).addUnits = ⨅ (i : ι), (f i).addUnits

theorem Submonoid.units_iInf {M : Type u_1} [Monoid M] {ι : Sort u_2} (f : ι → Submonoid M) : (iInf f).units = ⨅ (i : ι), (f i).units

theorem AddSubmonoid.addUnits_iInf₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubmonoid M) : (⨅ (i : ι), ⨅ (j : κ i), f i j).addUnits = ⨅ (i : ι), ⨅ (j : κ i), (f i j).addUnits

theorem Submonoid.units_iInf₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Submonoid M) : (⨅ (i : ι), ⨅ (j : κ i), f i j).units = ⨅ (i : ι), ⨅ (j : κ i), (f i j).units

@[simp]

theorem AddSubmonoid.addUnits_bot {M : Type u_1} [AddMonoid M] : ⊥.addUnits = ⊥

@[simp]

theorem Submonoid.units_bot {M : Type u_1} [Monoid M] : ⊥.units = ⊥

theorem AddSubmonoid.addUnits_surjective {M : Type u_1} [AddMonoid M] : Function.Surjective AddSubmonoid.addUnits

theorem Submonoid.units_surjective {M : Type u_1} [Monoid M] : Function.Surjective Submonoid.units

theorem AddSubmonoid.addUnits_left_inverse {M : Type u_1} [AddMonoid M] : Function.LeftInverse AddSubmonoid.addUnits AddSubgroup.ofAddUnits

theorem Submonoid.units_left_inverse {M : Type u_1} [Monoid M] : Function.LeftInverse Submonoid.units Subgroup.ofUnits

noncomputable def AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoid {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : { x : AddUnits M // x ∈ S.addUnits } ≃+ { x : { x : M // x ∈ S } // x ∈ IsAddUnit.addSubmonoid { x : M // x ∈ S } }

The equivalence between the additive subgroup of additive units of S and the additive submonoid of additive unit elements of S.

Equations

• S.addUnitsEquivIsAddUnitAddSubmonoid = S.addUnitsEquivAddUnitsType.trans AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid

noncomputable def Submonoid.unitsEquivIsUnitSubmonoid {M : Type u_1} [Monoid M] (S : Submonoid M) : { x : Mˣ // x ∈ S.units } ≃* { x : { x : M // x ∈ S } // x ∈ IsUnit.submonoid { x : M // x ∈ S } }

The equivalence between the subgroup of units of S and the submonoid of unit elements of S.

Equations

• S.unitsEquivIsUnitSubmonoid = S.unitsEquivUnitsType.trans Submonoid.unitsTypeEquivIsUnitSubmonoid

theorem AddSubgroup.mem_ofAddUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) : x ∈ S.ofAddUnits ↔ ∃ y ∈ S, ↑y = x

theorem Subgroup.mem_ofUnits_iff {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) : x ∈ S.ofUnits ↔ ∃ y ∈ S, ↑y = x

theorem AddSubgroup.mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {y : AddUnits M} (h₁ : y ∈ S) (h₂ : ↑y = x) : x ∈ S.ofAddUnits

theorem Subgroup.mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {y : Mˣ} (h₁ : y ∈ S) (h₂ : ↑y = x) : x ∈ S.ofUnits

theorem AddSubgroup.exists_mem_ofAddUnits_val_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits) : ∃ y ∈ S, ↑y = x

theorem Subgroup.exists_mem_ofUnits_val_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) : ∃ y ∈ S, ↑y = x

theorem AddSubgroup.mem_of_mem_val_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {y : AddUnits M} (hy : ↑y ∈ S.ofAddUnits) : y ∈ S

theorem Subgroup.mem_of_mem_val_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {y : Mˣ} (hy : ↑y ∈ S.ofUnits) : y ∈ S

theorem AddSubgroup.isAddUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (hx : x ∈ S.ofAddUnits) : IsAddUnit x

theorem Subgroup.isUnit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (hx : x ∈ S.ofUnits) : IsUnit x

noncomputable def AddSubgroup.addUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits) : AddUnits M

Given some x : M which is a member of the additive submonoid of additive unit elements corresponding to a subgroup of units, produce a unit of M whose coercion is equal to x.

Equations

• S.addUnit_of_mem_ofAddUnits h = (Classical.choose h).copy x ⋯ ↑(-Classical.choose h) ⋯

theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits) : x = (AddUnits.coeHom M) (Classical.choose h)

theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits) : ↑(-Classical.choose h) = ↑(-Classical.choose h)

noncomputable def Subgroup.unit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) : Mˣ

Given some x : M which is a member of the submonoid of unit elements corresponding to a subgroup of units, produce a unit of M whose coercion is equal to x. `

Equations

• S.unit_of_mem_ofUnits h = (Classical.choose h).copy x ⋯ ↑(Classical.choose h)⁻¹ ⋯

theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_eq_of_val_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : AddUnits M} (h : ↑x ∈ S.ofAddUnits) : S.addUnit_of_mem_ofAddUnits h = x

theorem Subgroup.unit_of_mem_ofUnits_spec_eq_of_val_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : Mˣ} (h : ↑x ∈ S.ofUnits) : S.unit_of_mem_ofUnits h = x

theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_val_eq_of_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits) : ↑(S.addUnit_of_mem_ofAddUnits h) = x

theorem Subgroup.unit_of_mem_ofUnits_spec_val_eq_of_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) : ↑(S.unit_of_mem_ofUnits h) = x

theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h : x ∈ S.ofAddUnits} : S.addUnit_of_mem_ofAddUnits h ∈ S

theorem Subgroup.unit_of_mem_ofUnits_spec_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h : x ∈ S.ofUnits} : S.unit_of_mem_ofUnits h ∈ S

theorem AddSubgroup.addUnit_eq_addUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x) (h₂ : x ∈ S.ofAddUnits) : h₁.addUnit = S.addUnit_of_mem_ofAddUnits h₂

theorem Subgroup.unit_eq_unit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : x ∈ S.ofUnits) : h₁.unit = S.unit_of_mem_ofUnits h₂

theorem AddSubgroup.addUnit_mem_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h₁ : IsAddUnit x} (h₂ : x ∈ S.ofAddUnits) : h₁.addUnit ∈ S

theorem Subgroup.unit_mem_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h₁ : IsUnit x} (h₂ : x ∈ S.ofUnits) : h₁.unit ∈ S

theorem AddSubgroup.mem_ofAddUnits_of_isAddUnit_of_addUnit_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x) (h₂ : h₁.addUnit ∈ S) : x ∈ S.ofAddUnits

theorem Subgroup.mem_ofUnits_of_isUnit_of_unit_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : h₁.unit ∈ S) : x ∈ S.ofUnits

theorem AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) : x ∈ S.ofAddUnits ↔ ∃ (h : IsAddUnit x), h.addUnit ∈ S

theorem Subgroup.mem_ofUnits_iff_exists_isUnit {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) : x ∈ S.ofUnits ↔ ∃ (h : IsUnit x), h.unit ∈ S

theorem AddSubgroup.ofAddUnitsEquivType.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : { x : M // x ∈ S.ofAddUnits }) : S.addUnit_of_mem_ofAddUnits ⋯ ∈ S

theorem AddSubgroup.ofAddUnitsEquivType.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : { x : AddUnits M // x ∈ S }) : ∃ a ∈ ↑S.toAddSubmonoid, (AddUnits.coeHom M) a = ↑↑x

theorem AddSubgroup.ofAddUnitsEquivType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x : { x : M // x ∈ S.ofAddUnits }), (fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩) ((fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩) x) = (fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩) ((fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩) x)

noncomputable def AddSubgroup.ofAddUnitsEquivType {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : { x : M // x ∈ S.ofAddUnits } ≃+ { x : AddUnits M // x ∈ S }

The equivalence between the coercion of an additive subgroup S of Mˣ to an additive submonoid of M and the additive subgroup itself as a type.

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubgroup.ofAddUnitsEquivType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x : { x : AddUnits M // x ∈ S }), (fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩) ((fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩) x) = x

theorem AddSubgroup.ofAddUnitsEquivType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x x_1 : { x : M // x ∈ S.ofAddUnits }), { toFun := fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩, invFun := fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩, invFun := fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (x : { x : M // x ∈ S.ofAddUnits }) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩, invFun := fun (x : { x : AddUnits M // x ∈ S }) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun x_1

theorem AddSubgroup.ofAddUnitsEquivType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : { x : M // x ∈ S.ofAddUnits }) : ↑x ∈ S.ofAddUnits

noncomputable def Subgroup.ofUnitsEquivType {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) : { x : M // x ∈ S.ofUnits } ≃* { x : Mˣ // x ∈ S }

The equivalence between the coercion of a subgroup S of Mˣ to a submonoid of M and the subgroup itself as a type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.ofAddUnits_bot {M : Type u_1} [AddMonoid M] : ⊥.ofAddUnits = ⊥

@[simp]

theorem Subgroup.ofUnits_bot {M : Type u_1} [Monoid M] : ⊥.ofUnits = ⊥

theorem AddSubgroup.ofAddUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) : (S ⊔ T).ofAddUnits = S.ofAddUnits ⊔ T.ofAddUnits

theorem Subgroup.ofUnits_inf {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : (S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits

theorem AddSubgroup.ofAddUnits_sSup {M : Type u_1} [AddMonoid M] (s : Set (AddSubgroup (AddUnits M))) : (sSup s).ofAddUnits = ⨆ S ∈ s, S.ofAddUnits

theorem Subgroup.ofUnits_sSup {M : Type u_1} [Monoid M] (s : Set (Subgroup Mˣ)) : (sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits

theorem AddSubgroup.ofAddUnits_iSup {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {f : ι → AddSubgroup (AddUnits M)} : (iSup f).ofAddUnits = ⨆ (i : ι), (f i).ofAddUnits

theorem Subgroup.ofUnits_iSup {M : Type u_1} [Monoid M] {ι : Sort u_2} {f : ι → Subgroup Mˣ} : (iSup f).ofUnits = ⨆ (i : ι), (f i).ofUnits

theorem AddSubgroup.ofAddUnits_iSup₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubgroup (AddUnits M)) : (⨆ (i : ι), ⨆ (j : κ i), f i j).ofAddUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofAddUnits

theorem Subgroup.ofUnits_iSup₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Subgroup Mˣ) : (⨆ (i : ι), ⨆ (j : κ i), f i j).ofUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofUnits

theorem AddSubgroup.ofAddUnits_injective {M : Type u_1} [AddMonoid M] : Function.Injective AddSubgroup.ofAddUnits

theorem Subgroup.ofUnits_injective {M : Type u_1} [Monoid M] : Function.Injective Subgroup.ofUnits

@[simp]

theorem AddSubgroup.ofAddUnits_sup_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) : (S.ofAddUnits ⊔ T.ofAddUnits).addUnits = S ⊔ T

@[simp]

theorem Subgroup.ofUnits_sup_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T

@[simp]

theorem AddSubgroup.ofAddUnits_inf_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) : (S.ofAddUnits ⊓ T.ofAddUnits).addUnits = S ⊓ T

@[simp]

theorem Subgroup.ofUnits_inf_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : (S.ofUnits ⊓ T.ofUnits).units = S ⊓ T

theorem AddSubgroup.ofAddUnits_right_inverse {M : Type u_1} [AddMonoid M] : Function.RightInverse AddSubgroup.ofAddUnits AddSubmonoid.addUnits

theorem Subgroup.ofUnits_right_inverse {M : Type u_1} [Monoid M] : Function.RightInverse Subgroup.ofUnits Submonoid.units

theorem AddSubgroup.ofAddUnits_strictMono {M : Type u_1} [AddMonoid M] : StrictMono AddSubgroup.ofAddUnits

theorem Subgroup.ofUnits_strictMono {M : Type u_1} [Monoid M] : StrictMono Subgroup.ofUnits

theorem Subgroup.ofUnits_le_ofUnits_iff {M : Type u_1} [Monoid M] {S : Subgroup Mˣ} {T : Subgroup Mˣ} : S.ofUnits ≤ T.ofUnits ↔ S ≤ T

noncomputable def AddSubgroup.ofAddUnitsTopEquiv {M : Type u_1} [AddMonoid M] : { x : M // x ∈ ⊤.ofAddUnits } ≃+ AddUnits M

The equivalence between the additive subgroup of additive units of S and the additive submonoid of additive unit elements of S.

Equations

• AddSubgroup.ofAddUnitsTopEquiv = ⊤.ofAddUnitsEquivType.trans AddSubgroup.topEquiv

noncomputable def Subgroup.ofUnitsTopEquiv {M : Type u_1} [Monoid M] : { x : M // x ∈ ⊤.ofUnits } ≃* Mˣ

The equivalence between the top subgroup of Mˣ coerced to a submonoid M and the units of M.

Equations

• Subgroup.ofUnitsTopEquiv = ⊤.ofUnitsEquivType.trans Subgroup.topEquiv

theorem AddSubgroup.mem_addUnits_iff_val_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : AddUnits G) : x ∈ H.addUnits ↔ ↑x ∈ H

theorem Subgroup.mem_units_iff_val_mem {G : Type u_2} [Group G] (H : Subgroup G) (x : Gˣ) : x ∈ H.units ↔ ↑x ∈ H

theorem AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : G) : x ∈ H.ofAddUnits ↔ toAddUnits x ∈ H

theorem Subgroup.mem_ofUnits_iff_toUnits_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : G) : x ∈ H.ofUnits ↔ toUnits x ∈ H

@[simp]

theorem AddSubgroup.mem_iff_toAddUnits_mem_addUnits {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : G) : toAddUnits x ∈ H.addUnits ↔ x ∈ H

@[simp]

theorem Subgroup.mem_iff_toUnits_mem_units {G : Type u_2} [Group G] (H : Subgroup G) (x : G) : toUnits x ∈ H.units ↔ x ∈ H

@[simp]

theorem AddSubgroup.val_mem_ofAddUnits_iff_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : AddUnits G) : ↑x ∈ H.ofAddUnits ↔ x ∈ H

@[simp]

theorem Subgroup.val_mem_ofUnits_iff_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : Gˣ) : ↑x ∈ H.ofUnits ↔ x ∈ H

def AddSubgroup.addUnitsEquivSelf {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : { x : AddUnits G // x ∈ H.addUnits } ≃+ { x : G // x ∈ H }

The equivalence between the greatest subgroup of additive units contained within T and T itself.

Equations

• H.addUnitsEquivSelf = H.addUnitsEquivAddUnitsType.trans toAddUnits.symm

def Subgroup.unitsEquivSelf {G : Type u_2} [Group G] (H : Subgroup G) : { x : Gˣ // x ∈ H.units } ≃* { x : G // x ∈ H }

The equivalence between the greatest subgroup of units contained within T and T itself.

Equations

• H.unitsEquivSelf = H.unitsEquivUnitsType.trans toUnits.symm