Group actions on and by Mˣ

This file provides the action of a unit on a type α, SMul Mˣ α, in the presence of SMul M α, with the obvious definition stated in Units.smul_def. This definition preserves MulAction and DistribMulAction structures too.

Additionally, a MulAction G M for some group G satisfying some additional properties admits a MulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul. These instances use a primed name.

The results are repeated for AddUnits and VAdd where relevant.

Action of the units of M on a type α

ink

instance AddUnits.instVAddAddUnits {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] : VAdd (AddUnits M) α

Equations

• AddUnits.instVAddAddUnits = { vadd := fun m a => ↑m +ᵥ a }

ink

instance Units.instSMulUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] : SMul Mˣ α

Equations

• Units.instSMulUnits = { smul := fun m a => ↑m • a }

ink

theorem AddUnits.vadd_def {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] (m : AddUnits M) (a : α) : m +ᵥ a = ↑m +ᵥ a

ink

theorem Units.smul_def {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] (m : Mˣ) (a : α) : m • a = ↑m • a

ink

@[simp]

theorem Units.smul_isUnit {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] {m : M} (hm : IsUnit m) (a : α) : IsUnit.unit hm • a = m • a

ink

theorem IsUnit.inv_smul {α : Type u_1} [inst : Monoid α] {a : α} (h : IsUnit a) : (IsUnit.unit h)⁻¹ • a = 1

ink

instance AddUnits.instFaithfulVAddAddUnitsInstVAddAddUnits {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] [inst : FaithfulVAdd M α] : FaithfulVAdd (AddUnits M) α

Equations

• @AddUnits.instFaithfulVAddAddUnitsInstVAddAddUnits = @AddUnits.instFaithfulVAddAddUnitsInstVAddAddUnits.proof_1

ink

def AddUnits.instFaithfulVAddAddUnitsInstVAddAddUnits.proof_1 {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : VAdd M α] [inst : FaithfulVAdd M α] : FaithfulVAdd (AddUnits M) α

Equations

• (_ : FaithfulVAdd (AddUnits M) α) = (_ : FaithfulVAdd (AddUnits M) α)

ink

instance Units.instFaithfulSMulUnitsInstSMulUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : SMul M α] [inst : FaithfulSMul M α] : FaithfulSMul Mˣ α

Equations

• @Units.instFaithfulSMulUnitsInstSMulUnits = @Units.instFaithfulSMulUnitsInstSMulUnits.proof_1

ink

def AddUnits.instAddActionAddUnitsToAddMonoidToSubNegAddMonoidInstAddGroupAddUnits.proof_1 {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] (m : AddUnits M) (n : AddUnits M) (b : α) : ↑m + ↑n +ᵥ b = ↑m +ᵥ (↑n +ᵥ b)

Equations

• (_ : ∀ (b : α), ↑m + ↑n +ᵥ b = ↑m +ᵥ (↑n +ᵥ b)) = (_ : ∀ (p : α), ↑m + ↑n +ᵥ p = ↑m +ᵥ (↑n +ᵥ p))

ink

instance AddUnits.instAddActionAddUnitsToAddMonoidToSubNegAddMonoidInstAddGroupAddUnits {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] : AddAction (AddUnits M) α

Equations

• AddUnits.instAddActionAddUnitsToAddMonoidToSubNegAddMonoidInstAddGroupAddUnits = AddAction.mk (_ : ∀ (b : α), 0 +ᵥ b = b) (_ : ∀ (m n : AddUnits M) (b : α), ↑m + ↑n +ᵥ b = ↑m +ᵥ (↑n +ᵥ b))

ink

instance Units.instMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] : MulAction Mˣ α

Equations

• Units.instMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits = MulAction.mk (_ : ∀ (b : α), 1 • b = b) (_ : ∀ (m n : Mˣ) (b : α), (↑m * ↑n) • b = ↑m • ↑n • b)

ink

instance Units.instSMulZeroClassUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : Zero α] [inst : SMulZeroClass M α] : SMulZeroClass Mˣ α

Equations

• Units.instSMulZeroClassUnits = SMulZeroClass.mk (_ : ∀ (m : Mˣ), ↑m • 0 = 0)

ink

instance Units.instDistribSMulUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : AddZeroClass α] [inst : DistribSMul M α] : DistribSMul Mˣ α

Equations

• Units.instDistribSMulUnits = DistribSMul.mk (_ : ∀ (m : Mˣ) (b₁ b₂ : α), ↑m • (b₁ + b₂) = ↑m • b₁ + ↑m • b₂)

