Equivariant homomorphisms

Main definitions

• MulActionHom M X Y, the type of equivariant functions from X to Y, where M is a monoid that acts on the types X and Y.
• DistribMulActionHom M A B, the type of equivariant additive monoid homomorphisms from A to B, where M is a monoid that acts on the additive monoids A and B.
• MulSemiringActionHom M R S, the type of equivariant ring homomorphisms from R to S, where M is a monoid that acts on the rings R and S.

The above types have corresponding classes:

• SMulHomClass F M X Y states that F is a type of bundled X → Y homs preserving scalar multiplication by M
• DistribMulActionHomClass F M A B states that F is a type of bundled A → B homs preserving the additive monoid structure and scalar multiplication by M
• MulSemiringActionHomClass F M R S states that F is a type of bundled R → S homs preserving the ring structure and scalar multiplication by M

Notations

• X →[M] Y is MulActionHom M X Y.
• A →+[M] B is DistribMulActionHom M A B.
• R →+*[M] S is MulSemiringActionHom M R S.

structure MulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] : Type (max u_2 u_3)

Equivariant functions.

• toFun : X → Y

  The underlying function.

• map_smul' : ∀ (m : M') (x : X), MulActionHom.toFun s (m • x) = m • MulActionHom.toFun s x

  The proposition that the function preserves the action.

def «MulActionHomLocal≺» : Lean.TrailingParserDescr

Equivariant functions.

Equations

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

class SMulHomClass (F : Type u_16) (M : outParam (Type u_17)) (X : outParam (Type u_18)) (Y : outParam (Type u_19)) [SMul M X] [SMul M Y] extends FunLike : Type (max (max u_16 u_18) u_19)

SMulHomClass F M X Y states that F is a type of morphisms preserving scalar multiplication by M.

You should extend this class when you extend MulActionHom.

• coe : F → X → Y
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : X), f (c • x) = c • f x

  The proposition that the function preserves the action.

instance instSMulHomClassMulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] : SMulHomClass (X →[M'] Y) M' X Y

Equations

• instSMulHomClassMulActionHom M' X Y = SMulHomClass.mk (_ : ∀ (self : X →[M'] Y) (m : M') (x : X), MulActionHom.toFun self (m • x) = m • MulActionHom.toFun self x)

def SMulHomClass.toMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] (f : F) : X →[M] Y

Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

Equations

• ↑f = { toFun := ⇑f, map_smul' := (_ : ∀ (c : M) (x : X), f (c • x) = c • f x) }

instance MulActionHom.instCoeTCMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [SMulHomClass F M X Y] : CoeTC F (X →[M] Y)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

Equations

• MulActionHom.instCoeTCMulActionHom = { coe := SMulHomClass.toMulActionHom }

def IsScalarTower.smulHomClass (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] (F : Type u_16) [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [SMulHomClass F X X Y] : SMulHomClass F M' X Y

If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action.

Equations

• IsScalarTower.smulHomClass M' X Y F = SMulHomClass.mk (_ : ∀ (f : F) (m : M') (x : X), f (m • x) = m • f x)

theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) (m : M') (x : X) : f (m • x) = m • f x

theorem MulActionHom.ext {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} : (∀ (x : X), f x = g x) → f = g

theorem MulActionHom.ext_iff {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} : f = g ↔ ∀ (x : X), f x = g x

theorem MulActionHom.congr_fun {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} (h : f = g) (x : X) : f x = g x

def MulActionHom.id (M' : Type u_1) {X : Type u_2} [SMul M' X] : X →[M'] X

The identity map as an equivariant map.

Equations

• MulActionHom.id M' = { toFun := id, map_smul' := (_ : ∀ (x : M') (x_1 : X), id (x • x_1) = id (x • x_1)) }

@[simp]

theorem MulActionHom.id_apply (M' : Type u_1) {X : Type u_2} [SMul M' X] (x : X) : (MulActionHom.id M') x = x

def MulActionHom.comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) : X →[M'] Z

Composition of two equivariant maps.

Equations

• MulActionHom.comp g f = { toFun := ⇑g ∘ ⇑f, map_smul' := (_ : ∀ (m : M') (x : X), g (f (m • x)) = m • g (f x)) }

@[simp]

theorem MulActionHom.comp_apply {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) : (MulActionHom.comp g f) x = g (f x)

@[simp]

theorem MulActionHom.id_comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) : MulActionHom.comp (MulActionHom.id M') f = f

@[simp]

theorem MulActionHom.comp_id {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) : MulActionHom.comp f (MulActionHom.id M') = f

@[simp]

theorem MulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (a : B), (MulActionHom.inverse f g h₁ h₂) a = g a

def MulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : B →[M] A

The inverse of a bijective equivariant map is equivariant.

Equations

• MulActionHom.inverse f g h₁ h₂ = { toFun := g, map_smul' := (_ : ∀ (m : M) (x : B), g (m • x) = m • g x) }

@[simp]

theorem SMulCommClass.toMulActionHom_apply {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) : ∀ (x : α), (SMulCommClass.toMulActionHom N α c) x = c • x

def SMulCommClass.toMulActionHom {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) : α →[N] α

If actions of M and N on α commute, then for c : M, (c • · : α → α) is an N-action homomorphism.

Equations

• SMulCommClass.toMulActionHom N α c = { toFun := fun (x : α) => c • x, map_smul' := (_ : ∀ (n : N) (a : α), c • n • a = n • c • a) }

structure DistribMulActionHom (M : Type u_5) [Monoid M] (A : Type u_6) [AddMonoid A] [DistribMulAction M A] (B : Type u_8) [AddMonoid B] [DistribMulAction M B] extends MulActionHom : Type (max u_6 u_8)

Equivariant additive monoid homomorphisms.

• toFun : A → B
• map_smul' : ∀ (m : M) (x : A), MulActionHom.toFun s.toMulActionHom (m • x) = m • MulActionHom.toFun s.toMulActionHom x
• map_zero' : MulActionHom.toFun s.toMulActionHom 0 = 0

  The proposition that the function preserves 0

• map_add' : ∀ (x y : A), MulActionHom.toFun s.toMulActionHom (x + y) = MulActionHom.toFun s.toMulActionHom x + MulActionHom.toFun s.toMulActionHom y

  The proposition that the function preserves addition

@[reducible]

abbrev DistribMulActionHom.toAddMonoidHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (self : A →+[M] B) : A →+ B

Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.

Equations

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

def «DistribMulActionHomLocal≺» : Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

class DistribMulActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (A : outParam (Type u_18)) (B : outParam (Type u_19)) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] extends SMulHomClass : Type (max (max u_16 u_18) u_19)

DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and scalar multiplication by M.

You should extend this class when you extend DistribMulActionHom.

• coe : F → A → B
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : A), f (c • x) = c • f x
• map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y

  The proposition that the function preserves addition

• map_zero : ∀ (f : F), f 0 = 0

  The proposition that the function preserves 0

instance DistribMulActionHom.instDistribMulActionHomClassDistribMulActionHom (M : Type u_5) [Monoid M] (A : Type u_6) [AddMonoid A] [DistribMulAction M A] (B : Type u_8) [AddMonoid B] [DistribMulAction M B] : DistribMulActionHomClass (A →+[M] B) M A B

Equations

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

def DistribMulActionHomClass.toDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [DistribMulActionHomClass F M A B] (f : F) : A →+[M] B

Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

Equations

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

instance DistribMulActionHom.instCoeTCDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [DistribMulActionHomClass F M A B] : CoeTC F (A →+[M] B)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

Equations

• DistribMulActionHom.instCoeTCDistribMulActionHom = { coe := DistribMulActionHomClass.toDistribMulActionHom }

@[simp]

theorem DistribMulActionHom.toFun_eq_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : f.toFun = ⇑f

theorem DistribMulActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : ⇑↑f = ⇑f

theorem DistribMulActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : ⇑↑f = ⇑f

theorem DistribMulActionHom.ext {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} : (∀ (x : A), f x = g x) → f = g

theorem DistribMulActionHom.ext_iff {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} : f = g ↔ ∀ (x : A), f x = g x

theorem DistribMulActionHom.congr_fun {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) (x : A) : f x = g x

theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : ↑f = ↑g) : f = g

theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : ↑f = ↑g) : f = g

theorem DistribMulActionHom.map_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : f 0 = 0

theorem DistribMulActionHom.map_add {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (x : A) (y : A) : f (x + y) = f x + f y

theorem DistribMulActionHom.map_neg {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') : f (-x) = -f x

theorem DistribMulActionHom.map_sub {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') (y : A') : f (x - y) = f x - f y

theorem DistribMulActionHom.map_smul {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (m : M) (x : A) : f (m • x) = m • f x

def DistribMulActionHom.id (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] : A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Equations

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

@[simp]

theorem DistribMulActionHom.id_apply (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (x : A) : (DistribMulActionHom.id M) x = x

instance DistribMulActionHom.instZeroDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] : Zero (A →+[M] B)

Equations

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

instance DistribMulActionHom.instOneDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] : One (A →+[M] A)

Equations

• DistribMulActionHom.instOneDistribMulActionHom = { one := DistribMulActionHom.id M }

@[simp]

theorem DistribMulActionHom.coe_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] : ⇑0 = 0

@[simp]

theorem DistribMulActionHom.coe_one {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] : ⇑1 = id

theorem DistribMulActionHom.zero_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (a : A) : 0 a = 0

theorem DistribMulActionHom.one_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (a : A) : 1 a = a

instance DistribMulActionHom.instInhabitedDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] : Inhabited (A →+[M] B)

Equations

• DistribMulActionHom.instInhabitedDistribMulActionHom = { default := 0 }

def DistribMulActionHom.comp {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) : A →+[M] C

Composition of two equivariant additive monoid homomorphisms.

Equations

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

@[simp]

theorem DistribMulActionHom.comp_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) (x : A) : (DistribMulActionHom.comp g f) x = g (f x)

@[simp]

theorem DistribMulActionHom.id_comp {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : DistribMulActionHom.comp (DistribMulActionHom.id M) f = f

@[simp]

theorem DistribMulActionHom.comp_id {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) : DistribMulActionHom.comp f (DistribMulActionHom.id M) = f

@[simp]

theorem DistribMulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (a : B), (DistribMulActionHom.inverse f g h₁ h₂) a = g a

def DistribMulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : B →+[M] A

The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

Equations

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

theorem DistribMulActionHom.ext_ring {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} (h : f 1 = g 1) : f = g

theorem DistribMulActionHom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} : f = g ↔ f 1 = g 1

@[simp]

theorem SMulCommClass.toDistribMulActionHom_apply {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) : ∀ (x : A), (SMulCommClass.toDistribMulActionHom N A c) x = c • x

def SMulCommClass.toDistribMulActionHom {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) : A →+[N] A

If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

Equations

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

structure MulSemiringActionHom (M : Type u_5) [Monoid M] (R : Type u_11) [Semiring R] [MulSemiringAction M R] (S : Type u_13) [Semiring S] [MulSemiringAction M S] extends DistribMulActionHom : Type (max u_11 u_13)

Equivariant ring homomorphisms.

• toFun : R → S
• map_smul' : ∀ (m : M) (x : R), MulActionHom.toFun s.toMulActionHom (m • x) = m • MulActionHom.toFun s.toMulActionHom x
• map_zero' : MulActionHom.toFun s.toMulActionHom 0 = 0
• map_add' : ∀ (x y : R), MulActionHom.toFun s.toMulActionHom (x + y) = MulActionHom.toFun s.toMulActionHom x + MulActionHom.toFun s.toMulActionHom y
• map_one' : MulActionHom.toFun s.toMulActionHom 1 = 1

  The proposition that the function preserves 1

• map_mul' : ∀ (x y : R), MulActionHom.toFun s.toMulActionHom (x * y) = MulActionHom.toFun s.toMulActionHom x * MulActionHom.toFun s.toMulActionHom y

  The proposition that the function preserves multiplication

@[reducible]

abbrev MulSemiringActionHom.toRingHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (self : R →+*[M] S) : R →+* S

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

Equations

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

def «MulSemiringActionHomLocal≺» : Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

class MulSemiringActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [Monoid M] [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction M S] extends DistribMulActionHomClass : Type (max (max u_16 u_18) u_19)

MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and scalar multiplication by M.

You should extend this class when you extend MulSemiringActionHom.

• coe : F → R → S
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : M) (x : R), f (c • x) = c • f x
• map_add : ∀ (f : F) (x y : R), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• map_mul : ∀ (f : F) (x y : R), f (x * y) = f x * f y

  The proposition that the function preserves multiplication

