Mathlib.GroupTheory.GroupAction.Hom

AddActionHom structure

{M N : Type*} (φ : M → N) (X : Type*) [VAdd M X] (Y : Type*) [VAdd N Y]

Full source

/-- 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)`. -/
structure AddActionHom {M N : Type*} (φ: M → N) (X : Type*) [VAdd M X] (Y : Type*) [VAdd N Y] where
  /-- The underlying function. -/
  protected toFun : X → Y
  /-- The proposition that the function commutes with the additive actions. -/
  protected map_vadd' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = (φ m) +ᵥ toFun x

Equivariant additive action homomorphism

Informal description

The structure representing an equivariant function between two additive actions. Given a function $\varphi: M \to N$ and types $X$ and $Y$ endowed with additive actions of $M$ and $N$ respectively, a function $f: X \to Y$ is $\varphi$-equivariant if it satisfies $f(m +ᵥ x) = \varphi(m) +ᵥ f(x)$ for all $m \in M$ and $x \in X$.

MulActionHom structure

Full source

/-- 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)`. -/
@[to_additive]
structure MulActionHom where
  /-- The underlying function. -/
  protected toFun : X → Y
  /-- The proposition that the function commutes with the actions. -/
  protected map_smul' : ∀ (m : M) (x : X), toFun (m • x) = (φ m) • toFun x

$\varphi$-equivariant function between multiplicative actions

Informal description

Given a function $\varphi : M \to N$ and types $X$ and $Y$ equipped with multiplicative actions of $M$ and $N$ respectively, a $\varphi$-equivariant function $f : X \to Y$ is a function that satisfies the condition $f(m \cdot x) = \varphi(m) \cdot f(x)$ for all $m \in M$ and $x \in X$. This structure bundles such equivariant functions.

MulActionHomLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

/-- `φ`-equivariant functions `X → Y`,
where `φ : M → N`, where `M` and `N` act on `X` and `Y` respectively. -/
notation:25 (name := «MulActionHomLocal≺») X " →ₑ[" φ:25 "] " Y:0 => MulActionHom φ X Y

Notation for equivariant functions

Informal description

The notation `X →ₑ[φ] Y` represents the type of `φ`-equivariant functions from `X$ to $Y$, where $\varphi : M \to N$ is a map between monoids (or additive monoids), with $M$ acting on $X$ and $N$ acting on $Y$. These functions satisfy the equivariance condition $f(m \cdot x) = \varphi(m) \cdot f(x)$ for all $m \in M$ and $x \in X$.

MulActionHomIdLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M`-equivariant functions `X → Y` with respect to the action of `M`.
This is the same as `X →ₑ[@id M] Y`. -/
notation:25 (name := «MulActionHomIdLocal≺») X " →[" M:25 "] " Y:0 => MulActionHom (@id M) X Y

Notation for M-equivariant functions

Informal description

The notation `X →[M] Y` represents the type of $M$-equivariant functions from $X$ to $Y$ with respect to the action of $M$, where $M$ acts on both $X$ and $Y$. This is equivalent to `MulActionHom (@id M) X Y`.

AddActionHomLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

/-- `φ`-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. -/
notation:25 (name := «AddActionHomLocal≺») X " →ₑ[" φ:25 "] " Y:0 => AddActionHom φ X Y

Notation for $\varphi$-equivariant additive functions

Informal description

The notation $X \to_{\varphi} Y$ represents the type of $\varphi$-equivariant additive functions from $X$ to $Y$, where $\varphi: M \to N$ is a map between monoids $M$ and $N$ that act additively on $X$ and $Y$ respectively. This notation is shared with multiplicative actions since conflicts are unlikely.

AddActionHomIdLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

/-- `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. -/
notation:25 (name := «AddActionHomIdLocal≺») X " →[" M:25 "] " Y:0 => AddActionHom (@id M) X Y

Notation for additive equivariant functions with identity action

Informal description

The notation `X →[M] Y` represents the type of `M`-equivariant functions from `X` to `Y` with respect to the additive action of `M`, where `M` acts on both `X` and `Y` via the identity map `id M`. This is equivalent to `X →ₑ[@id M] Y` in the general notation for equivariant functions.

AddActionSemiHomClass structure

 (F : Type*) {M N : outParam Type*} (φ : outParam (M → N)) (X Y : outParam Type*) [VAdd M X] [VAdd N Y] [FunLike F X Y]

Full source

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

You should extend this class when you extend `AddActionHom`. -/
class AddActionSemiHomClass (F : Type*)
    {M N : outParam Type*} (φ : outParam (M → N))
    (X Y : outParam Type*) [VAdd M X] [VAdd N Y] [FunLike F X Y] : Prop where
  /-- The proposition that the function preserves the action. -/
  map_vaddₛₗ : ∀ (f : F) (c : M) (x : X), f (c +ᵥ x) = (φ c) +ᵥ (f x)

Additive Action Semi-Homomorphism Class

Informal description

The class `AddActionSemiHomClass F φ X Y` states that `F` is a type of morphisms from `X` to `Y` that are equivariant with respect to the map `φ : M → N`, where `M` acts on `X` and `N` acts on `Y` via additive actions. This means that for any `f : F` and any `m : M`, `x : X`, the relation `f (m +ᵥ x) = φ m +ᵥ f x` holds, where `+ᵥ` denotes the additive action.

MulActionSemiHomClass structure

 (F : Type*) {M N : outParam Type*} (φ : outParam (M → N)) (X Y : outParam Type*) [SMul M X] [SMul N Y] [FunLike F X Y]

Full source

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

You should extend this class when you extend `MulActionHom`. -/
@[to_additive]
class MulActionSemiHomClass (F : Type*)
    {M N : outParam Type*} (φ : outParam (M → N))
    (X Y : outParam Type*) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
  /-- The proposition that the function preserves the action. -/
  map_smulₛₗ : ∀ (f : F) (c : M) (x : X), f (c • x) = (φ c) • (f x)

Class of φ-equivariant morphisms between actions

Informal description

The class `MulActionSemiHomClass F φ X Y` asserts that `F` is a type of morphisms between `X` and `Y` that are equivariant with respect to a map `φ : M → N`, where `M` acts on `X` and `N` acts on `Y`. This means that for any `f : F`, the action of `M` on `X` and the action of `N` on `Y` are compatible via `φ`, i.e., `f (m • x) = φ m • f x` for all `m ∈ M` and `x ∈ X`.

MulActionHomClass abbrev

(F : Type*) (M : outParam Type*) (X Y : outParam Type*) [SMul M X] [SMul M Y] [FunLike F X Y]

Full source

/-- `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`. -/
@[to_additive "`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`."]
abbrev MulActionHomClass (F : Type*) (M : outParam Type*)
    (X Y : outParam Type*) [SMul M X] [SMul M Y] [FunLike F X Y] :=
  MulActionSemiHomClass F (@id M) X Y

Class of $M$-equivariant multiplicative action homomorphisms from $X$ to $Y$

Informal description

The class `MulActionHomClass F M X Y` asserts that `F` is a type of morphisms between `X` and `Y` that are equivariant with respect to the multiplicative action of `M`, where `M` acts on both `X` and `Y`. This means that for any `f : F`, the action of `M` on `X` and `Y` is preserved, i.e., \[ f(m \cdot x) = m \cdot f(x) \] for all `m ∈ M` and `x ∈ X`.

instFunLikeMulActionHom instance

: FunLike (MulActionHom φ X Y) X Y

Full source

@[to_additive] instance : FunLike (MulActionHom φ X Y) X Y where
  coe := MulActionHom.toFun
  coe_injective' f g h := by cases f; cases g; congr

Function-Like Structure for Equivariant Homomorphisms

Informal description

The type of $\varphi$-equivariant functions between multiplicative actions $X$ and $Y$ forms a function-like structure, where each element can be viewed as a function from $X$ to $Y$.

map_smul theorem

 {F M X Y : Type*} [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

Full source

@[to_additive (attr := simp)]
theorem map_smul {F M X Y : Type*} [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 :=
  map_smulₛₗ f c x

Equivariance Property of Multiplicative Action Homomorphisms

Informal description

For any type $F$ equipped with a `MulActionHomClass` structure, and for any scalar multiplication actions of $M$ on $X$ and $Y$, if $f \in F$ is a $\varphi$-equivariant function, then $f$ satisfies the equivariance property: \[ f(c \cdot x) = c \cdot f(x) \] for all $c \in M$ and $x \in X$.

instMulActionSemiHomClassMulActionHom instance

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

Full source

@[to_additive]
instance : MulActionSemiHomClass (X →ₑ[φ] Y) φ X Y where
  map_smulₛₗ := MulActionHom.map_smul'

$\varphi$-Equivariant Function Class for Multiplicative Actions

Informal description

The type of $\varphi$-equivariant functions $X \to_{\varphi} Y$ between multiplicative actions $X$ and $Y$ forms a class of $\varphi$-equivariant morphisms, where each function $f$ satisfies $f(m \cdot x) = \varphi(m) \cdot f(x)$ for all $m \in M$ and $x \in X$.

MulActionSemiHomClass.toMulActionHom definition

[MulActionSemiHomClass F φ X Y] (f : F) : X →ₑ[φ] Y

Full source

/-- 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`. -/
@[to_additive (attr := coe)
  "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`."]
def _root_.MulActionSemiHomClass.toMulActionHom [MulActionSemiHomClass F φ X Y] (f : F) :
    X →ₑ[φ] Y where
  toFun := DFunLike.coe f
  map_smul' := map_smulₛₗ f

Conversion to $\varphi$-equivariant function between multiplicative actions

Informal description

Given a type `F` that satisfies `MulActionSemiHomClass F φ X Y`, the function converts an element of `F` into a $\varphi$-equivariant function between the multiplicative actions on $X$ and $Y$. Specifically, for any $f \in F$, the resulting function $f : X \to Y$ satisfies $f(m \cdot x) = \varphi(m) \cdot f(x)$ for all $m \in M$ and $x \in X$.

MulActionHom.instCoeTCOfMulActionSemiHomClass instance

[MulActionSemiHomClass F φ X Y] : CoeTC F (X →ₑ[φ] Y)

Full source

/-- Any type satisfying `MulActionSemiHomClass` can be cast into `MulActionHom` via
  `MulActionHomSemiClass.toMulActionHom`. -/
@[to_additive]
instance [MulActionSemiHomClass F φ X Y] : CoeTC F (X →ₑ[φ] Y) :=
  ⟨MulActionSemiHomClass.toMulActionHom⟩

Canonical Coercion from Equivariant Homomorphism Class to Equivariant Functions

Informal description