ink

instance Units.instDistribMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : AddMonoid α] [inst : DistribMulAction M α] : DistribMulAction Mˣ α

Equations

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

ink

instance Units.instMulDistribMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : Monoid α] [inst : MulDistribMulAction M α] : MulDistribMulAction Mˣ α

Equations

• Units.instMulDistribMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits = MulDistribMulAction.mk (_ : ∀ (m : Mˣ) (b₁ b₂ : α), ↑m • (b₁ * b₂) = ↑m • b₁ * ↑m • b₂) (_ : ∀ (m : Mˣ), ↑m • 1 = 1)

ink

instance Units.smulCommClass_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid M] [inst : SMul M α] [inst : SMul N α] [inst : SMulCommClass M N α] : SMulCommClass Mˣ N α

Equations

• @Units.smulCommClass_left = @Units.smulCommClass_left.proof_1

ink

instance Units.smulCommClass_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid N] [inst : SMul M α] [inst : SMul N α] [inst : SMulCommClass M N α] : SMulCommClass M Nˣ α

Equations

• @Units.smulCommClass_right = @Units.smulCommClass_right.proof_1

ink

instance Units.instIsScalarTowerUnitsInstSMulUnitsInstSMulUnits {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid M] [inst : SMul M N] [inst : SMul M α] [inst : SMul N α] [inst : IsScalarTower M N α] : IsScalarTower Mˣ N α

Equations

• @Units.instIsScalarTowerUnitsInstSMulUnitsInstSMulUnits = @Units.instIsScalarTowerUnitsInstSMulUnitsInstSMulUnits.proof_1

Action of a group G on units of M

ink

instance Units.mulAction' {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] : MulAction G Mˣ

If an action G associates and commutes with multiplication on M, then it lifts to an action on Mˣ. Notably, this provides mul_action Mˣ Nˣ under suitable conditions.

Equations

• Units.mulAction' = MulAction.mk (_ : ∀ (m : Mˣ), 1 • m = m) (_ : ∀ (g₁ g₂ : G) (m : Mˣ), (g₁ * g₂) • m = g₁ • g₂ • m)

ink

@[simp]

theorem Units.val_smul {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] (g : G) (m : Mˣ) : ↑(g • m) = g • ↑m

ink

@[simp]

theorem Units.smul_inv {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] (g : G) (m : Mˣ) : (g • m)⁻¹ = g⁻¹ • m⁻¹

Note that this lemma exists more generally as the global smul_inv

ink

instance Units.smulCommClass' {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : Group G] [inst : Group H] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : MulAction H M] [inst : SMulCommClass H M M] [inst : IsScalarTower G M M] [inst : IsScalarTower H M M] [inst : SMulCommClass G H M] : SMulCommClass G H Mˣ

Transfer SMulCommClass G H M to SMulCommClass G H Mˣ

Equations

• @Units.smulCommClass' = @Units.smulCommClass'.proof_1

ink

instance Units.isScalarTower' {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : SMul G H] [inst : Group G] [inst : Group H] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : MulAction H M] [inst : SMulCommClass H M M] [inst : IsScalarTower G M M] [inst : IsScalarTower H M M] [inst : IsScalarTower G H M] : IsScalarTower G H Mˣ

Transfer IsScalarTower G H M to IsScalarTower G H Mˣ

Equations

• @Units.isScalarTower' = @Units.isScalarTower'.proof_1

ink

instance Units.isScalarTower'_left {G : Type u_1} {M : Type u_2} {α : Type u_3} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMul M α] [inst : SMul G α] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] [inst : IsScalarTower G M α] : IsScalarTower G Mˣ α

Transfer IsScalarTower G M α to IsScalarTower G Mˣ α

Equations

• @Units.isScalarTower'_left = @Units.isScalarTower'_left.proof_1

ink

instance Units.mulDistribMulAction' {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulDistribMulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] : MulDistribMulAction G Mˣ

A stronger form of Units.mul_action'.

Equations

• Units.mulDistribMulAction' = let src := Units.mulAction'; MulDistribMulAction.mk (_ : ∀ (x : G) (x_1 x_2 : Mˣ), x • (x_1 * x_2) = x • x_1 * x • x_2) (_ : ∀ (x : G), x • 1 = 1)

ink

theorem IsUnit.smul {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] [inst : MulAction G M] [inst : SMulCommClass G M M] [inst : IsScalarTower G M M] {m : M} (g : G) (h : IsUnit m) : IsUnit (g • m)