Equivariant homomorphisms #
Main definitions #
MulActionHom φ X Y
, the type of equivariant functions fromX
toY
, whereφ : M → N
is a map,M
acting on the typeX
andN
acting on the type ofY
.AddActionHom φ X Y
is its additive version.DistribMulActionHom φ A B
, the type of equivariant additive monoid homomorphisms fromA
toB
, whereφ : M → N
is a morphism of monoids,M
acting on the additive monoidA
andN
acting on the additive monoid ofB
SMulSemiringHom φ R S
, the type of equivariant ring homomorphisms fromR
toS
, whereφ : M → N
is a morphism of monoids,M
acting on the ringR
andN
acting on the ringS
.
The above types have corresponding classes:
MulActionHomClass F φ X Y
states thatF
is a type of bundledX → Y
homs which areφ
-equivariant;AddActionHomClass F φ X Y
is its additive version.DistribMulActionHomClass F φ A B
states thatF
is a type of bundledA → B
homs preserving the additive monoid structure andφ
-equivariantSMulSemiringHomClass F φ R S
states thatF
is a type of bundledR → 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
isMulActionHom φ X Y
andAddActionHom φ X Y
A →ₑ+[φ] B
isDistribMulActionHom φ A B
.R →ₑ+*[φ] S
isMulSemiringActionHom φ R S
.
When M = N
and φ = MonoidHom.id M
, we provide the backward compatible notation :
X →[M] Y
isMulActionHom (@id M) X Y
andAddActionHom (@id M) X Y
A →+[M] B
isDistribMulActionHom (MonoidHom.id M) A B
R →+*[M] S
isMulSemiringActionHom (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
…
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.
The proposition that the function commutes with the additive actions.
Instances For
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.
Instances For
φ
-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.
Instances For
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.
Instances For
φ
-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.
Instances For
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.
Instances For
AddActionSemiHomClass F φ X Y
states that
F
is a type of morphisms which are φ
-equivariant.
You should extend this class when you extend AddActionHom
.
The proposition that the function preserves the action.
Instances
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
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
Instances For
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
Instances For
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
Any type satisfying MulActionSemiHomClass
can be cast into MulActionHom
via
MulActionHomSemiClass.toMulActionHom
.
Equations
- MulActionHom.instCoeTCOfMulActionSemiHomClass = { coe := MulActionSemiHomClass.toMulActionHom }
Equations
- AddActionHom.instCoeTCOfAddActionSemiHomClass = { coe := AddActionSemiHomClass.toAddActionHom }
If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action.
Two equal maps on scalars give rise to an equivariant map for identity
Equations
- MulActionHom.ofEq h f = { toFun := f.toFun, map_smul' := ⋯ }
Instances For
Two equal maps on scalars give rise to an equivariant map for identity
Equations
- AddActionHom.ofEq h f = { toFun := f.toFun, map_vadd' := ⋯ }
Instances For
The identity map as an equivariant map.
Equations
- MulActionHom.id M = { toFun := id, map_smul' := ⋯ }
Instances For
The identity map as an equivariant map.
Equations
- AddActionHom.id M = { toFun := id, map_vadd' := ⋯ }
Instances For
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯ }
Instances For
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_vadd' := ⋯ }
Instances For
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse' g k h₁ h₂ = { toFun := g, map_smul' := ⋯ }
Instances For
The inverse of a bijective equivariant map is equivariant.
Equations
- f.inverse' g k h₁ h₂ = { toFun := g, map_vadd' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
Equivariant additive monoid homomorphisms.
- toFun : A → B
Instances For
Equivariant additive monoid homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivariant additive monoid homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
Instances For
Equations
- DistribMulActionHom.instFunLike φ A B = { coe := fun (m : A →ₑ+[φ] B) => m.toFun, coe_injective' := ⋯ }
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' := ⋯ }
Instances For
Any type satisfying MulActionHomClass
can be cast into MulActionHom
via MulActionHomClass.toMulActionHom
.
Equations
- DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom = { coe := DistribMulActionSemiHomClass.toDistribMulActionHom }
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' := ⋯ }
Instances For
The identity map as an equivariant additive monoid homomorphism.
Equations
- DistribMulActionHom.id M = { toMulActionHom := MulActionHom.id M, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- DistribMulActionHom.instZero = { zero := let __src := 0; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } }
Equations
- DistribMulActionHom.instOneId = { one := DistribMulActionHom.id M }
Equations
- DistribMulActionHom.instInhabited = { default := 0 }
Composition of two equivariant additive monoid homomorphisms.
Equations
- g.comp f = { toMulActionHom := (↑g).comp ↑f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The inverse of a bijective DistribMulActionHom
is a DistribMulActionHom
.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equivariant ring homomorphisms.
- toFun : R → S
Instances For
Equivariant ring homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivariant ring homomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
MulSemiringActionHomClass F M R S
states that F
is a type of morphisms preserving
the ring structure and equivariant with respect to a DistribMulAction
of M
on R
and S
.
Equations
- MulSemiringActionHomClass F R S = MulSemiringActionSemiHomClass F (⇑(MonoidHom.id M)) R S
Instances For
Equations
- MulSemiringActionHom.instFunLike φ R S = { coe := fun (m : R →ₑ+*[φ] S) => m.toFun, coe_injective' := ⋯ }
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' := ⋯ }
Instances For
Any type satisfying MulSemiringActionHomClass
can be cast into MulSemiringActionHom
via
MulSemiringActionHomClass.toMulSemiringActionHom
.
Equations
- MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }
The identity map as an equivariant ring homomorphism.
Equations
- MulSemiringActionHom.id M = { toDistribMulActionHom := DistribMulActionHom.id M, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Composition of two equivariant additive ring homomorphisms.
Equations
- g.comp f = { toDistribMulActionHom := (↑g).comp ↑f, map_one' := ⋯, map_mul' := ⋯ }
Instances For
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' := ⋯ }
Instances For
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' := ⋯ }