For any type `F` that satisfies `MulActionSemiHomClass F φ X Y`, there is a canonical coercion from `F` to the type of $\varphi$-equivariant functions $X \to_{\varphi} Y$.

IsScalarTower.smulHomClass theorem

[MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [MulActionHomClass F X X Y] : MulActionHomClass F M' X Y

Full source

/-- If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action. -/
@[to_additive]
theorem _root_.IsScalarTower.smulHomClass [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y]
    [MulActionHomClass F X X Y] : MulActionHomClass F M' X Y where
  map_smulₛₗ f m x := by
    rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul,
      smul_eq_mul, mul_one, id_eq]

Scalar Tower Implies Equivariance for Multiplicative Action Homomorphisms

Informal description

Let $M'$, $X$, and $Y$ be types with the following structures: - $X$ is a multiplicative monoid (i.e., has a `MulOneClass` instance), - There is a scalar multiplication action of $X$ on $Y$ (`SMul X Y`), - The actions form a scalar tower (`IsScalarTower M' X Y`), meaning that for all $m \in M'$, $x \in X$, and $y \in Y$, we have $m \cdot (x \cdot y) = (m \cdot x) \cdot y$, - $F$ is a type of functions from $X$ to $Y$ that are $X$-equivariant (`MulActionHomClass F X X Y`). Then $F$ is also a type of $M'$-equivariant functions from $X$ to $Y$ (`MulActionHomClass F M' X Y`). In other words, any $X$-equivariant function in this context automatically preserves the $M'$-action.

MulActionHom.map_smul theorem

