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→ Y homs preserving scalar multiplication by M
DistribMulActionHomClass F M A B states that F is a type of bundled A → B→ 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→ S homs preserving the ring structure and scalar multiplication by M

Notations #

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

source

ink

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

Type (maxu_2u_3)

The underlying function.
toFun : X → Y
The proposition that the function preserves the action.
map_smul' : ∀ (m : M') (x : X), toFun (m • x) = m • toFun x

Equivariant functions.

Instances For

source

ink

def «MulActionHomLocal≺» :

Lean.TrailingParserDescr

Equivariant functions.

Equations

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

source

ink

class SMulHomClass (F : Type u_1) (M : outParam (Type u_2)) (X : outParam (Type u_3)) (Y : outParam (Type u_4)) [inst : SMul M X] [inst : SMul M Y] extends FunLike :

Type (max(maxu_1u_3)u_4)

The proposition that the function preserves the action.
map_smul : ∀ (f : F) (c : M) (x : X), ↑f (c • x) = c • ↑f x

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.

Instances

source

ink

instance instSMulHomClassMulActionHom (M' : Type u_1) (X : Type u_2) [inst : SMul M' X] (Y : Type u_3) [inst : 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)

source

ink

def SMulHomClass.toMulActionHom {X : Type u_1} {Y : Type u_2} {M : Type u_3} {F : Type u_4} [inst : SMul M X] [inst : SMul M Y] [inst : 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) }

source

ink

instance MulActionHom.instCoeTCMulActionHom {X : Type u_1} {Y : Type u_2} {M : Type u_3} {F : Type u_4} [inst : SMul M X] [inst : SMul M Y] [inst : 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 }

source

ink

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

↑f (m • x) = m • ↑f x

source

ink

