Equivariant homomorphisms #

Main definitions #

MulActionHom φ X Y, the type of equivariant functions from X to Y, where φ : M → N is a map, M acting on the type X and N acting on the type of Y. AddActionHom φ X Y is its additive version.
DistribMulActionHom φ A B, the type of equivariant additive monoid homomorphisms from A to B, where φ : M → N is a morphism of monoids, M acting on the additive monoid A and N acting on the additive monoid of B
SMulSemiringHom φ R S, the type of equivariant ring homomorphisms from R to S, where φ : M → N is a morphism of monoids, M acting on the ring R and N acting on the ring S.

The above types have corresponding classes:

MulActionHomClass F φ X Y states that F is a type of bundled X → Y homs which are φ-equivariant; AddActionHomClass F φ X Y is its additive version.
DistribMulActionHomClass F φ A B states that F is a type of bundled A → B homs preserving the additive monoid structure and φ-equivariant
SMulSemiringHomClass F φ R S states that F is a type of bundled R → S homs preserving the ring structure and φ-equivariant

Notation #

We introduce the following notation to code equivariant maps (the subscript index ₑ is for equivariant) :

X →ₑ[φ] Y is MulActionHom φ X Y and AddActionHom φ X Y
A →ₑ+[φ] B is DistribMulActionHom φ A B.
R →ₑ+*[φ] S is MulSemiringActionHom φ R S.

When M = N and φ = MonoidHom.id M, we provide the backward compatible notation :

X →[M] Y is MulActionHom (@id M) X Y and AddActionHom (@id M) X Y
A →+[M] B is DistribMulActionHom (MonoidHom.id M) A B
R →+*[M] S is MulSemiringActionHom (MonoidHom.id M) R S

The notation for MulActionHom and AddActionHom is the same, because it is unlikely that it could lead to confusion — unless one needs types M and X with simultaneous instances of Mul M, Add M, SMul M X and VAdd M X…

source

structure AddActionHom {M : Type u_8} {N : Type u_9} (φ : M → N) (X : Type u_10) [VAdd M X] (Y : Type u_11) [VAdd N Y] :

Type (max u_10 u_11)

Equivariant functions : When φ : M → N is a function, and types X and Y are endowed with additive actions of M and N, a function f : X → Y is φ-equivariant if f (m +ᵥ x) = (φ m) +ᵥ (f x).

toFun : X → Y
The underlying function.
map_vadd' (m : M) (x : X) : self.toFun (m +ᵥ x) = φ m +ᵥ self.toFun x
The proposition that the function commutes with the additive actions.

source