(f : X →[M'] Y) (m : M') (x : X) : f (m • x) = m • f x

Full source

@[to_additive]
protected theorem map_smul (f : X →[M'] Y) (m : M') (x : X) : f (m • x) = m • f x :=
  map_smul f m x

Equivariance Property of $M'$-Action Homomorphisms

Informal description

For any $M'$-equivariant function $f \colon X \to Y$ between multiplicative actions and for any $m \in M'$ and $x \in X$, the function $f$ satisfies the equivariance property: \[ f(m \cdot x) = m \cdot f(x). \]

MulActionHom.ext theorem

{f g : X →ₑ[φ] Y} :
    (∀ x, f x = g x) → f = g

Full source

@[to_additive (attr := ext)]
theorem ext {f g : X →ₑ[φ] Y} :
    (∀ x, f x = g x) → f = g :=
  DFunLike.ext f g

Extensionality of Equivariant Homomorphisms

Informal description

For any two $\varphi$-equivariant functions $f, g : X \to Y$ between multiplicative actions, if $f(x) = g(x)$ for all $x \in X$, then $f = g$.

MulActionHom.congr_fun theorem

{f g : X →ₑ[φ] Y} (h : f = g) (x : X) :
    f x = g x

Full source

@[to_additive]
protected theorem congr_fun {f g : X →ₑ[φ] Y} (h : f = g) (x : X) :
    f x = g x :=
  DFunLike.congr_fun h _

Function Equality Implies Pointwise Equality for Equivariant Homomorphisms

Informal description

For any two $\varphi$-equivariant functions $f, g : X \to Y$ between multiplicative actions, if $f = g$, then $f(x) = g(x)$ for all $x \in X$.

MulActionHom.ofEq definition

{φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) : X →ₑ[φ'] Y

Full source

/-- Two equal maps on scalars give rise to an equivariant map for identity -/
@[to_additive "Two equal maps on scalars give rise to an equivariant map for identity"]
def ofEq {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) : X →ₑ[φ'] Y where
  toFun := f.toFun
  map_smul' m a := h ▸ f.map_smul' m a

Equivariant function under equal scalar maps

Informal description

Given two functions $\varphi, \varphi' : M \to N$ that are equal (i.e., $\varphi = \varphi'$), and a $\varphi$-equivariant function $f : X \to Y$ between multiplicative actions, the function $f$ can also be viewed as a $\varphi'$-equivariant function. This construction preserves the underlying function $f$ and adjusts the equivariance condition accordingly.

MulActionHom.ofEq_coe theorem

{φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :
    (f.ofEq h).toFun = f.toFun

Full source

@[to_additive (attr := simp)]
theorem ofEq_coe {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) :
    (f.ofEq h).toFun = f.toFun := rfl

Underlying Function Preservation in Equivariant Function Adjustment

Informal description

Given functions $\varphi, \varphi' : M \to N$ such that $\varphi = \varphi'$, and a $\varphi$-equivariant function $f : X \to Y$ between multiplicative actions, the underlying function of the adjusted equivariant function $f.\text{ofEq}\,h$ is equal to the underlying function of $f$.

MulActionHom.ofEq_apply theorem

{φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :
    (f.ofEq h) a = f a

Full source

@[to_additive (attr := simp)]
theorem ofEq_apply {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X) :
    (f.ofEq h) a = f a :=
  rfl

Application of Equivariant Function Under Equal Scalar Maps: $(f.\text{ofEq}\,h)(a) = f(a)$

Informal description

Given functions $\varphi, \varphi' : M \to N$ such that $\varphi = \varphi'$, and a $\varphi$-equivariant function $f : X \to Y$ between multiplicative actions, the application of the adjusted function $f.\text{ofEq}\,h$ at any point $a \in X$ equals the application of $f$ at $a$, i.e., $(f.\text{ofEq}\,h)(a) = f(a)$.

MulActionHom.id definition

: X →[M] X

Full source

/-- The identity map as an equivariant map. -/
@[to_additive "The identity map as an equivariant map."]
protected def id : X →[M] X :=
  ⟨id, fun _ _ => rfl⟩

Identity equivariant map

Informal description

The identity map on a type $X$ equipped with a multiplicative action of $M$, viewed as an $M$-equivariant map from $X$ to itself. It satisfies $\text{id}(m \cdot x) = m \cdot \text{id}(x)$ for all $m \in M$ and $x \in X$.

MulActionHom.id_apply theorem

(x : X) : MulActionHom.id M x = x

Full source

@[to_additive (attr := simp)]
theorem id_apply (x : X) :
    MulActionHom.id M x = x :=
  rfl

Identity Equivariant Map Evaluation: $\text{id}(x) = x$

Informal description

For any element $x$ in a type $X$ equipped with a multiplicative action of $M$, the identity equivariant map evaluated at $x$ is equal to $x$ itself, i.e., $\text{id}(x) = x$.

MulActionHom.comp definition

(g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :
    X →ₑ[χ] Z

Full source

/-- Composition of two equivariant maps. -/
@[to_additive "Composition of two equivariant maps."]
def comp (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [κ : CompTriple φ ψ χ] :
    X →ₑ[χ] Z :=
  ⟨g ∘ f, fun m x =>
    calc
      g (f (m • x)) = g (φ m • f x) := by rw [map_smulₛₗ]
      _ = ψ (φ m) • g (f x) := by rw [map_smulₛₗ]
      _ = (ψ ∘ φ) m • g (f x) := rfl
      _ = χ m • g (f x) := by rw [κ.comp_eq] ⟩

Composition of equivariant functions

Informal description

Given $\varphi$-equivariant functions $f \colon X \to Y$ and $g \colon Y \to Z$ with respect to maps $\varphi \colon M \to N$ and $\psi \colon N \to P$, and given a composition triple $\kappa$ ensuring $\psi \circ \varphi = \chi$, the composition $g \circ f \colon X \to Z$ is $\chi$-equivariant. This means that for all $m \in M$ and $x \in X$, the relation $(g \circ f)(m \cdot x) = \chi(m) \cdot (g \circ f)(x)$ holds.

MulActionHom.comp_apply theorem

(g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :
    g.comp f x = g (f x)

Full source

@[to_additive (attr := simp)]
theorem comp_apply
    (g : Y →ₑ[ψ] Z) (f : X →ₑ[φ] Y) [CompTriple φ ψ χ] (x : X) :
    g.comp f x = g (f x) := rfl

Evaluation of Composition of Equivariant Functions: $(g \circ f)(x) = g(f(x))$

Informal description

For any $\varphi$-equivariant function $f \colon X \to Y$ and $\psi$-equivariant function $g \colon Y \to Z$, where $\varphi \colon M \to N$ and $\psi \colon N \to P$ are maps between monoids acting on the respective types, and given a composition triple ensuring $\psi \circ \varphi = \chi$, the composition $g \circ f$ evaluated at any $x \in X$ satisfies $(g \circ f)(x) = g(f(x))$.

MulActionHom.id_comp theorem

(f : X →ₑ[φ] Y) :
    (MulActionHom.id N).comp f = f

Full source

@[to_additive (attr := simp)]
theorem id_comp (f : X →ₑ[φ] Y) :
    (MulActionHom.id N).comp f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Identity Equivariant Map is Left Identity for Composition: $\text{id}_Y \circ f = f$

Informal description

For any $\varphi$-equivariant function $f \colon X \to Y$ between multiplicative actions, the composition of $f$ with the identity equivariant map on $Y$ equals $f$ itself, i.e., $\text{id}_Y \circ f = f$.

MulActionHom.comp_id theorem

(f : X →ₑ[φ] Y) :
    f.comp (MulActionHom.id M) = f

Full source

@[to_additive (attr := simp)]
theorem comp_id (f : X →ₑ[φ] Y) :
    f.comp (MulActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Right Identity Law for Composition of Equivariant Functions: $f \circ \text{id} = f$

Informal description

For any $\varphi$-equivariant function $f \colon X \to Y$ between multiplicative actions of $M$ and $N$ (where $\varphi \colon M \to N$), the composition of $f$ with the identity equivariant map on $X$ is equal to $f$ itself, i.e., $f \circ \text{id} = f$.

MulActionHom.comp_assoc theorem

{Q T : Type*} [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

Full source

@[to_additive (attr := simp)]
theorem comp_assoc {Q T : Type*} [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 :=
  ext fun _ => rfl

Associativity of Composition for Equivariant Functions

Informal description

Let $M$, $N$, $P$, $Q$ be types with scalar multiplication operations, and let $\varphi \colon M \to N$, $\psi \colon N \to P$, $\eta \colon P \to Q$, $\chi \colon M \to P$, $\theta \colon M \to Q$, and $\zeta \colon N \to Q$ be functions such that: - $\psi \circ \varphi = \chi$, - $\eta \circ \chi = \theta$, - $\eta \circ \psi = \zeta$, - $\zeta \circ \varphi = \theta$. Given $\varphi$-equivariant $f \colon X \to Y$, $\psi$-equivariant $g \colon Y \to Z$, and $\eta$-equivariant $h \colon Z \to T$, the composition of equivariant functions satisfies the associativity law: \[ h \circ (g \circ f) = (h \circ g) \circ f. \]

MulActionHom.inverse definition

(f : X →[M] Y₁) (g : Y₁ → X)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : Y₁ →[M] X

Full source

/-- The inverse of a bijective equivariant map is equivariant. -/
@[to_additive (attr := simps) "The inverse of a bijective equivariant map is equivariant."]
def inverse (f : X →[M] Y₁) (g : Y₁ → X)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : Y₁ →[M] X where
  toFun := g
  map_smul' m x :=
    calc
      g (m • x) = g (m • f (g x)) := by rw [h₂]
      _ = g (f (m • g x)) := by simp only [map_smul, id_eq]
      _ = m • g x := by rw [h₁]

Inverse of a bijective equivariant function is equivariant

Informal description

Given a bijective $M$-equivariant function $f : X \to Y$ (where $M$ acts on $X$ and $Y$) with inverse $g : Y \to X$, the inverse function $g$ is also $M$-equivariant. That is, for all $m \in M$ and $y \in Y$, we have $g(m \cdot y) = m \cdot g(y)$.

MulActionHom.inverse' definition

(f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    Y →ₑ[φ'] X

Full source

/-- The inverse of a bijective equivariant map is equivariant. -/
@[to_additive (attr := simps) "The inverse of a bijective equivariant map is equivariant."]
def inverse' (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    Y →ₑ[φ'] X where
  toFun := g
  map_smul' m x :=
    calc
      g (m • x) = g (m • f (g x)) := by rw [h₂]
      _ = g ((φ (φ' m)) • f (g x)) := by rw [k]
      _ = g (f (φ' m • g x)) := by rw [map_smulₛₗ]
      _ = φ' m • g x := by rw [h₁]

Inverse of a bijective equivariant function with right inverse condition

Informal description

Given a $\varphi$-equivariant function $f : X \to Y$ between multiplicative actions of $M$ and $N$ respectively, with inverse function $g : Y \to X$, and given a function $\varphi' : N \to M$ that is a right inverse of $\varphi$ (i.e., $\varphi \circ \varphi' = \text{id}_N$), then $g$ is $\varphi'$-equivariant. That is, for all $m \in N$ and $y \in Y$, we have $g(m \cdot y) = \varphi'(m) \cdot g(y)$.

MulActionHom.inverse_eq_inverse' theorem

(f : X →[M] Y₁) (g : Y₁ → X)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
  inverse f g h₁ h₂ = inverse' f g (congrFun rfl) h₁ h₂

Full source

@[to_additive]
lemma inverse_eq_inverse' (f : X →[M] Y₁) (g : Y₁ → X)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
  inverse f g h₁ h₂ = inverse' f g (congrFun rfl) h₁ h₂ := by
  rfl

Equivalence of Inverse Constructions for Bijective Equivariant Functions

Informal description

Let $f : X \to Y$ be a bijective $M$-equivariant function between multiplicative actions of $M$ on $X$ and $Y$, with inverse function $g : Y \to X$. Then the inverse function constructed via `inverse` is equal to the one constructed via `inverse'` when $\varphi$ is the identity map on $M$ (i.e., $\varphi = \text{id}_M$). More precisely, if $f$ is bijective with left inverse $g$ (i.e., $g \circ f = \text{id}_X$) and right inverse $g$ (i.e., $f \circ g = \text{id}_Y$), then: $$ \text{inverse}(f, g, h_1, h_2) = \text{inverse'}(f, g, \text{congrFun}(\text{rfl}), h_1, h_2), $$ where $\text{congrFun}(\text{rfl})$ ensures that $\varphi' = \text{id}_M$ is a right inverse of $\varphi = \text{id}_M$.

MulActionHom.inverse'_inverse' theorem

{f : X →ₑ[φ] Y} {g : Y → X}
    {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    inverse' (inverse' f g k₂ h₁ h₂) f k₁ h₂ h₁ = f

Full source

@[to_additive]
theorem inverse'_inverse'
    {f : X →ₑ[φ] Y} {g : Y → X}
    {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    inverse' (inverse' f g k₂ h₁ h₂) f k₁ h₂ h₁ = f :=
  ext fun _ => rfl

Double Inverse Construction Yields Original Equivariant Function

Informal description

Let $f : X \to Y$ be a $\varphi$-equivariant function between multiplicative actions of $M$ on $X$ and $N$ on $Y$, with inverse function $g : Y \to X$. Suppose $\varphi' : N \to M$ is both a left and right inverse of $\varphi$ (i.e., $\varphi' \circ \varphi = \text{id}_M$ and $\varphi \circ \varphi' = \text{id}_N$), and $g$ is both a left and right inverse of $f$ (i.e., $g \circ f = \text{id}_X$ and $f \circ g = \text{id}_Y$). Then the double application of the inverse construction yields the original function: $$ \text{inverse'}(\text{inverse'}(f, g, k_2, h_1, h_2), f, k_1, h_2, h_1) = f. $$

MulActionHom.comp_inverse' theorem

{f : X →ₑ[φ] Y} {g : Y → X}
    {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    (inverse' f g k₂ h₁ h₂).comp f (κ := CompTriple.comp_inv k₁)
      = MulActionHom.id M

Full source

@[to_additive]
theorem comp_inverse' {f : X →ₑ[φ] Y} {g : Y → X}
    {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    (inverse' f g k₂ h₁ h₂).comp f (κ := CompTriple.comp_inv k₁)
      = MulActionHom.id M := by
  rw [MulActionHom.ext_iff]
  intro x
  simp only [comp_apply, inverse_apply, id_apply]
  exact h₁ x

Composition of Equivariant Function with Its Inverse Yields Identity

Informal description

Let $f \colon X \to Y$ be a $\varphi$-equivariant function between multiplicative actions of $M$ on $X$ and $N$ on $Y$, with inverse function $g \colon Y \to X$. Suppose $\varphi' \colon N \to M$ is both a left and right inverse of $\varphi$ (i.e., $\varphi' \circ \varphi = \text{id}_M$ and $\varphi \circ \varphi' = \text{id}_N$), and $g$ is both a left and right inverse of $f$ (i.e., $g \circ f = \text{id}_X$ and $f \circ g = \text{id}_Y$). Then the composition of the inverse equivariant function $\text{inverse'}(f, g, k_2, h_1, h_2)$ with $f$ yields the identity equivariant map on $X$: $$ \text{inverse'}(f, g, k_2, h_1, h_2) \circ f = \text{id}_M. $$

MulActionHom.inverse'_comp theorem

{f : X →ₑ[φ] Y} {g : Y → X}
    {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    f.comp (inverse' f g k₂ h₁ h₂) (κ := CompTriple.comp_inv k₂) = MulActionHom.id N

Full source

@[to_additive]
theorem inverse'_comp {f : X →ₑ[φ] Y} {g : Y → X}
    {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    f.comp (inverse' f g k₂ h₁ h₂) (κ := CompTriple.comp_inv k₂) = MulActionHom.id N := by
  rw [MulActionHom.ext_iff]
  intro x
  simp only [comp_apply, inverse_apply, id_apply]
  exact h₂ x

Composition of Equivariant Function with Its Inverse Yields Identity

Informal description

Let $f \colon X \to Y$ be a $\varphi$-equivariant function between multiplicative actions of $M$ on $X$ and $N$ on $Y$, with inverse function $g \colon Y \to X$. Suppose $\varphi' \colon N \to M$ is a right inverse of $\varphi$ (i.e., $\varphi \circ \varphi' = \text{id}_N$), and $g$ is both a left and right inverse of $f$ (i.e., $g \circ f = \text{id}_X$ and $f \circ g = \text{id}_Y$). Then the composition of $f$ with its $\varphi'$-equivariant inverse $\text{inverse'}(f, g, k_2, h_1, h_2)$ yields the identity map on $Y$ as an $N$-equivariant function: $$ f \circ g = \text{id}_N. $$

SMulCommClass.toMulActionHom definition

{M} (N α : Type*) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) : α →[N] α

Full source

/-- If actions of `M` and `N` on `α` commute,
  then for `c : M`, `(c • · : α → α)` is an `N`-action homomorphism. -/
@[to_additive (attr := simps) "If additive actions of `M` and `N` on `α` commute,
  then for `c : M`, `(c • · : α → α)` is an `N`-additive action homomorphism."]
def _root_.SMulCommClass.toMulActionHom {M} (N α : Type*)
    [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
    α →[N] α where
  toFun := (c • ·)
  map_smul' := smul_comm _

Scalar multiplication as an equivariant function under commuting actions

Informal description

Given types $M$, $N$, and $\alpha$ with scalar multiplication actions of $M$ and $N$ on $\alpha$, if the actions of $M$ and $N$ on $\alpha$ commute (i.e., $m \cdot (n \cdot x) = n \cdot (m \cdot x)$ for all $m \in M$, $n \in N$, $x \in \alpha$), then for any $c \in M$, the function $x \mapsto c \cdot x$ is an $N$-equivariant function from $\alpha$ to itself (where $\varphi$ is the identity map on $N$).

Pi.evalMulActionHom definition

{ι M : Type*} {X : ι → Type*} [∀ i, SMul M (X i)] (i : ι) : (∀ i, X i) →[M] X i

Full source

/-- Evaluation at a point as a `MulActionHom`. -/
@[to_additive (attr := simps) "Evaluation at a point as an `AddActionHom`."]
def Pi.evalMulActionHom {ι M : Type*} {X : ι → Type*} [∀ i, SMul M (X i)] (i : ι) :
    (∀ i, X i) →[M] X i where
  toFun := Function.eval i
  map_smul' _ _ := rfl

Evaluation as an equivariant function

Informal description

For each index $i$ in a family of types $X_i$ equipped with a multiplicative action by $M$, the evaluation function $\mathrm{eval}_i : (\forall i, X_i) \to X_i$ is a $M$-equivariant function (where $\varphi$ is the identity map on $M$). This means that for any $m \in M$ and $f \in \forall i, X_i$, we have $\mathrm{eval}_i(m \cdot f) = m \cdot \mathrm{eval}_i(f)$.

MulActionHom.fst definition

: α × β →[M] α

Full source

/-- `Prod.fst` as a bundled `MulActionHom`. -/
@[to_additive (attr := simps -fullyApplied) "`Prod.fst` as a bundled `AddActionHom`."]
def fst : α × βα × β →[M] α where
  toFun := Prod.fst
  map_smul' _ _ := rfl

First projection as an equivariant function

Informal description

The first projection function $\mathrm{fst} : \alpha \times \beta \to \alpha$ is a $\varphi$-equivariant function between multiplicative actions, where $\varphi$ is the identity map on $M$. This means that for any $m \in M$ and $(x, y) \in \alpha \times \beta$, we have $\mathrm{fst}(m \cdot (x, y)) = m \cdot \mathrm{fst}(x, y) = m \cdot x$.

MulActionHom.snd definition

: α × β →[M] β

Full source

/-- `Prod.snd` as a bundled `MulActionHom`. -/
@[to_additive (attr := simps -fullyApplied) "`Prod.snd` as a bundled `AddActionHom`."]
def snd : α × βα × β →[M] β where
  toFun := Prod.snd
  map_smul' _ _ := rfl

Second projection as an equivariant function

Informal description

The second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$ is a $\varphi$-equivariant function between multiplicative actions, where $\varphi$ is the identity map on $M$. This means that for any $m \in M$ and $(x, y) \in \alpha \times \beta$, we have $\mathrm{snd}(m \cdot (x, y)) = m \cdot \mathrm{snd}(x, y) = m \cdot y$.

MulActionHom.prod definition

(f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : α →ₑ[σ] γ × δ

Full source

/-- If `f` and `g` are equivariant maps, then so is `x ↦ (f x, g x)`. -/
@[to_additive (attr := simps -fullyApplied) prod
  "If `f` and `g` are equivariant maps, then so is `x ↦ (f x, g x)`."]
def prod (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : α →ₑ[σ] γ × δ where
  toFun x := (f x, g x)
  map_smul' _ _ := Prod.ext (map_smulₛₗ f _ _) (map_smulₛₗ g _ _)

Product of equivariant functions

Informal description

Given two $\sigma$-equivariant functions $f \colon \alpha \to \gamma$ and $g \colon \alpha \to \delta$, the function $x \mapsto (f(x), g(x))$ is also $\sigma$-equivariant. That is, for any $m \in M$ and $x \in \alpha$, we have $(f(m \cdot x), g(m \cdot x)) = \sigma(m) \cdot (f(x), g(x))$.

MulActionHom.fst_comp_prod theorem

(f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : (fst _ _ _).comp (prod f g) = f

Full source

@[to_additive (attr := simp) fst_comp_prod]
lemma fst_comp_prod (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : (fst _ _ _).comp (prod f g) = f := rfl

First Projection of Product Map Equals First Component: $\mathrm{fst} \circ (f, g) = f$

Informal description

Given two $\sigma$-equivariant functions $f \colon \alpha \to \gamma$ and $g \colon \alpha \to \delta$, the composition of the first projection $\mathrm{fst} \colon \gamma \times \delta \to \gamma$ with the product map $(f, g) \colon \alpha \to \gamma \times \delta$ equals $f$. That is, $\mathrm{fst} \circ (f, g) = f$.

MulActionHom.snd_comp_prod theorem

(f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : (snd _ _ _).comp (prod f g) = g

Full source

@[to_additive (attr := simp) snd_comp_prod]
lemma snd_comp_prod (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ) : (snd _ _ _).comp (prod f g) = g := rfl

Second Projection of Product Map Equals Second Component

Informal description

Given two $\sigma$-equivariant functions $f \colon \alpha \to \gamma$ and $g \colon \alpha \to \delta$, the composition of the second projection $\mathrm{snd} \colon \gamma \times \delta \to \delta$ with the product map $(f, g) \colon \alpha \to \gamma \times \delta$ equals $g$. That is, $\mathrm{snd} \circ (f, g) = g$.

MulActionHom.prod_fst_snd theorem

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

Full source

@[to_additive (attr := simp) prod_fst_snd]
lemma prod_fst_snd : prod (fst M α β) (snd M α β) = .id .. := rfl

Product of Projections Equals Identity: $(\mathrm{fst}, \mathrm{snd}) = \mathrm{id}$

Informal description

For any multiplicative actions of $M$ on $\alpha$ and $\beta$, the product of the first projection $\mathrm{fst} : \alpha \times \beta \to \alpha$ and the second projection $\mathrm{snd} : \alpha \times \beta \to \beta$ (both considered as $M$-equivariant maps) equals the identity map on $\alpha \times \beta$. In other words, the pair $(\mathrm{fst}, \mathrm{snd})$ reconstructs the original element: $(x,y) \mapsto (x,y)$.

MulActionHom.prodMap definition

(f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) : α × β →ₑ[σ] γ × δ

Full source

/-- If `f` and `g` are equivariant maps, then so is `(x, y) ↦ (f x, g y)`. -/
@[to_additive (attr := simps -fullyApplied) prodMap
  "If `f` and `g` are equivariant maps, then so is `(x, y) ↦ (f x, g y)`."]
def prodMap (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) : α × βα × β →ₑ[σ] γ × δ where
  toFun := Prod.map f g
  __ := (f.comp (fst ..)).prod (g.comp (snd ..))

Product of equivariant functions

Informal description

Given two $\sigma$-equivariant functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \delta$, the product map $(x, y) \mapsto (f(x), g(y))$ is also $\sigma$-equivariant. That is, for any $m \in M$ and $(x, y) \in \alpha \times \beta$, we have $(f(m \cdot x), g(m \cdot y)) = \sigma(m) \cdot (f(x), g(y))$.

DistribMulActionHom structure

extends A →ₑ[φ] B, A →+ B

Full source

/-- Equivariant additive monoid homomorphisms. -/
structure DistribMulActionHom extends A →ₑ[φ] B, A →+ B

Equivariant Additive Monoid Homomorphism

Informal description

The structure representing equivariant additive monoid homomorphisms, which are both additive monoid homomorphisms and equivariant maps with respect to a given monoid morphism $\varphi$. Specifically, for monoids $M$ and $N$ acting on additive monoids $A$ and $B$ respectively, and a monoid morphism $\varphi: M \to N$, a `DistribMulActionHom` is a map $f: A \to B$ that preserves the additive structure (i.e., $f$ is an additive monoid homomorphism) and is $\varphi$-equivariant (i.e., $f(m \cdot a) = \varphi(m) \cdot f(a)$ for all $m \in M$ and $a \in A$).

DistribMulActionHomLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 (name := «DistribMulActionHomLocal≺»)
  A " →ₑ+[" φ:25 "] " B:0 => DistribMulActionHom φ A B

Notation for Equivariant Additive Monoid Homomorphisms

Informal description

The notation `A →ₑ+[φ] B` represents the type of equivariant additive monoid homomorphisms from `A` to `B`, where `φ` is a monoid morphism, `A` is an additive monoid with an action of the domain monoid of `φ`, and `B` is an additive monoid with an action of the codomain monoid of `φ`. These homomorphisms preserve both the additive structure and are equivariant with respect to the monoid actions.

DistribMulActionHomIdLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 (name := «DistribMulActionHomIdLocal≺»)
  A " →+[" M:25 "] " B:0 => DistribMulActionHom (MonoidHom.id M) A B

Notation for identity-equivariant additive monoid homomorphisms

Informal description

The notation `A →+[M] B` represents the type of equivariant additive monoid homomorphisms from `A` to `B` that are equivariant with respect to the identity monoid homomorphism on `M`, where `M` acts on both the additive monoid `A` and `B`.

DistribMulActionSemiHomClass structure

(F : Type*)
    {M N : outParam Type*} (φ : outParam (M → N))
    (A B : outParam Type*)
    [Monoid M] [Monoid N]
    [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction N B]
    [FunLike F A B] : Prop
    extends MulActionSemiHomClass F φ A B, AddMonoidHomClass F A B

Full source

/-- `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`. -/
class DistribMulActionSemiHomClass (F : Type*)
    {M N : outParam Type*} (φ : outParam (M → N))
    (A B : outParam Type*)
    [Monoid M] [Monoid N]
    [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction N B]
    [FunLike F A B] : Prop
    extends MulActionSemiHomClass F φ A B, AddMonoidHomClass F A B

Class of equivariant additive monoid homomorphisms with distributive actions

Informal description

The class `DistribMulActionSemiHomClass F φ A B` characterizes types `F` of morphisms between additive monoids `A` and `B` that preserve the additive structure and are equivariant with respect to a monoid homomorphism `φ : M → N`, where `M` acts distributively on `A` and `N` acts distributively on `B`. This class extends both `MulActionSemiHomClass` (for equivariance) and `AddMonoidHomClass` (for additive structure preservation).

DistribMulActionHomClass abbrev

 (F : Type*) (M : outParam Type*) (A B : outParam Type*) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A]
  [DistribMulAction M B] [FunLike F A B]

Full source

/-- `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`. -/
abbrev DistribMulActionHomClass (F : Type*) (M : outParam Type*)
    (A B : outParam Type*) [Monoid M] [AddMonoid A] [AddMonoid B]
    [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] :=
    DistribMulActionSemiHomClass F (MonoidHom.id M) A B

Class of $M$-equivariant additive monoid homomorphisms with distributive actions

Informal description

The class `DistribMulActionHomClass F M A B` characterizes types `F` of morphisms between additive monoids `A$ and $B$ that preserve the additive structure and are equivariant with respect to the action of a monoid $M$, where $M$ acts distributively on $A$ and $B$.

DistribMulActionHom.instFunLike instance

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

Full source

instance : FunLike (A →ₑ+[φ] B) A B where
  coe m := m.toFun
  coe_injective' f g h := by
    rcases f with ⟨tF, _, _⟩; rcases g with ⟨tG, _, _⟩
    cases tF; cases tG; congr

Function-like Structure of Equivariant Additive Monoid Homomorphisms

Informal description

For any monoids $M$ and $N$ acting on additive monoids $A$ and $B$ respectively, and a monoid morphism $\varphi: M \to N$, the type of equivariant additive monoid homomorphisms $A \to B$ (denoted $A \to_{e+}[\varphi] B$) forms a function-like structure, meaning it can be treated as a function type from $A$ to $B$.

DistribMulActionHom.instDistribMulActionSemiHomClassCoeMonoidHom instance

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

Full source

instance : DistribMulActionSemiHomClass (A →ₑ+[φ] B) φ A B where
  map_smulₛₗ m := m.map_smul'
  map_zero := DistribMulActionHom.map_zero'
  map_add := DistribMulActionHom.map_add'

Equivariant Additive Monoid Homomorphism Class

Informal description

The type of equivariant additive monoid homomorphisms $A \to_{e+}[\varphi] B$ forms a class of morphisms that preserve the additive structure and are equivariant with respect to a monoid homomorphism $\varphi: M \to N$, where $M$ acts distributively on $A$ and $N$ acts distributively on $B$.

DistribMulActionSemiHomClass.toDistribMulActionHom definition

[DistribMulActionSemiHomClass F φ A B] (f : F) : A →ₑ+[φ] B

Full source

/-- 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`. -/
@[coe]
def _root_.DistribMulActionSemiHomClass.toDistribMulActionHom
    [DistribMulActionSemiHomClass F φ A B]
    (f : F) : A →ₑ+[φ] B :=
  { (f : A →+ B),  (f : A →ₑ[φ] B) with }

Conversion to equivariant additive monoid homomorphism

Informal description

Given a type `F` that satisfies `DistribMulActionSemiHomClass F φ A B`, the function converts an element `f` of `F` into an equivariant additive monoid homomorphism from `A` to `B` with respect to the monoid homomorphism `φ`. Specifically, for any `f ∈ F`, the resulting function `f : A → B` preserves the additive structure (i.e., `f` is an additive monoid homomorphism) and is `φ`-equivariant (i.e., `f(m • a) = φ(m) • f(a)` for all `m ∈ M` and `a ∈ A`).

DistribMulActionHom.instCoeTCOfDistribMulActionSemiHomClassCoeMonoidHom instance

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

Full source

/-- Any type satisfying `MulActionHomClass` can be cast into `MulActionHom`
via `MulActionHomClass.toMulActionHom`. -/
instance [DistribMulActionSemiHomClass F φ A B] :
  CoeTC F (A →ₑ+[φ] B) :=
  ⟨DistribMulActionSemiHomClass.toDistribMulActionHom⟩

Coercion from Distributive Action Homomorphism Class to Equivariant Additive Monoid Homomorphisms

Informal description

For any type `F` that satisfies `DistribMulActionSemiHomClass F φ A B`, there is a canonical way to view elements of `F` as equivariant additive monoid homomorphisms from `A` to `B` with respect to the monoid homomorphism `φ`. Specifically, any `f : F` can be coerced to a function `A →ₑ+[φ] B` that preserves the additive structure and is `φ`-equivariant (i.e., `f(m • a) = φ(m) • f(a)` for all `m ∈ M` and `a ∈ A`).

SMulCommClass.toDistribMulActionHom definition

 {M} (N A : Type*) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) :
  A →+[N] A

Full source

/-- If `DistribMulAction` of `M` and `N` on `A` commute,
  then for each `c : M`, `(c • ·)` is an `N`-action additive homomorphism. -/
@[simps]
def _root_.SMulCommClass.toDistribMulActionHom {M} (N A : Type*) [Monoid N] [AddMonoid A]
    [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) : A →+[N] A :=
  { SMulCommClass.toMulActionHom N A c,
    DistribSMul.toAddMonoidHom _ c with
    toFun := (c • ·) }

Scalar multiplication as an equivariant additive monoid homomorphism under commuting actions

Informal description

Given a monoid $N$, an additive monoid $A$, and a scalar multiplication action of $M$ on $A$ that distributes over addition, if the actions of $M$ and $N$ on $A$ commute (i.e., $m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $m \in M$, $n \in N$, $a \in A$), then for any $c \in M$, the scalar multiplication function $a \mapsto c \cdot a$ is an $N$-equivariant additive monoid homomorphism from $A$ to itself (where $\varphi$ is the identity map on $N$).

DistribMulActionHom.toFun_eq_coe theorem

(f : A →ₑ+[φ] B) : f.toFun = f

Full source

@[simp]
theorem toFun_eq_coe (f : A →ₑ+[φ] B) : f.toFun = f := rfl

Underlying Function of Equivariant Additive Monoid Homomorphism Equals Itself

Informal description

For any equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$, the underlying function $f.\text{toFun}$ is equal to $f$ itself.

DistribMulActionHom.coe_fn_coe theorem

(f : A →ₑ+[φ] B) : ⇑(f : A →+ B) = f

Full source

@[norm_cast]
theorem coe_fn_coe (f : A →ₑ+[φ] B) : ⇑(f : A →+ B) = f :=
  rfl

Coercion of Equivariant Additive Monoid Homomorphism to Additive Monoid Homomorphism Preserves Underlying Function

Informal description

For any equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$, the underlying function of $f$ when viewed as an additive monoid homomorphism (via the coercion `(f : A →+ B)`) is equal to $f$ itself.

DistribMulActionHom.coe_fn_coe' theorem

(f : A →ₑ+[φ] B) : ⇑(f : A →ₑ[φ] B) = f

Full source

@[norm_cast]
theorem coe_fn_coe' (f : A →ₑ+[φ] B) : ⇑(f : A →ₑ[φ] B) = f :=
  rfl

Equality of Underlying Functions in Coercion of Equivariant Additive Monoid Homomorphism to Equivariant Map

Informal description

For any $\varphi$-equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$, the underlying function of $f$ when viewed as a $\varphi$-equivariant map (via the coercion $(f : A \to_e[\varphi] B)$) is equal to $f$ itself.

DistribMulActionHom.ext theorem

{f g : A →ₑ+[φ] B} : (∀ x, f x = g x) → f = g

Full source

@[ext]
theorem ext {f g : A →ₑ+[φ] B} : (∀ x, f x = g x) → f = g :=
  DFunLike.ext f g

Extensionality of Equivariant Additive Monoid Homomorphisms

Informal description

For any two equivariant additive monoid homomorphisms $f, g: A \to_{e+}[\varphi] B$, if $f(x) = g(x)$ for all $x \in A$, then $f = g$.

DistribMulActionHom.congr_fun theorem

{f g : A →ₑ+[φ] B} (h : f = g) (x : A) : f x = g x

Full source

protected theorem congr_fun {f g : A →ₑ+[φ] B} (h : f = g) (x : A) : f x = g x :=
  DFunLike.congr_fun h _

Function Equality Implies Pointwise Equality for Equivariant Additive Monoid Homomorphisms

Informal description

For any two equivariant additive monoid homomorphisms $f, g: A \to_{e+}[\varphi] B$, if $f = g$, then $f(x) = g(x)$ for all $x \in A$.

DistribMulActionHom.toMulActionHom_injective theorem

{f g : A →ₑ+[φ] B} (h : (f : A →ₑ[φ] B) = (g : A →ₑ[φ] B)) : f = g

Full source

theorem toMulActionHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →ₑ[φ] B) = (g : A →ₑ[φ] B)) :
    f = g := by
  ext a
  exact MulActionHom.congr_fun h a

Injectivity of the Underlying Equivariant Function for Equivariant Additive Monoid Homomorphisms

Informal description

For any two equivariant additive monoid homomorphisms $f, g: A \to_{e+}[\varphi] B$, if their underlying $\varphi$-equivariant functions (as elements of $A \to_e[\varphi] B$) are equal, then $f = g$.

DistribMulActionHom.toAddMonoidHom_injective theorem

{f g : A →ₑ+[φ] B} (h : (f : A →+ B) = (g : A →+ B)) : f = g

Full source

theorem toAddMonoidHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →+ B) = (g : A →+ B)) : f = g := by
  ext a
  exact DFunLike.congr_fun h a

Injectivity of the Underlying Additive Monoid Homomorphism for Equivariant Additive Monoid Homomorphisms

Informal description

For any two equivariant additive monoid homomorphisms $f, g \colon A \to_{e+}[\varphi] B$, if their underlying additive monoid homomorphisms (as elements of $A \to^+ B$) are equal, then $f = g$.

DistribMulActionHom.map_zero theorem

(f : A →ₑ+[φ] B) : f 0 = 0

Full source

protected theorem map_zero (f : A →ₑ+[φ] B) : f 0 = 0 :=
  map_zero f

Preservation of Zero by Equivariant Additive Monoid Homomorphisms

Informal description

For any equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$, the image of the zero element under $f$ is the zero element in $B$, i.e., $f(0) = 0$.

DistribMulActionHom.map_add theorem

(f : A →ₑ+[φ] B) (x y : A) : f (x + y) = f x + f y

Full source

protected theorem map_add (f : A →ₑ+[φ] B) (x y : A) : f (x + y) = f x + f y :=
  map_add f x y

Additivity of Equivariant Additive Monoid Homomorphisms

Informal description

For any equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$ and any elements $x, y \in A$, the function $f$ preserves addition, i.e., $f(x + y) = f(x) + f(y)$.

DistribMulActionHom.map_neg theorem

(f : A' →ₑ+[φ] B') (x : A') : f (-x) = -f x

Full source

protected theorem map_neg (f : A' →ₑ+[φ] B') (x : A') : f (-x) = -f x :=
  map_neg f x

Negation Preservation in Equivariant Additive Monoid Homomorphisms

Informal description

For any equivariant additive monoid homomorphism $f \colon A' \to_{e+}[\varphi] B'$ and any element $x \in A'$, the function $f$ preserves negation, i.e., $f(-x) = -f(x)$.

DistribMulActionHom.map_sub theorem

(f : A' →ₑ+[φ] B') (x y : A') : f (x - y) = f x - f y

Full source

protected theorem map_sub (f : A' →ₑ+[φ] B') (x y : A') : f (x - y) = f x - f y :=
  map_sub f x y

Subtraction Preservation in Equivariant Additive Monoid Homomorphisms

Informal description

For any $\varphi$-equivariant additive monoid homomorphism $f \colon A' \to_{e+}[\varphi] B'$ and any elements $x, y \in A'$, the function $f$ preserves subtraction, i.e., $f(x - y) = f(x) - f(y)$.

DistribMulActionHom.map_smulₑ theorem

(f : A →ₑ+[φ] B) (m : M) (x : A) : f (m • x) = (φ m) • f x

Full source

protected theorem map_smulₑ (f : A →ₑ+[φ] B) (m : M) (x : A) : f (m • x) = (φ m) • f x :=
  map_smulₛₗ f m x

Equivariance property of additive monoid homomorphisms: $f(m \cdot x) = \varphi(m) \cdot f(x)$

Informal description

Let $M$ and $N$ be monoids acting on additive monoids $A$ and $B$ respectively, and let $\varphi: M \to N$ be a monoid homomorphism. For any $\varphi$-equivariant additive monoid homomorphism $f: A \to B$, element $m \in M$, and $x \in A$, we have $f(m \cdot x) = \varphi(m) \cdot f(x)$.

DistribMulActionHom.id definition

: A →+[M] A

Full source

/-- The identity map as an equivariant additive monoid homomorphism. -/
protected def id : A →+[M] A :=
  ⟨MulActionHom.id _, rfl, fun _ _ => rfl⟩

Identity equivariant additive monoid homomorphism

Informal description

The identity map on an additive monoid $A$ equipped with an action of a monoid $M$, viewed as an $M$-equivariant additive monoid homomorphism from $A$ to itself. It satisfies $\text{id}(x + y) = \text{id}(x) + \text{id}(y)$ for all $x, y \in A$ and $\text{id}(m \cdot x) = m \cdot \text{id}(x)$ for all $m \in M$ and $x \in A$.

DistribMulActionHom.id_apply theorem

(x : A) : DistribMulActionHom.id M x = x

Full source

@[simp]
theorem id_apply (x : A) : DistribMulActionHom.id M x = x := by
  rfl

Identity Equivariant Homomorphism Acts as Identity on Elements

Informal description

For any element $x$ in an additive monoid $A$ equipped with an action of a monoid $M$, the identity equivariant additive monoid homomorphism $\text{id}_M$ satisfies $\text{id}_M(x) = x$.

DistribMulActionHom.instZero instance

: Zero (A →ₑ+[φ] B)

Full source

instance : Zero (A →ₑ+[φ] B) :=
  ⟨{ (0 : A →+ B) with map_smul' := fun m _ => by simp }⟩

Zero Element in Equivariant Additive Monoid Homomorphisms

Informal description

For any additive monoids $A$ and $B$ with actions by monoids $M$ and $N$ respectively, and a monoid morphism $\varphi: M \to N$, the type of $\varphi$-equivariant additive monoid homomorphisms from $A$ to $B$ has a zero element.

DistribMulActionHom.instOneId instance

: One (A →+[M] A)

Full source

instance : One (A →+[M] A) :=
  ⟨DistribMulActionHom.id M⟩

Identity as the One Element in Equivariant Additive Monoid Homomorphisms

Informal description

For any additive monoid $A$ equipped with an action of a monoid $M$, there is a canonical one element in the type of $M$-equivariant additive monoid homomorphisms from $A$ to itself. This one element is the identity map on $A$.

DistribMulActionHom.coe_zero theorem

: ⇑(0 : A →ₑ+[φ] B) = 0

Full source

@[simp]
theorem coe_zero : ⇑(0 : A →ₑ+[φ] B) = 0 :=
  rfl

Zero Equivariant Additive Monoid Homomorphism is the Zero Function

Informal description

The zero equivariant additive monoid homomorphism $0 : A \to_{e+}[\varphi] B$ is equal to the zero function, i.e., $0(a) = 0$ for all $a \in A$.

DistribMulActionHom.coe_one theorem

: ⇑(1 : A →+[M] A) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : A →+[M] A) = id :=
  rfl

Identity Equivariant Homomorphism is Identity Function

Informal description

The canonical map from the identity element of the type of $M$-equivariant additive monoid homomorphisms from $A$ to itself is equal to the identity function on $A$, i.e., $1(a) = a$ for all $a \in A$.

DistribMulActionHom.zero_apply theorem

(a : A) : (0 : A →ₑ+[φ] B) a = 0

Full source

theorem zero_apply (a : A) : (0 : A →ₑ+[φ] B) a = 0 :=
  rfl

Zero equivariant additive monoid homomorphism evaluates to zero

Informal description

For any element $a$ in an additive monoid $A$ with a monoid action, the zero equivariant additive monoid homomorphism $0 : A \to_{e+}[\varphi] B$ evaluates to zero at $a$, i.e., $0(a) = 0$.

DistribMulActionHom.one_apply theorem

(a : A) : (1 : A →+[M] A) a = a

Full source

theorem one_apply (a : A) : (1 : A →+[M] A) a = a :=
  rfl

Identity Equivariant Additive Monoid Homomorphism Acts as Identity Function

Informal description

For any element $a$ in an additive monoid $A$ equipped with an action of a monoid $M$, the identity equivariant additive monoid homomorphism $1 \colon A \to_{[M]} A$ evaluates to $a$ at $a$, i.e., $1(a) = a$.

DistribMulActionHom.instInhabited instance

: Inhabited (A →ₑ+[φ] B)

Full source

instance : Inhabited (A →ₑ+[φ] B) :=
  ⟨0⟩

Inhabited Type of Equivariant Additive Monoid Homomorphisms

Informal description

For any additive monoids $A$ and $B$ with actions by monoids $M$ and $N$ respectively, and a monoid morphism $\varphi: M \to N$, the type of $\varphi$-equivariant additive monoid homomorphisms from $A$ to $B$ is inhabited.

DistribMulActionHom.comp definition

(g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [κ : MonoidHom.CompTriple φ ψ χ] : A →ₑ+[χ] C

Full source

/-- Composition of two equivariant additive monoid homomorphisms. -/
def comp (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [κ : MonoidHom.CompTriple φ ψ χ] :
    A →ₑ+[χ] C :=
  { MulActionHom.comp (g : B →ₑ[ψ] C) (f : A →ₑ[φ] B),
    AddMonoidHom.comp (g : B →+ C) (f : A →+ B) with }

Composition of equivariant additive monoid homomorphisms

Informal description

Given monoids $ M $, $ N $, and $ P $ acting on additive monoids $ A $, $ B $, and $ C $ respectively, and monoid morphisms $ \varphi \colon M \to N $ and $ \psi \colon N \to P $, the composition $ g \circ f \colon A \to C $ of two equivariant additive monoid homomorphisms $ f \colon A \to B $ and $ g \colon B \to C $ is an equivariant additive monoid homomorphism with respect to the composition $ \chi = \psi \circ \varphi $. This means that $ g \circ f $ preserves the additive structure (i.e., it is an additive monoid homomorphism) and satisfies the equivariance condition $ (g \circ f)(m \cdot a) = \chi(m) \cdot (g \circ f)(a) $ for all $ m \in M $ and $ a \in A $.

DistribMulActionHom.comp_apply theorem

(g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [MonoidHom.CompTriple φ ψ χ] (x : A) : g.comp f x = g (f x)

Full source

@[simp]
theorem comp_apply
    (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [MonoidHom.CompTriple φ ψ χ] (x : A) : g.comp f x = g (f x) :=
  rfl

Composition of Equivariant Additive Monoid Homomorphisms Evaluates Pointwise

Informal description

For monoids $M$, $N$, and $P$ acting on additive monoids $A$, $B$, and $C$ respectively, and monoid morphisms $\varphi \colon M \to N$ and $\psi \colon N \to P$, let $f \colon A \to B$ and $g \colon B \to C$ be $\varphi$- and $\psi$-equivariant additive monoid homomorphisms respectively. Then for any $x \in A$, the composition $(g \circ f)(x)$ equals $g(f(x))$.

DistribMulActionHom.id_comp theorem

(f : A →ₑ+[φ] B) : comp (DistribMulActionHom.id N) f = f

Full source

@[simp]
theorem id_comp (f : A →ₑ+[φ] B) : comp (DistribMulActionHom.id N) f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Identity Equivariant Homomorphism Acts as Left Identity under Composition

Informal description

For any $\varphi$-equivariant additive monoid homomorphism $f \colon A \to B$ between additive monoids $A$ and $B$ acted upon by monoids $M$ and $N$ respectively, the composition of $f$ with the identity equivariant homomorphism $\text{id}_N \colon B \to B$ equals $f$, i.e., $\text{id}_N \circ f = f$.

DistribMulActionHom.comp_id theorem

(f : A →ₑ+[φ] B) : f.comp (DistribMulActionHom.id M) = f

Full source

@[simp]
theorem comp_id (f : A →ₑ+[φ] B) : f.comp (DistribMulActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Right identity law for composition of equivariant additive monoid homomorphisms

Informal description

For any $\varphi$-equivariant additive monoid homomorphism $f \colon A \to B$ between additive monoids $A$ and $B$ equipped with actions of monoids $M$ and $N$ respectively (where $\varphi \colon M \to N$ is a monoid homomorphism), the composition of $f$ with the identity equivariant homomorphism on $A$ equals $f$. That is, $f \circ \text{id}_M = f$.

DistribMulActionHom.comp_assoc theorem

 {Q D : Type*} [Monoid Q] [AddMonoid D] [DistribMulAction Q D] {η : P →* Q} {θ : M →* Q} {ζ : N →* Q} (h : C →ₑ+[η] D)
  (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B) [MonoidHom.CompTriple φ ψ χ] [MonoidHom.CompTriple χ η θ]
  [MonoidHom.CompTriple ψ η ζ] [MonoidHom.CompTriple φ ζ θ] : h.comp (g.comp f) = (h.comp g).comp f

Full source

@[simp]
theorem comp_assoc {Q D : Type*} [Monoid Q] [AddMonoid D] [DistribMulAction Q D]
    {η : P →* Q} {θ : M →* Q} {ζ : N →* Q}
    (h : C →ₑ+[η] D) (g : B →ₑ+[ψ] C) (f : A →ₑ+[φ] B)
    [MonoidHom.CompTriple φ ψ χ] [MonoidHom.CompTriple χ η θ]
    [MonoidHom.CompTriple ψ η ζ] [MonoidHom.CompTriple φ ζ θ] :
    h.comp (g.comp f) = (h.comp g).comp f :=
  ext fun _ => rfl

Associativity of Composition of Equivariant Additive Monoid Homomorphisms

Informal description

Let $M$, $N$, $P$, and $Q$ be monoids acting on additive monoids $A$, $B$, $C$, and $D$ respectively. Given monoid homomorphisms $\varphi \colon M \to N$, $\psi \colon N \to P$, $\eta \colon P \to Q$, $\chi = \psi \circ \varphi$, $\theta = \eta \circ \chi$, and $\zeta = \eta \circ \psi$, and equivariant additive monoid homomorphisms $f \colon A \to B$, $g \colon B \to C$, and $h \colon C \to D$, the composition of these homomorphisms satisfies the associativity property: \[ h \circ (g \circ f) = (h \circ g) \circ f. \]

DistribMulActionHom.inverse definition

 (f : A →+[M] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B₁ →+[M] A

Full source

/-- The inverse of a bijective `DistribMulActionHom` is a `DistribMulActionHom`. -/
@[simps]
def inverse (f : A →+[M] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : B₁ →+[M] A :=
  { (f : A →+ B₁).inverse g h₁ h₂, f.toMulActionHom.inverse g h₁ h₂ with toFun := g }

Inverse of a bijective equivariant additive monoid homomorphism is equivariant

Informal description

Given a bijective equivariant additive monoid homomorphism $ f : A \to B $ (where $ M $ acts on $ A $ and $ B $) with inverse $ g : B \to A $, the inverse function $ g $ is also an equivariant additive monoid homomorphism. That is, $ g $ preserves the additive monoid structure and satisfies $ g(m \cdot b) = m \cdot g(b) $ for all $ m \in M $ and $ b \in B $.

DistribMulActionHom.ext_ring theorem

{f g : R →ₑ+[σ] N'} (h : f 1 = g 1) : f = g

Full source

@[ext]
theorem ext_ring {f g : R →ₑ+[σ] N'} (h : f 1 = g 1) : f = g := by
  ext x
  rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]

Extensionality of Equivariant Additive Monoid Homomorphisms via Unit Condition

Informal description

Let $R$ and $N'$ be additive monoids with actions by a monoid $M$ via a monoid homomorphism $\sigma: M \to M$. For any two $\sigma$-equivariant additive monoid homomorphisms $f, g: R \to N'$, if $f(1) = g(1)$, then $f = g$.

MulSemiringActionHom structure

extends R →ₑ+[φ] S, R →+* S

Full source

/-- Equivariant ring homomorphisms. -/
structure MulSemiringActionHom extends R →ₑ+[φ] S, R →+* S

Equivariant Ring Homomorphism

Informal description

The structure representing equivariant ring homomorphisms from $R$ to $S$ with respect to a monoid homomorphism $\phi: M \to N$, where $M$ acts on $R$ and $N$ acts on $S$. These are both ring homomorphisms (preserving the ring structure) and equivariant maps (respecting the group actions).

MulSemiringActionHomLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 (name := «MulSemiringActionHomLocal≺»)
  R " →ₑ+*[" φ:25 "] " S:0 => MulSemiringActionHom φ R S

Notation for equivariant ring homomorphisms

Informal description

The notation $R \rightarrowₑ+*[\phi] S$ represents the type of equivariant ring homomorphisms from $R$ to $S$, where $\phi: M \rightarrow N$ is a morphism of monoids, $M$ acts on the ring $R$, and $N$ acts on the ring $S$. These homomorphisms preserve both the ring structure and are equivariant with respect to the actions of $M$ and $N$ via $\phi$.

MulSemiringActionHomIdLocal≺ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 (name := «MulSemiringActionHomIdLocal≺»)
  R " →+*[" M:25 "] " S:0 => MulSemiringActionHom (MonoidHom.id M) R S

Notation for identity-action equivariant ring homomorphisms

Informal description

The notation `R →+*[M] S` represents the type of equivariant ring homomorphisms from `R` to `S` where the action is given by the identity monoid homomorphism on `M`. This means the homomorphisms preserve both the ring structure and are equivariant with respect to the action of `M` on both rings.

MulSemiringActionSemiHomClass structure

(F : Type*)
    {M N : outParam Type*} [Monoid M] [Monoid N]
    (φ : outParam (M → N))
    (R S : outParam Type*) [Semiring R] [Semiring S]
    [DistribMulAction M R] [DistribMulAction N S] [FunLike F R S] : Prop
    extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S

Full source

/-- `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`. -/
class MulSemiringActionSemiHomClass (F : Type*)
    {M N : outParam Type*} [Monoid M] [Monoid N]
    (φ : outParam (M → N))
    (R S : outParam Type*) [Semiring R] [Semiring S]
    [DistribMulAction M R] [DistribMulAction N S] [FunLike F R S] : Prop
    extends DistribMulActionSemiHomClass F φ R S, RingHomClass F R S

Class of φ-equivariant semiring homomorphisms

Informal description

The class `MulSemiringActionSemiHomClass F φ R S` states that `F` is a type of morphisms from `R` to `S` that preserve the ring structure and are equivariant with respect to a monoid homomorphism `φ : M → N`, where `M` acts on `R` and `N` acts on `S`. More precisely, for any `f : F`, the following conditions hold: 1. `f` is a ring homomorphism (i.e., preserves addition, multiplication, and multiplicative identity). 2. `f` is `φ`-equivariant, meaning that for all `m ∈ M` and `r ∈ R`, we have `f (m • r) = φ m • f r`. This class extends both `DistribMulActionSemiHomClass` (which ensures `φ`-equivariance and additive structure preservation) and `RingHomClass` (which ensures ring structure preservation).

MulSemiringActionHomClass abbrev

 (F : Type*) {M : outParam Type*} [Monoid M] (R S : outParam Type*) [Semiring R] [Semiring S] [DistribMulAction M R]
  [DistribMulAction M S] [FunLike F R S]

Full source

/-- `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` .
-/
abbrev MulSemiringActionHomClass
    (F : Type*)
    {M : outParam Type*} [Monoid M]
    (R S : outParam Type*) [Semiring R] [Semiring S]
    [DistribMulAction M R] [DistribMulAction M S] [FunLike F R S] :=
  MulSemiringActionSemiHomClass F (MonoidHom.id M) R S

Class of $M$-equivariant semiring homomorphisms

Informal description

The class `MulSemiringActionHomClass F M R S` states that `F` is a type of morphisms from a semiring $R$ to a semiring $S$ that preserve the ring structure and are equivariant with respect to the action of a monoid $M$ on $R$ and $S$. More precisely, for any $f \in F$, the following conditions hold: 1. $f$ is a ring homomorphism (i.e., preserves addition, multiplication, and multiplicative identity). 2. $f$ is $M$-equivariant, meaning that for all $m \in M$ and $r \in R$, we have $f (m \cdot r) = m \cdot f(r)$. This class extends both `DistribMulActionHomClass` (which ensures $M$-equivariance and additive structure preservation) and `RingHomClass` (which ensures ring structure preservation).

MulSemiringActionHom.instFunLike instance

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

Full source

instance : FunLike (R →ₑ+*[φ] S) R S where
  coe m := m.toFun
  coe_injective' f g h := by
    rcases f with ⟨⟨tF, _, _⟩, _, _⟩; rcases g with ⟨⟨tG, _, _⟩, _, _⟩
    cases tF; cases tG; congr

Function-Like Structure on Equivariant Ring Homomorphisms

Informal description

The type of equivariant ring homomorphisms $R \to_{\phi}^* S$ (denoted as $R \to_{\phi}^* S$) is equipped with a function-like structure, meaning it can be treated as a collection of functions from $R$ to $S$.

MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom instance

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

Full source

instance : MulSemiringActionSemiHomClass (R →ₑ+*[φ] S) φ R S where
  map_zero m := m.map_zero'
  map_add m := m.map_add'
  map_one := MulSemiringActionHom.map_one'
  map_mul := MulSemiringActionHom.map_mul'
  map_smulₛₗ m := m.map_smul'

Equivariant Semiring Homomorphism Class for $R \to_{\phi}^* S$

Informal description

The type of equivariant ring homomorphisms $R \to_{\phi}^* S$ forms a class of $\phi$-equivariant semiring homomorphisms. Specifically, for a monoid homomorphism $\phi: M \to N$ where $M$ acts on the semiring $R$ and $N$ acts on the semiring $S$, every homomorphism in $R \to_{\phi}^* S$ preserves both the ring structure and the actions, satisfying $f(m \cdot r) = \phi(m) \cdot f(r)$ for all $m \in M$ and $r \in R$.

MulSemiringActionHomClass.toMulSemiringActionHom definition

[MulSemiringActionSemiHomClass F φ R S] (f : F) : R →ₑ+*[φ] S

Full source

/-- 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`. -/
@[coe]
def _root_.MulSemiringActionHomClass.toMulSemiringActionHom
    [MulSemiringActionSemiHomClass F φ R S]
    (f : F) : R →ₑ+*[φ] S :=
 { (f : R →+* S),  (f : R →ₑ+[φ] S) with }

Conversion to equivariant ring homomorphism

Informal description

Given a type `F` that satisfies `MulSemiringActionSemiHomClass F φ R S`, the function converts an element `f` of `F` into an equivariant ring homomorphism from `R` to `S` with respect to the monoid homomorphism `φ`. Specifically, for any `f ∈ F`, the resulting function `f : R → S` preserves both the ring structure (i.e., `f` is a ring homomorphism) and is `φ`-equivariant (i.e., `f(m • r) = φ(m) • f(r)` for all `m ∈ M` and `r ∈ R`).

MulSemiringActionHom.instCoeTCOfMulSemiringActionSemiHomClassCoeMonoidHom instance

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

Full source

/-- Any type satisfying `MulSemiringActionHomClass` can be cast into `MulSemiringActionHom` via
  `MulSemiringActionHomClass.toMulSemiringActionHom`. -/
instance [MulSemiringActionSemiHomClass F φ R S] :
    CoeTC F (R →ₑ+*[φ] S) :=
  ⟨MulSemiringActionHomClass.toMulSemiringActionHom⟩

Canonical Coercion to Equivariant Ring Homomorphisms

Informal description

For any type `F` that satisfies `MulSemiringActionSemiHomClass F φ R S`, there is a canonical coercion from `F` to the type of equivariant ring homomorphisms `R →ₑ+*[φ] S`. This means that any element `f` of `F` can be treated as an equivariant ring homomorphism from `R` to `S` with respect to the monoid homomorphism `φ`, preserving both the ring structure and the group actions.

MulSemiringActionHom.coe_fn_coe theorem

(f : R →ₑ+*[φ] S) : ⇑(f : R →+* S) = f

Full source

@[norm_cast]
theorem coe_fn_coe (f : R →ₑ+*[φ] S) : ⇑(f : R →+* S) = f :=
  rfl

Underlying Function of Equivariant Ring Homomorphism as Ring Homomorphism

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$, the underlying function of $f$ (when viewed as a ring homomorphism $R \to S$) is equal to $f$ itself.

MulSemiringActionHom.coe_fn_coe' theorem

(f : R →ₑ+*[φ] S) : ⇑(f : R →ₑ+[φ] S) = f

Full source

@[norm_cast]
theorem coe_fn_coe' (f : R →ₑ+*[φ] S) : ⇑(f : R →ₑ+[φ] S) = f :=
  rfl

Underlying Function of Equivariant Ring Homomorphism as Equivariant Additive Homomorphism

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$, the underlying function of $f$ (when viewed as an equivariant additive monoid homomorphism $R \to_{\phi}^+ S$) is equal to $f$ itself.

MulSemiringActionHom.ext theorem

{f g : R →ₑ+*[φ] S} : (∀ x, f x = g x) → f = g

Full source

@[ext]
theorem ext {f g : R →ₑ+*[φ] S} : (∀ x, f x = g x) → f = g :=
  DFunLike.ext f g

Extensionality of Equivariant Ring Homomorphisms

Informal description

For any two equivariant ring homomorphisms $f, g: R \to_{\phi}^* S$, if $f(x) = g(x)$ for all $x \in R$, then $f = g$.

MulSemiringActionHom.map_zero theorem

(f : R →ₑ+*[φ] S) : f 0 = 0

Full source

protected theorem map_zero (f : R →ₑ+*[φ] S) : f 0 = 0 :=
  map_zero f

Preservation of Zero by Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$, the image of the zero element of $R$ under $f$ is the zero element of $S$, i.e., $f(0) = 0$.

MulSemiringActionHom.map_add theorem

(f : R →ₑ+*[φ] S) (x y : R) : f (x + y) = f x + f y

Full source

protected theorem map_add (f : R →ₑ+*[φ] S) (x y : R) : f (x + y) = f x + f y :=
  map_add f x y

Additivity of Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$ with respect to a monoid homomorphism $\phi \colon M \to N$, and for any elements $x, y \in R$, the image of the sum $x + y$ under $f$ is equal to the sum of the images, i.e., $f(x + y) = f(x) + f(y)$.

MulSemiringActionHom.map_neg theorem

(f : R' →ₑ+*[φ] S') (x : R') : f (-x) = -f x

Full source

protected theorem map_neg (f : R' →ₑ+*[φ] S') (x : R') : f (-x) = -f x :=
  map_neg f x

Negation Preservation by Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R' \to_{\phi}^* S'$ with respect to a monoid homomorphism $\phi \colon M \to N$, and for any element $x \in R'$, the image of the negation $-x$ under $f$ is equal to the negation of the image, i.e., $f(-x) = -f(x)$.

MulSemiringActionHom.map_sub theorem

(f : R' →ₑ+*[φ] S') (x y : R') : f (x - y) = f x - f y

Full source

protected theorem map_sub (f : R' →ₑ+*[φ] S') (x y : R') : f (x - y) = f x - f y :=
  map_sub f x y

Preservation of Subtraction by Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R' \to_{\phi}^* S'$ with respect to a monoid homomorphism $\phi \colon M \to N$, and for any elements $x, y \in R'$, the image of the difference $x - y$ under $f$ is equal to the difference of the images, i.e., $f(x - y) = f(x) - f(y)$.

MulSemiringActionHom.map_one theorem

(f : R →ₑ+*[φ] S) : f 1 = 1

Full source

protected theorem map_one (f : R →ₑ+*[φ] S) : f 1 = 1 :=
  map_one f

Preservation of Multiplicative Identity by Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$ with respect to a monoid homomorphism $\phi \colon M \to N$, the image of the multiplicative identity $1 \in R$ under $f$ is the multiplicative identity $1 \in S$, i.e., $f(1) = 1$.

MulSemiringActionHom.map_mul theorem

(f : R →ₑ+*[φ] S) (x y : R) : f (x * y) = f x * f y

Full source

protected theorem map_mul (f : R →ₑ+*[φ] S) (x y : R) : f (x * y) = f x * f y :=
  map_mul f x y

Preservation of Multiplication by Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$ with respect to a monoid homomorphism $\phi \colon M \to N$, and for any elements $x, y \in R$, the image of the product $x * y$ under $f$ is equal to the product of the images, i.e., $f(x * y) = f(x) * f(y)$.

MulSemiringActionHom.map_smulₛₗ theorem

(f : R →ₑ+*[φ] S) (m : M) (x : R) : f (m • x) = φ m • f x

Full source

protected theorem map_smulₛₗ (f : R →ₑ+*[φ] S) (m : M) (x : R) : f (m • x) = φ m • f x :=
  map_smulₛₗ f m x

Equivariance Property of Ring Homomorphisms: $f(m \cdot x) = \phi(m) \cdot f(x)$

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$ with respect to a monoid homomorphism $\phi \colon M \to N$, and for any $m \in M$ and $x \in R$, we have $f(m \cdot x) = \phi(m) \cdot f(x)$, where $\cdot$ denotes the respective actions of $M$ on $R$ and $N$ on $S$.

MulSemiringActionHom.map_smul theorem

[MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) : f (m • x) = m • f x

Full source

protected theorem map_smul [MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) :
    f (m • x) = m • f x :=
  map_smulₛₗ f m x

Equivariance of Ring Homomorphisms under Monoid Actions

Informal description

Let $M$ be a monoid acting on a semiring $R$ and a semiring $S$, and let $f: R \to S$ be an $M$-equivariant ring homomorphism. Then for any $m \in M$ and $x \in R$, we have $f(m \cdot x) = m \cdot f(x)$, where $\cdot$ denotes the action of $M$ on $R$ and $S$.

MulSemiringActionHom.id definition

: R →+*[M] R

Full source

/-- The identity map as an equivariant ring homomorphism. -/
protected def id : R →+*[M] R :=
  ⟨DistribMulActionHom.id _, rfl, (fun _ _ => rfl)⟩

Identity equivariant ring homomorphism

Informal description

The identity map on a semiring $R$ equipped with an action of a monoid $M$, viewed as an $M$-equivariant ring homomorphism from $R$ to itself. It satisfies $\text{id}(x + y) = \text{id}(x) + \text{id}(y)$ and $\text{id}(x \cdot y) = \text{id}(x) \cdot \text{id}(y)$ for all $x, y \in R$, and $\text{id}(m \cdot x) = m \cdot \text{id}(x)$ for all $m \in M$ and $x \in R$.

MulSemiringActionHom.id_apply theorem

(x : R) : MulSemiringActionHom.id M x = x

Full source

@[simp]
theorem id_apply (x : R) : MulSemiringActionHom.id M x = x :=
  rfl

Identity Equivariant Ring Homomorphism Acts as Identity Function

Informal description

For any element $x$ in a semiring $R$ equipped with an action of a monoid $M$, the identity equivariant ring homomorphism $\text{id}_M$ satisfies $\text{id}_M(x) = x$.

MulSemiringActionHom.comp definition

(g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [κ : MonoidHom.CompTriple φ ψ χ] : R →ₑ+*[χ] T

Full source

/-- Composition of two equivariant additive ring homomorphisms. -/
def comp (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [κ : MonoidHom.CompTriple φ ψ χ] : R →ₑ+*[χ] T :=
  { DistribMulActionHom.comp (g : S →ₑ+[ψ] T) (f : R →ₑ+[φ] S),
    RingHom.comp (g : S →+* T) (f : R →+* S) with }

Composition of equivariant ring homomorphisms

Informal description

Given monoids $ M $, $ N $, and $ P $ acting on semirings $ R $, $ S $, and $ T $ respectively, and monoid homomorphisms $ \varphi \colon M \to N $ and $ \psi \colon N \to P $, the composition $ g \circ f \colon R \to T $ of two equivariant ring homomorphisms $ f \colon R \to S $ and $ g \colon S \to T $ is an equivariant ring homomorphism with respect to the composition $ \chi = \psi \circ \varphi $. This means that $ g \circ f $ preserves both the ring structure (addition and multiplication) and satisfies the equivariance condition $ (g \circ f)(m \cdot r) = \chi(m) \cdot (g \circ f)(r) $ for all $ m \in M $ and $ r \in R $.

MulSemiringActionHom.comp_apply theorem

(g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [MonoidHom.CompTriple φ ψ χ] (x : R) : g.comp f x = g (f x)

Full source

@[simp]
theorem comp_apply (g : S →ₑ+*[ψ] T) (f : R →ₑ+*[φ] S) [MonoidHom.CompTriple φ ψ χ] (x : R) :
    g.comp f x = g (f x) := rfl

Composition of Equivariant Ring Homomorphisms Preserves Function Application

Informal description

For equivariant ring homomorphisms $f \colon R \to_{\phi}^* S$ and $g \colon S \to_{\psi}^* T$, and for any $x \in R$, the composition $(g \circ f)(x)$ equals $g(f(x))$.

MulSemiringActionHom.id_comp theorem

(f : R →ₑ+*[φ] S) : (MulSemiringActionHom.id N).comp f = f

Full source

@[simp]
theorem id_comp (f : R →ₑ+*[φ] S) : (MulSemiringActionHom.id N).comp f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Identity Composition Law for Equivariant Ring Homomorphisms

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$, the composition of the identity equivariant ring homomorphism on $S$ with $f$ equals $f$ itself, i.e., $\text{id}_N \circ f = f$.

MulSemiringActionHom.comp_id theorem

(f : R →ₑ+*[φ] S) : f.comp (MulSemiringActionHom.id M) = f

Full source

@[simp]
theorem comp_id (f : R →ₑ+*[φ] S) : f.comp (MulSemiringActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Composition with Identity Equivariant Ring Homomorphism Preserves $f$

Informal description

For any equivariant ring homomorphism $f \colon R \to_{\phi}^* S$, the composition of $f$ with the identity equivariant ring homomorphism on $R$ equals $f$ itself, i.e., $f \circ \text{id}_M = f$.

MulSemiringActionHom.inverse' definition

 (f : R →ₑ+*[φ] S) (g : S → R) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f)
  (h₂ : Function.RightInverse g f) : S →ₑ+*[φ'] R

Full source

/-- The inverse of a bijective `MulSemiringActionHom` is a `MulSemiringActionHom`. -/
@[simps]
def inverse' (f : R →ₑ+*[φ] S) (g : S → R) (k : Function.RightInverse φ' φ)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    S →ₑ+*[φ'] R :=
  { (f : R →+ S).inverse g h₁ h₂,
    (f : R →* S).inverse g h₁ h₂,
    (f : R →ₑ[φ] S).inverse' g k h₁ h₂ with
    toFun := g }

Inverse of a bijective equivariant ring homomorphism with right inverse condition

Informal description

Given a bijective equivariant ring homomorphism $f : R \to_{\phi}^* S$ with inverse $g : S \to R$, and given a monoid homomorphism $\phi' : N \to M$ that is a right inverse of $\phi$ (i.e., $\phi \circ \phi' = \text{id}_N$), then $g$ is an equivariant ring homomorphism $S \to_{\phi'}^* R$. Specifically, $g$ preserves the ring structure (addition, multiplication, and multiplicative identity) and satisfies the equivariance condition $g(n \cdot s) = \phi'(n) \cdot g(s)$ for all $n \in N$ and $s \in S$.

MulSemiringActionHom.inverse definition

 {S₁ : Type*} [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

Full source

/-- The inverse of a bijective `MulSemiringActionHom` is a `MulSemiringActionHom`. -/
@[simps]
def inverse {S₁ : Type*} [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 :=
  { (f : R →+ S₁).inverse g h₁ h₂,
    (f : R →* S₁).inverse g h₁ h₂,
    f.toMulActionHom.inverse g h₁ h₂ with
    toFun := g }

Inverse of a bijective equivariant ring homomorphism

Informal description

Given a bijective equivariant ring homomorphism $ f : R \to_{M}^* S_1 $ (where $ M $ acts on both $ R $ and $ S_1 $) with inverse $ g : S_1 \to R $, the inverse function $ g $ is also an equivariant ring homomorphism $ S_1 \to_{M}^* R $. Specifically, $ g $ preserves the ring structure (addition, multiplication, and multiplicative identity) and satisfies the equivariance condition $ g(m \cdot s) = m \cdot g(s) $ for all $ m \in M $ and $ s \in S_1 $.

Main definitions

Notation