theorem MulActionHom.ext {M' : Type u_1} {X : Type u_2} [inst : SMul M' X] {Y : Type u_3} [inst : SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :

(∀ (x : X), ↑f x = ↑g x) → f = g

source

ink

theorem MulActionHom.ext_iff {M' : Type u_1} {X : Type u_2} [inst : SMul M' X] {Y : Type u_3} [inst : SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :

f = g ↔ ∀ (x : X), ↑f x = ↑g x

source

ink

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

↑f x = ↑g x

source

ink

def MulActionHom.id (M' : Type u_1) {X : Type u_2} [inst : 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)) }

source

ink

@[simp]

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

↑(MulActionHom.id M') x = x

source

ink

def MulActionHom.comp {M' : Type u_1} {X : Type u_2} [inst : SMul M' X] {Y : Type u_3} [inst : SMul M' Y] {Z : Type u_4} [inst : 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)) }

source

ink

@[simp]

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

↑(MulActionHom.comp g f) x = ↑g (↑f x)

source

ink

@[simp]

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

MulActionHom.comp (MulActionHom.id M') f = f

source

ink

@[simp]

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

MulActionHom.comp f (MulActionHom.id M') = f

source

ink

@[simp]

theorem MulActionHom.inverse_toFun {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : 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

source

ink

def MulActionHom.inverse {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : 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) }

source

ink

structure DistribMulActionHom (M : Type u_1) [inst : Monoid M] (A : Type u_2) [inst : AddMonoid A] [inst : DistribMulAction M A] (B : Type u_3) [inst : AddMonoid B] [inst : DistribMulAction M B] extends MulActionHom :

Type (maxu_2u_3)

The proposition that the function preserves 0
map_zero' : MulActionHom.toFun toMulActionHom 0 = 0
The proposition that the function preserves addition
map_add' : ∀ (x y : A), MulActionHom.toFun toMulActionHom (x + y) = MulActionHom.toFun toMulActionHom x + MulActionHom.toFun toMulActionHom y

Equivariant additive monoid homomorphisms.

Instances For

source

ink

abbrev DistribMulActionHom.toAddMonoidHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : 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.

source

ink

def «DistribMulActionHomLocal≺» :

Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

source

ink

class DistribMulActionHomClass (F : Type u_1) (M : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [inst : Monoid M] [inst : AddMonoid A] [inst : AddMonoid B] [inst : DistribMulAction M A] [inst : DistribMulAction M B] extends SMulHomClass :

Type (max(maxu_1u_3)u_4)

The proposition that the function preserves addition
map_add : ∀ (f : F) (x y : A), ↑f (x + y) = ↑f x + ↑f y
The proposition that the function preserves 0
map_zero : ∀ (f : F), ↑f 0 = 0

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.

Instances

source

ink

instance DistribMulActionHom.instDistribMulActionHomClassDistribMulActionHom (M : Type u_1) [inst : Monoid M] (A : Type u_2) [inst : AddMonoid A] [inst : DistribMulAction M A] (B : Type u_3) [inst : AddMonoid B] [inst : DistribMulAction M B] :

DistribMulActionHomClass (A →+[M] B) M A B

Equations

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

source

ink

def DistribMulActionHomClass.toDistribMulActionHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {F : Type u_4} [inst : 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.

source

ink

instance DistribMulActionHom.instCoeTCDistribMulActionHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {F : Type u_4} [inst : 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 }

source

ink

@[simp]

theorem DistribMulActionHom.toFun_eq_coe {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

f.toMulActionHom.toFun = ↑f

source

ink

theorem DistribMulActionHom.coe_fn_coe {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

↑↑f = ↑f

source

ink

theorem DistribMulActionHom.coe_fn_coe' {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

↑↑f = ↑f

source

ink

theorem DistribMulActionHom.ext {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :

(∀ (x : A), ↑f x = ↑g x) → f = g

source

ink

theorem DistribMulActionHom.ext_iff {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :

f = g ↔ ∀ (x : A), ↑f x = ↑g x

source

ink

theorem DistribMulActionHom.congr_fun {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) (x : A) :

↑f x = ↑g x

source

ink

theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : ↑f = ↑g) :

f = g

source

ink

theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : ↑f = ↑g) :

f = g

source

ink

theorem DistribMulActionHom.map_zero {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

↑f 0 = 0

source

ink

theorem DistribMulActionHom.map_add {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) (x : A) (y : A) :

↑f (x + y) = ↑f x + ↑f y

source

ink

theorem DistribMulActionHom.map_neg {M : Type u_1} [inst : Monoid M] (A' : Type u_2) [inst : AddGroup A'] [inst : DistribMulAction M A'] (B' : Type u_3) [inst : AddGroup B'] [inst : DistribMulAction M B'] (f : A' →+[M] B') (x : A') :

↑f (-x) = -↑f x

source

ink

theorem DistribMulActionHom.map_sub {M : Type u_1} [inst : Monoid M] (A' : Type u_2) [inst : AddGroup A'] [inst : DistribMulAction M A'] (B' : Type u_3) [inst : AddGroup B'] [inst : DistribMulAction M B'] (f : A' →+[M] B') (x : A') (y : A') :

↑f (x - y) = ↑f x - ↑f y

source

ink

theorem DistribMulActionHom.map_smul {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) (m : M) (x : A) :

↑f (m • x) = m • ↑f x

source

ink

def DistribMulActionHom.id (M : Type u_1) [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : 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.

source

ink

@[simp]

theorem DistribMulActionHom.id_apply (M : Type u_2) [inst : Monoid M] {A : Type u_1} [inst : AddMonoid A] [inst : DistribMulAction M A] (x : A) :

↑(DistribMulActionHom.id M) x = x

source

ink

instance DistribMulActionHom.instZeroDistribMulActionHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] :

Zero (A →+[M] B)

Equations

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

source

ink

instance DistribMulActionHom.instOneDistribMulActionHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] :

One (A →+[M] A)

Equations

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

source

ink

@[simp]

theorem DistribMulActionHom.coe_zero {M : Type u_3} [inst : Monoid M] {A : Type u_1} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_2} [inst : AddMonoid B] [inst : DistribMulAction M B] :

↑0 = 0

source

ink

@[simp]

theorem DistribMulActionHom.coe_one {M : Type u_2} [inst : Monoid M] {A : Type u_1} [inst : AddMonoid A] [inst : DistribMulAction M A] :

↑1 = id

source

ink

theorem DistribMulActionHom.zero_apply {M : Type u_3} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_1} [inst : AddMonoid B] [inst : DistribMulAction M B] (a : A) :

↑0 a = 0

source

ink

theorem DistribMulActionHom.one_apply {M : Type u_2} [inst : Monoid M] {A : Type u_1} [inst : AddMonoid A] [inst : DistribMulAction M A] (a : A) :

↑1 a = a

source

ink

instance DistribMulActionHom.instInhabitedDistribMulActionHom {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] :

Inhabited (A →+[M] B)

Equations

DistribMulActionHom.instInhabitedDistribMulActionHom = { default := 0 }

source

ink

def DistribMulActionHom.comp {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] {C : Type u_4} [inst : AddMonoid C] [inst : 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.

source

ink

@[simp]

theorem DistribMulActionHom.comp_apply {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_2} [inst : AddMonoid B] [inst : DistribMulAction M B] {C : Type u_3} [inst : AddMonoid C] [inst : DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :

↑(DistribMulActionHom.comp g f) x = ↑g (↑f x)

source

ink

@[simp]

theorem DistribMulActionHom.id_comp {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

DistribMulActionHom.comp (DistribMulActionHom.id M) f = f

source

ink

@[simp]

theorem DistribMulActionHom.comp_id {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : DistribMulAction M B] (f : A →+[M] B) :

DistribMulActionHom.comp f (DistribMulActionHom.id M) = f

source

ink

@[simp]

theorem DistribMulActionHom.inverse_toFun {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : 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

source

ink

def DistribMulActionHom.inverse {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : AddMonoid A] [inst : DistribMulAction M A] {B : Type u_3} [inst : AddMonoid B] [inst : 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.

source

ink

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

f = g

source

ink

theorem DistribMulActionHom.ext_ring_iff {M' : Type u_2} {R : Type u_1} [inst : Semiring R] [inst : AddMonoid M'] [inst : DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} :

f = g ↔ ↑f 1 = ↑g 1

source

ink

structure MulSemiringActionHom (M : Type u_1) [inst : Monoid M] (R : Type u_2) [inst : Semiring R] [inst : MulSemiringAction M R] (S : Type u_3) [inst : Semiring S] [inst : MulSemiringAction M S] extends DistribMulActionHom :

Type (maxu_2u_3)

The proposition that the function preserves 1
map_one' : MulActionHom.toFun toDistribMulActionHom.toMulActionHom 1 = 1
The proposition that the function preserves multiplication
map_mul' : ∀ (x y : R), MulActionHom.toFun toDistribMulActionHom.toMulActionHom (x * y) = MulActionHom.toFun toDistribMulActionHom.toMulActionHom x * MulActionHom.toFun toDistribMulActionHom.toMulActionHom y

Equivariant ring homomorphisms.

Instances For

source

ink

abbrev MulSemiringActionHom.toRingHom {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : 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.

source

ink

def «MulSemiringActionHomLocal≺» :

Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

source

ink

class MulSemiringActionHomClass (F : Type u_1) (M : outParam (Type u_2)) (R : outParam (Type u_3)) (S : outParam (Type u_4)) [inst : Monoid M] [inst : Semiring R] [inst : Semiring S] [inst : DistribMulAction M R] [inst : DistribMulAction M S] extends DistribMulActionHomClass :

Type (max(maxu_1u_3)u_4)

The proposition that the function preserves multiplication
map_mul : ∀ (f : F) (x y : R), ↑f (x * y) = ↑f x * ↑f y
The proposition that the function preserves 1
map_one : ∀ (f : F), ↑f 1 = 1

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.

Instances

source

ink

instance MulSemiringActionHom.instMulSemiringActionHomClassMulSemiringActionHomToDistribMulActionToDistribMulAction (M : Type u_1) [inst : Monoid M] (R : Type u_2) [inst : Semiring R] [inst : MulSemiringAction M R] (S : Type u_3) [inst : Semiring S] [inst : MulSemiringAction M S] :

MulSemiringActionHomClass (R →+*[M] S) M R S

Equations

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

source

ink

def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] {F : Type u_4} [inst : 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.

source

ink

instance MulSemiringActionHom.instCoeTCMulSemiringActionHom {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] {F : Type u_4} [inst : 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 }

source

ink

theorem MulSemiringActionHom.coe_fn_coe {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

↑↑f = ↑f

source

ink

theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

↑↑f = ↑f

source

ink

theorem MulSemiringActionHom.ext {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :

(∀ (x : R), ↑f x = ↑g x) → f = g

source

ink

theorem MulSemiringActionHom.ext_iff {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :

f = g ↔ ∀ (x : R), ↑f x = ↑g x

source

ink

theorem MulSemiringActionHom.map_zero {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

↑f 0 = 0

source

ink

theorem MulSemiringActionHom.map_add {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :

↑f (x + y) = ↑f x + ↑f y

source

ink

theorem MulSemiringActionHom.map_neg {M : Type u_1} [inst : Monoid M] (R' : Type u_2) [inst : Ring R'] [inst : MulSemiringAction M R'] (S' : Type u_3) [inst : Ring S'] [inst : MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') :

↑f (-x) = -↑f x

source

ink

theorem MulSemiringActionHom.map_sub {M : Type u_1} [inst : Monoid M] (R' : Type u_2) [inst : Ring R'] [inst : MulSemiringAction M R'] (S' : Type u_3) [inst : Ring S'] [inst : MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') (y : R') :

↑f (x - y) = ↑f x - ↑f y

source

ink

theorem MulSemiringActionHom.map_one {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

↑f 1 = 1

source

ink

theorem MulSemiringActionHom.map_mul {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :

↑f (x * y) = ↑f x * ↑f y

source

ink

theorem MulSemiringActionHom.map_smul {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) :

↑f (m • x) = m • ↑f x

source

ink

def MulSemiringActionHom.id (M : Type u_1) [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : 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.

source

ink

@[simp]

theorem MulSemiringActionHom.id_apply (M : Type u_2) [inst : Monoid M] {R : Type u_1} [inst : Semiring R] [inst : MulSemiringAction M R] (x : R) :

↑(MulSemiringActionHom.id M) x = x

source

ink

def MulSemiringActionHom.comp {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] {T : Type u_4} [inst : Semiring T] [inst : 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.

source

ink

@[simp]

theorem MulSemiringActionHom.comp_apply {M : Type u_1} [inst : Monoid M] {R : Type u_4} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_2} [inst : Semiring S] [inst : MulSemiringAction M S] {T : Type u_3} [inst : Semiring T] [inst : MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :

↑(MulSemiringActionHom.comp g f) x = ↑g (↑f x)

source

ink

@[simp]

theorem MulSemiringActionHom.id_comp {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

MulSemiringActionHom.comp (MulSemiringActionHom.id M) f = f

source

ink

@[simp]

theorem MulSemiringActionHom.comp_id {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst : Semiring R] [inst : MulSemiringAction M R] {S : Type u_3} [inst : Semiring S] [inst : MulSemiringAction M S] (f : R →+*[M] S) :

MulSemiringActionHom.comp f (MulSemiringActionHom.id M) = f