• map_one : ∀ (f : F), f 1 = 1

  The proposition that the function preserves 1

instance MulSemiringActionHom.instMulSemiringActionHomClassMulSemiringActionHomToDistribMulActionToDistribMulAction (M : Type u_5) [Monoid M] (R : Type u_11) [Semiring R] [MulSemiringAction M R] (S : Type u_13) [Semiring S] [MulSemiringAction M S] : MulSemiringActionHomClass (R →+*[M] S) M R S

Equations

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

def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {F : Type u_16} [MulSemiringActionHomClass F M R S] (f : F) : R →+*[M] S

Turn an element of a type F satisfying MulSemiringActionHomClass F M R S into an actual MulSemiringActionHom. This is declared as the default coercion from F to MulSemiringActionHom M X Y.

Equations

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

instance MulSemiringActionHom.instCoeTCMulSemiringActionHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {F : Type u_16} [MulSemiringActionHomClass F M R S] : CoeTC F (R →+*[M] S)

Any type satisfying MulSemiringActionHomClass can be cast into MulSemiringActionHom via MulSemiringActionHomClass.toMulSemiringActionHom.

Equations

• MulSemiringActionHom.instCoeTCMulSemiringActionHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }

theorem MulSemiringActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : ⇑↑f = ⇑f

theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : ⇑↑f = ⇑f

theorem MulSemiringActionHom.ext {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} : (∀ (x : R), f x = g x) → f = g

theorem MulSemiringActionHom.ext_iff {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} : f = g ↔ ∀ (x : R), f x = g x

theorem MulSemiringActionHom.map_zero {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : f 0 = 0

theorem MulSemiringActionHom.map_add {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) : f (x + y) = f x + f y

theorem MulSemiringActionHom.map_neg {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') : f (-x) = -f x

theorem MulSemiringActionHom.map_sub {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') (y : R') : f (x - y) = f x - f y

theorem MulSemiringActionHom.map_one {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : f 1 = 1

theorem MulSemiringActionHom.map_mul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) : f (x * y) = f x * f y

theorem MulSemiringActionHom.map_smul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) : f (m • x) = m • f x

def MulSemiringActionHom.id (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] : R →+*[M] R

The identity map as an equivariant ring homomorphism.

Equations

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

@[simp]

theorem MulSemiringActionHom.id_apply (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] (x : R) : (MulSemiringActionHom.id M) x = x

def MulSemiringActionHom.comp {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) : R →+*[M] T

Composition of two equivariant additive monoid homomorphisms.

Equations

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

@[simp]

theorem MulSemiringActionHom.comp_apply {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) : (MulSemiringActionHom.comp g f) x = g (f x)

@[simp]

theorem MulSemiringActionHom.id_comp {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : MulSemiringActionHom.comp (MulSemiringActionHom.id M) f = f

@[simp]

theorem MulSemiringActionHom.comp_id {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) : MulSemiringActionHom.comp f (MulSemiringActionHom.id M) = f