structure MulActionHom {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :

Type (max u_5 u_6)

Equivariant functions : When φ : M → N is a function, and types X and Y are endowed with actions of M and N, a function f : X → Y is φ-equivariant if f (m • x) = (φ m) • (f x).

toFun : X → Y
The underlying function.
map_smul' (m : M) (x : X) : self.toFun (m • x) = φ m • self.toFun x
The proposition that the function commutes with the actions.

source

def «MulActionHomLocal≺» :

Lean.TrailingParserDescr

φ-equivariant functions X → Y, where φ : M → N, where M and N act on X and Y respectively.

Equations

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

source

def «MulActionHomIdLocal≺» :

Lean.TrailingParserDescr

M-equivariant functions X → Y with respect to the action of M. This is the same as X →ₑ[@id M] Y.

Equations

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

source

def «AddActionHomLocal≺» :

Lean.TrailingParserDescr

φ-equivariant functions X → Y, where φ : M → N, where M and N act additively on X and Y respectively

We use the same notation as for multiplicative actions, as conflicts are unlikely.

Equations

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

source

def «AddActionHomIdLocal≺» :

Lean.TrailingParserDescr

M-equivariant functions X → Y with respect to the additive action of M. This is the same as X →ₑ[@id M] Y.

We use the same notation as for multiplicative actions, as conflicts are unlikely.

Equations

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

source

class AddActionSemiHomClass (F : Type u_8) {M : outParam (Type u_9)} {N : outParam (Type u_10)} (φ : outParam (M → N)) (X : outParam (Type u_11)) (Y : outParam (Type u_12)) [VAdd M X] [VAdd N Y] [FunLike F X Y] :

Prop

AddActionSemiHomClass F φ X Y states that F is a type of morphisms which are φ-equivariant.

You should extend this class when you extend AddActionHom.

map_vaddₛₗ (f : F) (c : M) (x : X) : f (c +ᵥ x) = φ c +ᵥ f x
The proposition that the function preserves the action.

Instances

source

class MulActionSemiHomClass (F : Type u_8) {M : outParam (Type u_9)} {N : outParam (Type u_10)} (φ : outParam (M → N)) (X : outParam (Type u_11)) (Y : outParam (Type u_12)) [SMul M X] [SMul N Y] [FunLike F X Y] :

Prop

MulActionSemiHomClass F φ X Y states that F is a type of morphisms which are φ-equivariant.

You should extend this class when you extend MulActionHom.

map_smulₛₗ (f : F) (c : M) (x : X) : f (c • x) = φ c • f x
The proposition that the function preserves the action.

Instances

source

@[reducible, inline]

abbrev MulActionHomClass (F : Type u_8) (M : outParam (Type u_9)) (X : outParam (Type u_10)) (Y : outParam (Type u_11)) [SMul M X] [SMul M Y] [FunLike F X Y] :

Prop

MulActionHomClass F M X Y states that F is a type of morphisms which are equivariant with respect to actions of M This is an abbreviation of MulActionSemiHomClass.

Equations

MulActionHomClass F M X Y = MulActionSemiHomClass F id X Y

source

@[reducible, inline]

abbrev AddActionHomClass (F : Type u_8) (M : outParam (Type u_9)) (X : outParam (Type u_10)) (Y : outParam (Type u_11)) [VAdd M X] [VAdd M Y] [FunLike F X Y] :

Prop

MulActionHomClass F M X Y states that F is a type of morphisms which are equivariant with respect to actions of M This is an abbreviation of MulActionSemiHomClass.

Equations

AddActionHomClass F M X Y = AddActionSemiHomClass F id X Y

source

instance instFunLikeMulActionHom {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :

FunLike (X →ₑ[φ] Y) X Y

Equations

instFunLikeMulActionHom φ X Y = { coe := MulActionHom.toFun, coe_injective' := ⋯ }

source

instance instFunLikeAddActionHom {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [VAdd M X] (Y : Type u_6) [VAdd N Y] :

FunLike (X →ₑ[φ] Y) X Y

Equations

instFunLikeAddActionHom φ X Y = { coe := AddActionHom.toFun, coe_injective' := ⋯ }

source

@[simp]

theorem map_smul {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [SMul M X] [SMul M Y] [FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M) (x : X) :

f (c • x) = c • f x

source

@[simp]

theorem map_vadd {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [VAdd M X] [VAdd M Y] [FunLike F X Y] [AddActionHomClass F M X Y] (f : F) (c : M) (x : X) :

f (c +ᵥ x) = c +ᵥ f x

source

instance instMulActionSemiHomClassMulActionHom {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [SMul M X] (Y : Type u_6) [SMul N Y] :

MulActionSemiHomClass (X →ₑ[φ] Y) φ X Y

source

instance instAddActionSemiHomClassAddActionHom {M : Type u_2} {N : Type u_3} (φ : M → N) (X : Type u_5) [VAdd M X] (Y : Type u_6) [VAdd N Y] :

AddActionSemiHomClass (X →ₑ[φ] Y) φ X Y

source

def MulActionSemiHomClass.toMulActionHom {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {F : Type u_8} [FunLike F X Y] [MulActionSemiHomClass F φ X Y] (f : F) :

X →ₑ[φ] Y

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

Equations

↑f = { toFun := ⇑f, map_smul' := ⋯ }

source

def AddActionSemiHomClass.toAddActionHom {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {F : Type u_8} [FunLike F X Y] [AddActionSemiHomClass F φ X Y] (f : F) :

X →ₑ[φ] Y

Turn an element of a type F satisfying AddActionSemiHomClass F φ X Y into an actual AddActionHom. This is declared as the default coercion from F to AddActionSemiHom φ X Y.

Equations

↑f = { toFun := ⇑f, map_vadd' := ⋯ }

source

instance MulActionHom.instCoeTCOfMulActionSemiHomClass {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {F : Type u_8} [FunLike F X Y] [MulActionSemiHomClass F φ X Y] :

CoeTC F (X →ₑ[φ] Y)

Any type satisfying MulActionSemiHomClass can be cast into MulActionHom via MulActionHomSemiClass.toMulActionHom.

Equations

MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }

source

instance AddActionHom.instCoeTCOfAddActionSemiHomClass {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {F : Type u_8} [FunLike F X Y] [AddActionSemiHomClass F φ X Y] :

CoeTC F (X →ₑ[φ] Y)

Equations

AddActionHom.instCoeTCOfAddActionSemiHomClass = { coe := AddActionSemiHomClass.toAddActionHom }

source

theorem IsScalarTower.smulHomClass (M' : Type u_1) (X : Type u_5) [SMul M' X] (Y : Type u_6) [SMul M' Y] (F : Type u_8) [FunLike F X Y] [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [MulActionHomClass F X X Y] :

MulActionHomClass F M' X Y

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

source

theorem VAddAssocClass.vaddHomClass (M' : Type u_1) (X : Type u_5) [VAdd M' X] (Y : Type u_6) [VAdd M' Y] (F : Type u_8) [FunLike F X Y] [AddZeroClass X] [VAdd X Y] [VAddAssocClass M' X Y] [AddActionHomClass F X X Y] :

AddActionHomClass F M' X Y

source

theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_5} [SMul M' X] {Y : Type u_6} [SMul M' Y] (f : X →ₑ[id ] Y) (m : M') (x : X) :

f (m • x) = m • f x

source

theorem AddActionHom.map_vadd {M' : Type u_1} {X : Type u_5} [VAdd M' X] {Y : Type u_6} [VAdd M' Y] (f : X →ₑ[id ] Y) (m : M') (x : X) :

f (m +ᵥ x) = m +ᵥ f x

source

theorem MulActionHom.ext {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {f g : X →ₑ[φ] Y} :

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

source

theorem AddActionHom.ext {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {f g : X →ₑ[φ] Y} :

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

source

theorem AddActionHom.ext_iff {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {f g : X →ₑ[φ] Y} :

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

source

theorem MulActionHom.ext_iff {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {f g : X →ₑ[φ] Y} :

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

source

theorem MulActionHom.congr_fun {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {f g : X →ₑ[φ] Y} (h : f = g) (x : X) :

f x = g x

source

theorem AddActionHom.congr_fun {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {f g : X →ₑ[φ] Y} (h : f = g) (x : X) :

f x = g x

source

def MulActionHom.ofEq {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :

X →ₑ[φ'] Y

Two equal maps on scalars give rise to an equivariant map for identity

Equations

MulActionHom.ofEq h f = { toFun := f.toFun, map_smul' := ⋯ }

source

def AddActionHom.ofEq {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :

X →ₑ[φ'] Y

Two equal maps on scalars give rise to an equivariant map for identity

Equations

AddActionHom.ofEq h f = { toFun := f.toFun, map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.ofEq_coe {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :

(ofEq h f).toFun = f.toFun

source

@[simp]

theorem AddActionHom.ofEq_coe {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :

(ofEq h f).toFun = f.toFun

source

@[simp]

theorem MulActionHom.ofEq_apply {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :

(ofEq h f) a = f a

source

@[simp]

theorem AddActionHom.ofEq_apply {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :

(ofEq h f) a = f a

source

theorem FaithfulSMul.of_injective {M' : Type u_1} {X : Type u_5} [SMul M' X] {Y : Type u_6} [SMul M' Y] {F : Type u_8} [FunLike F X Y] [FaithfulSMul M' X] [MulActionHomClass F M' X Y] (f : F) (hf : Function.Injective ⇑f) :

FaithfulSMul M' Y

source

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

X →ₑ[id ] X

The identity map as an equivariant map.

Equations

MulActionHom.id M = { toFun := id, map_smul' := ⋯ }

source

def AddActionHom.id (M : Type u_2) {X : Type u_5} [VAdd M X] :

X →ₑ[id ] X

The identity map as an equivariant map.

Equations

AddActionHom.id M = { toFun := id, map_vadd' := ⋯ }

source

@[simp]

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

(MulActionHom.id M) x = x

source

@[simp]

theorem AddActionHom.id_apply {M : Type u_2} {X : Type u_5} [VAdd M X] (x : X) :

(AddActionHom.id M) x = x

source

def MulActionHom.comp {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :

X →ₑ[χ] Z

Composition of two equivariant maps.

Equations

g.comp f = { toFun := ⇑g ∘ ⇑f, map_smul' := ⋯ }

source

def AddActionHom.comp {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :

X →ₑ[χ] Z

Composition of two equivariant maps.

Equations

g.comp f = { toFun := ⇑g ∘ ⇑f, map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.comp_apply {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :

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

source

@[simp]

theorem AddActionHom.comp_apply {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :

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

source

@[simp]

theorem MulActionHom.id_comp {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] (f : X →ₑ[φ] Y) :

(MulActionHom.id N).comp f = f

source

@[simp]

theorem AddActionHom.id_comp {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] (f : X →ₑ[φ] Y) :

(AddActionHom.id N).comp f = f

source

@[simp]

theorem MulActionHom.comp_id {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] (f : X →ₑ[φ] Y) :

f.comp (MulActionHom.id M) = f

source

@[simp]

theorem AddActionHom.comp_id {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] (f : X →ₑ[φ] Y) :

f.comp (AddActionHom.id M) = f

source

@[simp]

theorem MulActionHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {Z : Type u_7} [SMul P Z] {Q : Type u_8} {T : Type u_9} [SMul Q T] {η : P → Q} {θ : M → Q} {ζ : N → Q} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] [CompTriple χ η θ] [CompTriple ψ η ζ] [CompTriple φ ζ θ] :

h.comp (g.comp f) = (h.comp g).comp f

source

@[simp]

theorem AddActionHom.comp_assoc {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {Z : Type u_7} [VAdd P Z] {Q : Type u_8} {T : Type u_9} [VAdd Q T] {η : P → Q} {θ : M → Q} {ζ : N → Q} (h : Z →ₑ[η] T) (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] [CompTriple χ η θ] [CompTriple ψ η ζ] [CompTriple φ ζ θ] :

h.comp (g.comp f) = (h.comp g).comp f

source

def MulActionHom.inverse {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

Y₁ →ₑ[id ] X

The inverse of a bijective equivariant map is equivariant.

Equations

f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯ }

source

def AddActionHom.inverse {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

Y₁ →ₑ[id ] X

The inverse of a bijective equivariant map is equivariant.

Equations

f.inverse g h₁ h₂ = { toFun := g, map_vadd' := ⋯ }

source

@[simp]

theorem AddActionHom.inverse_apply {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : Y₁) :

(f.inverse g h₁ h₂) a✝ = g a✝

source

@[simp]

theorem MulActionHom.inverse_apply {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : Y₁) :

(f.inverse g h₁ h₂) a✝ = g a✝

source

def MulActionHom.inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

Y →ₑ[φ'] X

The inverse of a bijective equivariant map is equivariant.

Equations

f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := ⋯ }

source

def AddActionHom.inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

Y →ₑ[φ'] X

The inverse of a bijective equivariant map is equivariant.

Equations

f.inverse' g k h₁ h₂ = { toFun := g, map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.inverse'_apply {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : Y) :

(f.inverse' g k h₁ h₂) a✝ = g a✝

source

@[simp]

theorem AddActionHom.inverse'_apply {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : Y) :

(f.inverse' g k h₁ h₂) a✝ = g a✝

source

theorem MulActionHom.inverse_eq_inverse' {M : Type u_2} {X : Type u_5} [SMul M X] {Y₁ : Type u_8} [SMul M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

source

theorem AddActionHom.inverse_eq_inverse' {M : Type u_2} {X : Type u_5} [VAdd M X] {Y₁ : Type u_8} [VAdd M Y₁] (f : X →ₑ[id ] Y₁) (g : Y₁ → X) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

source

theorem MulActionHom.inverse'_inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

(f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f

source

theorem AddActionHom.inverse'_inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

(f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f

source

theorem MulActionHom.comp_inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

(f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M

source

theorem AddActionHom.comp_inverse' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

(f.inverse' g k₂ h₁ h₂).comp f = AddActionHom.id M

source

theorem MulActionHom.inverse'_comp {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N

source

theorem AddActionHom.inverse'_comp {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [VAdd M X] {Y : Type u_6} [VAdd N Y] {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₂ : Function.RightInverse φ' φ} {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f} :

f.comp (f.inverse' g k₂ h₁ h₂) = AddActionHom.id N

source

def SMulCommClass.toMulActionHom {M : Type u_11} (N : Type u_9) (α : Type u_10) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :

α →ₑ[id ] α

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' := ⋯ }

source

def VAddCommClass.toAddActionHom {M : Type u_11} (N : Type u_9) (α : Type u_10) [VAdd M α] [VAdd N α] [VAddCommClass M N α] (c : M) :

α →ₑ[id ] α

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

Equations

VAddCommClass.toAddActionHom N α c = { toFun := fun (x : α) => c +ᵥ x, map_vadd' := ⋯ }

source

@[simp]

theorem VAddCommClass.toAddActionHom_apply {M : Type u_11} (N : Type u_9) (α : Type u_10) [VAdd M α] [VAdd N α] [VAddCommClass M N α] (c : M) (x✝ : α) :

(toAddActionHom N α c) x✝ = c +ᵥ x✝

source

@[simp]

theorem SMulCommClass.toMulActionHom_apply {M : Type u_11} (N : Type u_9) (α : Type u_10) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) (x✝ : α) :

(toMulActionHom N α c) x✝ = c • x✝

source

def Pi.evalMulActionHom {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [(i : ι) → SMul M (X i)] (i : ι) :

((i : ι) → X i) →ₑ[id ] X i

Evaluation at a point as a MulActionHom.

Equations

Pi.evalMulActionHom i = { toFun := Function.eval i, map_smul' := ⋯ }

source

def Pi.evalAddActionHom {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [(i : ι) → VAdd M (X i)] (i : ι) :

((i : ι) → X i) →ₑ[id ] X i

Evaluation at a point as an AddActionHom.

Equations

Pi.evalAddActionHom i = { toFun := Function.eval i, map_vadd' := ⋯ }

source

@[simp]

theorem Pi.evalMulActionHom_apply {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [(i : ι) → SMul M (X i)] (i : ι) (f : (x : ι) → X x) :

(evalMulActionHom i) f = Function.eval i f

source

@[simp]

theorem Pi.evalAddActionHom_apply {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [(i : ι) → VAdd M (X i)] (i : ι) (f : (x : ι) → X x) :

(evalAddActionHom i) f = Function.eval i f

source

def MulActionHom.fst (M : Type u_1) (α : Type u_2) (β : Type u_3) [SMul M α] [SMul M β] :

α × β →ₑ[id ] α

Prod.fst as a bundled MulActionHom.

Equations

MulActionHom.fst M α β = { toFun := Prod.fst, map_smul' := ⋯ }

source

def AddActionHom.fst (M : Type u_1) (α : Type u_2) (β : Type u_3) [VAdd M α] [VAdd M β] :

α × β →ₑ[id ] α

Prod.fst as a bundled AddActionHom.

Equations

AddActionHom.fst M α β = { toFun := Prod.fst, map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.fst_apply (M : Type u_1) (α : Type u_2) (β : Type u_3) [SMul M α] [SMul M β] :

⇑(fst M α β) = Prod.fst

source

@[simp]

theorem AddActionHom.fst_apply (M : Type u_1) (α : Type u_2) (β : Type u_3) [VAdd M α] [VAdd M β] :

⇑(fst M α β) = Prod.fst

source

def MulActionHom.snd (M : Type u_1) (α : Type u_2) (β : Type u_3) [SMul M α] [SMul M β] :

α × β →ₑ[id ] β

Prod.snd as a bundled MulActionHom.

Equations

MulActionHom.snd M α β = { toFun := Prod.snd, map_smul' := ⋯ }

source

def AddActionHom.snd (M : Type u_1) (α : Type u_2) (β : Type u_3) [VAdd M α] [VAdd M β] :

α × β →ₑ[id ] β

Prod.snd as a bundled AddActionHom.

Equations

AddActionHom.snd M α β = { toFun := Prod.snd, map_vadd' := ⋯ }

source

@[simp]

theorem AddActionHom.snd_apply (M : Type u_1) (α : Type u_2) (β : Type u_3) [VAdd M α] [VAdd M β] :

⇑(snd M α β) = Prod.snd

source

@[simp]

theorem MulActionHom.snd_apply (M : Type u_1) (α : Type u_2) (β : Type u_3) [SMul M α] [SMul M β] :

⇑(snd M α β) = Prod.snd

source

def MulActionHom.prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

α →ₑ[σ] γ × δ

If f and g are equivariant maps, then so is x ↦ (f x, g x).

Equations

f.prod g = { toFun := fun (x : α) => (f x, g x), map_smul' := ⋯ }

source

def AddActionHom.prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

α →ₑ[σ] γ × δ

If f and g are equivariant maps, then so is x ↦ (f x, g x).

Equations

f.prod g = { toFun := fun (x : α) => (f x, g x), map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.prod_apply {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

⇑(f.prod g) = fun (x : α) => (f x, g x)

source

@[simp]

theorem AddActionHom.prod_apply {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

⇑(f.prod g) = fun (x : α) => (f x, g x)

source

@[simp]

theorem MulActionHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

(fst N γ δ).comp (f.prod g) = f

source

@[simp]

theorem AddActionHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

(fst N γ δ).comp (f.prod g) = f

source

@[simp]

theorem MulActionHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

(snd N γ δ).comp (f.prod g) = g

source

@[simp]

theorem AddActionHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) :

(snd N γ δ).comp (f.prod g) = g

source

@[simp]

theorem MulActionHom.prod_fst_snd {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] :

(fst M α β).prod (snd M α β) = MulActionHom.id M

source

@[simp]

theorem AddActionHom.prod_fst_snd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] :

(fst M α β).prod (snd M α β) = AddActionHom.id M

source

def MulActionHom.prodMap {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul M β] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) :

α × β →ₑ[σ] γ × δ

If f and g are equivariant maps, then so is (x, y) ↦ (f x, g y).

Equations

f.prodMap g = { toFun := Prod.map ⇑f ⇑g, map_smul' := ⋯ }

source

def AddActionHom.prodMap {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd M β] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) :

α × β →ₑ[σ] γ × δ

If f and g are equivariant maps, then so is (x, y) ↦ (f x, g y).

Equations

f.prodMap g = { toFun := Prod.map ⇑f ⇑g, map_vadd' := ⋯ }

source

@[simp]

theorem MulActionHom.prodMap_apply {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul M β] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

@[simp]

theorem AddActionHom.prodMap_apply {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd M β] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) :

⇑(f.prodMap g) = Prod.map ⇑f ⇑g

source

structure DistribMulActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] extends A →ₑ[⇑φ] B, A →+ B :

Type (max u_4 u_5)

Equivariant additive monoid homomorphisms.

toFun : A → B
map_smul' (m : M) (x : A) : self.toFun (m • x) = φ m • self.toFun x
map_zero' : self.toFun 0 = 0
map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y

source

def «DistribMulActionHomLocal≺» :

Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

source

def «DistribMulActionHomIdLocal≺» :

Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

source

class DistribMulActionSemiHomClass (F : Type u_10) {M : outParam (Type u_11)} {N : outParam (Type u_12)} (φ : outParam (M → N)) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Monoid M] [Monoid N] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction N B] [FunLike F A B] extends MulActionSemiHomClass F φ A B, AddMonoidHomClass F A B :

Prop

DistribMulActionSemiHomClass F φ A B states that F is a type of morphisms preserving the additive monoid structure and equivariant with respect to φ. You should extend this class when you extend DistribMulActionSemiHom.

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
map_zero (f : F) : f 0 = 0

Instances

source

@[reducible, inline]

abbrev DistribMulActionHomClass (F : Type u_10) (M : outParam (Type u_11)) (A : outParam (Type u_12)) (B : outParam (Type u_13)) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] :

Prop

DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and equivariant with respect to the action of M. It is an abbreviation to DistribMulActionHomClass F (MonoidHom.id M) A B You should extend this class when you extend DistribMulActionHom.

Equations

DistribMulActionHomClass F M A B = DistribMulActionSemiHomClass F (⇑(MonoidHom.id M)) A B

source

instance DistribMulActionHom.instFunLike {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] :

FunLike (A →ₑ+[φ] B) A B

Equations

DistribMulActionHom.instFunLike φ A B = { coe := fun (m : A →ₑ+[φ] B) => m.toFun, coe_injective' := ⋯ }

source

instance DistribMulActionHom.instDistribMulActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] :

DistribMulActionSemiHomClass (A →ₑ+[φ] B) (⇑φ) A B

source

def DistribMulActionSemiHomClass.toDistribMulActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {F : Type u_10} [FunLike F A B] [DistribMulActionSemiHomClass F (⇑φ) A B] (f : F) :

A →ₑ+[φ] B

Turn an element of a type F satisfying MulActionHomClass 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).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

source

instance DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {F : Type u_10} [FunLike F A B] [DistribMulActionSemiHomClass F (⇑φ) A B] :

CoeTC F (A →ₑ+[φ] B)

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

Equations

DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom = { coe := DistribMulActionSemiHomClass.toDistribMulActionHom }

source

def SMulCommClass.toDistribMulActionHom {M : Type u_13} (N : Type u_11) (A : Type u_12) [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

SMulCommClass.toDistribMulActionHom N A c = { toFun := fun (x : A) => c • x, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem SMulCommClass.toDistribMulActionHom_toFun {M : Type u_13} (N : Type u_11) (A : Type u_12) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) (x✝ : A) :

(toDistribMulActionHom N A c) x✝ = c • x✝

source

@[simp]

theorem DistribMulActionHom.toFun_eq_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

f.toFun = ⇑f

source

theorem DistribMulActionHom.coe_fn_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

⇑↑f = ⇑f

source

theorem DistribMulActionHom.coe_fn_coe' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

⇑↑f = ⇑f

source

theorem DistribMulActionHom.ext {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} :

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

source

theorem DistribMulActionHom.ext_iff {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} :

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

source

theorem DistribMulActionHom.congr_fun {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : f = g) (x : A) :

f x = g x

source

theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : ↑f = ↑g) :

f = g

source

theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {f g : A →ₑ+[φ] B} (h : ↑f = ↑g) :

f = g

source

theorem DistribMulActionHom.map_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

f 0 = 0

source

theorem DistribMulActionHom.map_add {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) (x y : A) :

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

source

theorem DistribMulActionHom.map_neg {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (A' : Type u_8) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x : A') :

f (-x) = -f x

source

theorem DistribMulActionHom.map_sub {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (A' : Type u_8) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction N B'] (f : A' →ₑ+[φ] B') (x y : A') :

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

source

theorem DistribMulActionHom.map_smulₑ {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) (m : M) (x : A) :

f (m • x) = φ m • f x

source

def DistribMulActionHom.id (M : Type u_1) [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] :

A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Equations

DistribMulActionHom.id M = { toMulActionHom := MulActionHom.id M, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

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

(DistribMulActionHom.id M) x = x

source

instance DistribMulActionHom.instZero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :

Zero (A →ₑ+[φ] B)

Equations

DistribMulActionHom.instZero = { zero := let __src := 0; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }

source

instance DistribMulActionHom.instOneId {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] :

One (A →+[M] A)

Equations

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

source

@[simp]

theorem DistribMulActionHom.coe_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :

⇑0 = 0

source

@[simp]

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

⇑1 = id

source

theorem DistribMulActionHom.zero_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (a : A) :

0 a = 0

source

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

1 a = a

source

instance DistribMulActionHom.instInhabited {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] :

Inhabited (A →ₑ+[φ] B)

Equations

DistribMulActionHom.instInhabited = { default := 0 }

source

def DistribMulActionHom.comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [κ : φ.CompTriple ψ χ] :

A →ₑ+[χ] C

Composition of two equivariant additive monoid homomorphisms.

Equations

g.comp f = { toMulActionHom := (↑g).comp ↑f, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem DistribMulActionHom.comp_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [φ.CompTriple ψ χ] (x : A) :

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

source

@[simp]

theorem DistribMulActionHom.id_comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

(DistribMulActionHom.id N).comp f = f

source

@[simp]

theorem DistribMulActionHom.comp_id {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] (f : A →ₑ+[φ] B) :

f.comp (DistribMulActionHom.id M) = f

source

@[simp]

theorem DistribMulActionHom.comp_assoc {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B : Type u_5} [AddMonoid B] [DistribMulAction N B] {C : Type u_7} [AddMonoid C] [DistribMulAction P C] {Q : Type u_11} {D : Type u_12} [Monoid Q] [AddMonoid D] [DistribMulAction Q D] {η : P →* Q} {θ : M →* Q} {ζ : N →* Q} (h : C →ₑ+[η] D) (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [φ.CompTriple ψ χ] [χ.CompTriple η θ] [ψ.CompTriple η ζ] [φ.CompTriple ζ θ] :

h.comp (g.comp f) = (h.comp g).comp f

source

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

f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem DistribMulActionHom.inverse_toFun {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] {B₁ : Type u_6} [AddMonoid B₁] [DistribMulAction M B₁] (f : A →+[M] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : B₁) :

(f.inverse g h₁ h₂) a✝ = g a✝

source

theorem DistribMulActionHom.ext_ring {R : Type u_11} [Semiring R] {S : Type u_12} [Semiring S] {N' : Type u_14} [AddMonoid N'] [DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'} (h : f 1 = g 1) :

f = g

source

theorem DistribMulActionHom.ext_ring_iff {R : Type u_11} [Semiring R] {S : Type u_12} [Semiring S] {N' : Type u_14} [AddMonoid N'] [DistribMulAction S N'] {σ : R →* S} {f g : R →ₑ+[σ] N'} :

f = g ↔ f 1 = g 1

source

structure MulSemiringActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] extends R →ₑ+[φ] S, R →+* S :

Type (max u_10 u_12)

Equivariant ring homomorphisms.

toFun : R → S
map_smul' (m : M) (x : R) : self.toFun (m • x) = φ m • self.toFun x
map_zero' : self.toFun 0 = 0
map_add' (x y : R) : self.toFun (x + y) = self.toFun x + self.toFun y
map_one' : self.toFun 1 = 1
map_mul' (x y : R) : self.toFun (x * y) = self.toFun x * self.toFun y

source

def «MulSemiringActionHomLocal≺» :

Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

source

def «MulSemiringActionHomIdLocal≺» :

Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

source

class MulSemiringActionSemiHomClass (F : Type u_15) {M : outParam (Type u_16)} {N : outParam (Type u_17)} [Monoid M] [Monoid N] (φ : outParam (M → N)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction N S] [FunLike F R S] extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S :

Prop

MulSemiringActionHomClass F φ R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to φ.

You should extend this class when you extend MulSemiringActionHom.

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
map_one (f : F) : f 1 = 1

Instances

source

@[reducible, inline]

abbrev MulSemiringActionHomClass (F : Type u_15) {M : outParam (Type u_16)} [Monoid M] (R : outParam (Type u_17)) (S : outParam (Type u_18)) [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction M S] [FunLike F R S] :

Prop

MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to a DistribMulActionof M on R and S .

Equations

MulSemiringActionHomClass F R S = MulSemiringActionSemiHomClass F (⇑(MonoidHom.id M)) R S

source

instance MulSemiringActionHom.instFunLike {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] :

FunLike (R →ₑ+*[φ] S) R S

Equations

MulSemiringActionHom.instFunLike φ R S = { coe := fun (m : R →ₑ+*[φ] S) => m.toFun, coe_injective' := ⋯ }

source

instance MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] :

MulSemiringActionSemiHomClass (R →ₑ+*[φ] S) (⇑φ) R S

source

def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {F : Type u_15} [FunLike F R S] [MulSemiringActionSemiHomClass F (⇑φ) R S] (f : F) :

R →ₑ+*[φ] 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

↑f = { toFun := (↑↑↑f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

source

instance MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {F : Type u_15} [FunLike F R S] [MulSemiringActionSemiHomClass F (⇑φ) R S] :

CoeTC F (R →ₑ+*[φ] S)

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

Equations

MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }

source

theorem MulSemiringActionHom.coe_fn_coe {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

⇑↑f = ⇑f

source

theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

⇑↑f = ⇑f

source

theorem MulSemiringActionHom.ext {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {f g : R →ₑ+*[φ] S} :

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

source

theorem MulSemiringActionHom.ext_iff {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {f g : R →ₑ+*[φ] S} :

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

source

theorem MulSemiringActionHom.map_zero {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

f 0 = 0

source

theorem MulSemiringActionHom.map_add {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (x y : R) :

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

source

theorem MulSemiringActionHom.map_neg {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (R' : Type u_11) [Ring R'] [MulSemiringAction M R'] (S' : Type u_13) [Ring S'] [MulSemiringAction N S'] (f : R' →ₑ+*[φ] S') (x : R') :

f (-x) = -f x

source

theorem MulSemiringActionHom.map_sub {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} (R' : Type u_11) [Ring R'] [MulSemiringAction M R'] (S' : Type u_13) [Ring S'] [MulSemiringAction N S'] (f : R' →ₑ+*[φ] S') (x y : R') :

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

source

theorem MulSemiringActionHom.map_one {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

f 1 = 1

source

theorem MulSemiringActionHom.map_mul {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (x y : R) :

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

source

theorem MulSemiringActionHom.map_smulₛₗ {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (m : M) (x : R) :

f (m • x) = φ m • f x

source

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

f (m • x) = m • f x

source

def MulSemiringActionHom.id (M : Type u_1) [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] :

R →+*[M] R

The identity map as an equivariant ring homomorphism.

Equations

MulSemiringActionHom.id M = { toDistribMulActionHom := DistribMulActionHom.id M, map_one' := ⋯, map_mul' := ⋯ }

source

@[simp]

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

(MulSemiringActionHom.id M) x = x

source

def MulSemiringActionHom.comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {T : Type u_14} [Semiring T] [MulSemiringAction P T] (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [κ : φ.CompTriple ψ χ] :

R →ₑ+*[χ] T

Composition of two equivariant additive ring homomorphisms.

Equations

g.comp f = { toDistribMulActionHom := (↑g).comp ↑f, map_one' := ⋯, map_mul' := ⋯ }

source

@[simp]

theorem MulSemiringActionHom.comp_apply {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {P : Type u_3} [Monoid P] {φ : M →* N} {ψ : N →* P} {χ : M →* P} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] {T : Type u_14} [Semiring T] [MulSemiringAction P T] (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [φ.CompTriple ψ χ] (x : R) :

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

source

@[simp]

theorem MulSemiringActionHom.id_comp {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

(MulSemiringActionHom.id N).comp f = f

source

@[simp]

theorem MulSemiringActionHom.comp_id {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) :

f.comp (MulSemiringActionHom.id M) = f

source

def MulSemiringActionHom.inverse' {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {φ' : N →* M} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (g : S → R) (k : Function.RightInverse ⇑φ' ⇑φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

S →ₑ+*[φ'] R

The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

Equations

f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

source

@[simp]

theorem MulSemiringActionHom.inverse'_toFun {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] {φ : M →* N} {φ' : N →* M} {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S : Type u_12} [Semiring S] [MulSemiringAction N S] (f : R →ₑ+*[φ] S) (g : S → R) (k : Function.RightInverse ⇑φ' ⇑φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : S) :

(f.inverse' g k h₁ h₂) a✝ = g a✝

source

def MulSemiringActionHom.inverse {M : Type u_1} [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S₁ : Type u_15} [Semiring S₁] [MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁ → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :

S₁ →+*[M] R

The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

Equations

f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

source

@[simp]

theorem MulSemiringActionHom.inverse_toFun {M : Type u_1} [Monoid M] {R : Type u_10} [Semiring R] [MulSemiringAction M R] {S₁ : Type u_15} [Semiring S₁] [MulSemiringAction M S₁] (f : R →+*[M] S₁) (g : S₁ → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a✝ : S₁) :

(f.inverse g h₁ h₂) a✝ = g a✝

Documentation

Mathlib.GroupTheory.GroupAction.Hom

Equivariant homomorphisms #

Main definitions #

Notation #