Equivariant homomorphisms #
Main definitions #
MulActionHom φ X Y, the type of equivariant functions fromXtoY, whereφ : M → Nis a map,Macting on the typeXandNacting on the type ofY.DistribMulActionHom φ A B, the type of equivariant additive monoid homomorphisms fromAtoB, whereφ : M → Nis a morphism of monoids,Macting on the additive monoidAandNacting on the additive monoid ofBSMulSemiringHom φ R S, the type of equivariant ring homomorphisms fromRtoS, whereφ : M → Nis a morphism of monoids,Macting on the ringRandNacting on the ringS.
The above types have corresponding classes:
MulActionHomClass F φ X Ystates thatFis a type of bundledX → Yhoms which areφ-equivariantDistribMulActionHomClass F φ A Bstates thatFis a type of bundledA → Bhoms preserving the additive monoid structure andφ-equivariantSMulSemiringHomClass F φ R Sstates thatFis a type of bundledR → Shoms preserving the ring structure andφ-equivariant
Notation #
We introduce the following notation to code equivariant maps
(the subscript index ₑ is for equivariant) :
X →ₑ[φ] YisMulActionHom φ X Y.A →ₑ+[φ] BisDistribMulActionHom φ A B.R →ₑ+*[φ] SisMulSemiringActionHom φ R S.
When M = N and φ = MonoidHom.id M, we provide the backward compatible notation :
X →[M] YisMulActionHom (@id M) X YA →+[M] BisDistribMulActionHom (MonoidHom.id M) A BR →+*[M] SisMulSemiringActionHom (MonoidHom.id M) R S
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.
The proposition that the function commutes with the actions.
φ-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.
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.
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]
:
MulActionSemiHomClass F φ X Y states that
F is a type of morphisms which are φ-equivariant.
You should extend this class when you extend MulActionHom.
The proposition that the function preserves the action.
Instances
@[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]
:
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
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)
:
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' := ⋯ }
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]
:
Any type satisfying MulActionSemiHomClass can be cast into MulActionHom via
MulActionHomSemiClass.toMulActionHom.
Equations
- MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }
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.
The identity map as an equivariant map.
Equations
- MulActionHom.id M = { toFun := id, map_smul' := ⋯ }
@[simp]
theorem
MulActionHom.id_apply
{M : Type u_2}
{X : Type u_5}
[SMul M X]
(x : X)
:
(MulActionHom.id M) x = x
@[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
@[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
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)
:
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯ }
@[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
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)
:
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := ⋯ }
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₂
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
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
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
@[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 : α), (SMulCommClass.toMulActionHom N α c) x = c • x
def
SMulCommClass.toMulActionHom
{M : Type u_11}
(N : Type u_9)
(α : Type u_10)
[SMul M α]
[SMul N α]
[SMulCommClass M N α]
(c : M)
:
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' := ⋯ }
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
MulActionHom
:
Type (max u_4 u_5)
Equivariant additive monoid homomorphisms.
- toFun : A → B
- map_zero' : self.toFun 0 = 0
The proposition that the function preserves 0
The proposition that the function preserves addition
@[reducible]
abbrev
DistribMulActionHom.toAddMonoidHom
{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]
(self : A →ₑ+[φ] B)
:
A →+ B
Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.
Equations
- self.toAddMonoidHom = { toFun := self.toFun, map_zero' := ⋯, map_add' := ⋯ }
Equivariant additive monoid homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Equivariant additive monoid homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
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
,
AddMonoidHomClass
:
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.
Instances
@[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]
:
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
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]
:
Equations
- DistribMulActionHom.instFunLike φ A B = { coe := fun (m : A →ₑ+[φ] B) => m.toFun, coe_injective' := ⋯ }
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
Equations
- ⋯ = ⋯
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)
:
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' := ⋯ }
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]
:
Any type satisfying MulActionHomClass can be cast into MulActionHom
via MulActionHomClass.toMulActionHom.
Equations
- DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom = { coe := DistribMulActionSemiHomClass.toDistribMulActionHom }
@[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), (SMulCommClass.toDistribMulActionHom N A c) x = c • x
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)
:
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' := ⋯ }
def
DistribMulActionHom.id
(M : Type u_1)
[Monoid M]
{A : Type u_4}
[AddMonoid A]
[DistribMulAction M A]
:
The identity map as an equivariant additive monoid homomorphism.
Equations
- DistribMulActionHom.id M = { toMulActionHom := MulActionHom.id M, map_zero' := ⋯, map_add' := ⋯ }
@[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
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]
:
Equations
- DistribMulActionHom.instZero = { zero := let __src := 0; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }
instance
DistribMulActionHom.instOneId
{M : Type u_1}
[Monoid M]
{A : Type u_4}
[AddMonoid A]
[DistribMulAction M A]
:
Equations
- DistribMulActionHom.instOneId = { one := DistribMulActionHom.id M }
@[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
@[simp]
theorem
DistribMulActionHom.coe_one
{M : Type u_1}
[Monoid M]
{A : Type u_4}
[AddMonoid A]
[DistribMulAction M A]
:
⇑1 = id
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
theorem
DistribMulActionHom.one_apply
{M : Type u_1}
[Monoid M]
{A : Type u_4}
[AddMonoid A]
[DistribMulAction M A]
(a : A)
:
1 a = a
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]
:
Equations
- DistribMulActionHom.instInhabited = { default := 0 }
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 ψ χ]
:
Composition of two equivariant additive monoid homomorphisms.
Equations
- g.comp f = { toMulActionHom := (↑g).comp ↑f, map_zero' := ⋯, map_add' := ⋯ }
@[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)
@[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
@[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
@[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
@[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
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)
:
The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
DistribMulActionHom
:
Type (max u_10 u_12)
Equivariant ring homomorphisms.
@[reducible]
abbrev
MulSemiringActionHom.toRingHom
{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]
(self : R →ₑ+*[φ] S)
:
R →+* S
Reinterpret an equivariant ring homomorphism as a ring homomorphism.
Equations
- self.toRingHom = { toFun := self.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Equivariant ring homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Equivariant ring homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
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
,
MonoidHomClass
:
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.
Instances
@[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]
:
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
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]
:
Equations
- MulSemiringActionHom.instFunLike φ R S = { coe := fun (m : R →ₑ+*[φ] S) => m.toFun, coe_injective' := ⋯ }
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
Equations
- ⋯ = ⋯
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)
:
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' := ⋯ }
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]
:
Any type satisfying MulSemiringActionHomClass can be cast into MulSemiringActionHom via
MulSemiringActionHomClass.toMulSemiringActionHom.
Equations
- MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }
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)
:
def
MulSemiringActionHom.id
(M : Type u_1)
[Monoid M]
{R : Type u_10}
[Semiring R]
[MulSemiringAction M R]
:
The identity map as an equivariant ring homomorphism.
Equations
- MulSemiringActionHom.id M = { toDistribMulActionHom := DistribMulActionHom.id M, map_one' := ⋯, map_mul' := ⋯ }
@[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
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 ψ χ]
:
Composition of two equivariant additive ring homomorphisms.
Equations
- g.comp f = { toDistribMulActionHom := (↑g).comp ↑f, map_one' := ⋯, map_mul' := ⋯ }
@[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)
@[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
@[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
@[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
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)
:
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' := ⋯ }
@[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
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)
:
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' := ⋯ }