Equivariant homomorphisms

Main definitions

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

The above types have corresponding classes:

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

Notation

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

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

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

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

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

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

• toFun : X → Y

  The underlying function.

• map_smul' : ∀ (m : M) (x : X), self.toFun (m • x) = φ m • self.toFun x

  The proposition that the function commutes with the actions.

theorem MulActionHom.map_smul' {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [SMul M X] {Y : Type u_6} [SMul N Y] (self : X →ₑ[φ] Y) (m : M) (x : X) : self.toFun (m • x) = φ m • self.toFun x

The proposition that the function commutes with the actions.

def «MulActionHomLocal≺» : Lean.TrailingParserDescr

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

Equations

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

def «MulActionHomIdLocal≺» : Lean.TrailingParserDescr

M-equivariant functions X → Y with respect to the action of M

This is the same as X →ₑ[@id M] Y

Equations

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

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

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

You should extend this class when you extend MulActionHom.

• map_smulₛₗ : ∀ (f : F) (c : M) (x : X), f (c • x) = φ c • f x

  The proposition that the function preserves the action.

theorem MulActionSemiHomClass.map_smulₛₗ {F : Type u_8} {M : outParam (Type u_9)} {N : outParam (Type u_10)} {φ : outParam (M → N)} {X : outParam (Type u_11)} {Y : outParam (Type u_12)} : ∀ {inst : SMul M X} {inst_1 : SMul N Y} {inst_2 : FunLike F X Y} [self : MulActionSemiHomClass F φ X Y] (f : F) (c : M) (x : X), f (c • x) = φ c • f x

The proposition that the function preserves the action.

@[reducible, inline]

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

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

Equations

• MulActionHomClass F M X Y = MulActionSemiHomClass F id X Y

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

Equations

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

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

Equations

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

The identity map as an equivariant map.

Equations

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

@[simp]

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

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

Composition of two equivariant maps.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The inverse of a bijective equivariant map is equivariant.

Equations

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

@[simp]

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

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

The inverse of a bijective equivariant map is equivariant.

Equations

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

@[simp]

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

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

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

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

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

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

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

Equations

• SMulCommClass.toMulActionHom N α c = { toFun := fun (x : α) => c • x, map_smul' := ⋯ }

@[simp]

theorem SMulCommClass.toMulActionHom_apply {M : Type u_11} (N : Type u_9) (α : Type u_10) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) : ∀ (x : α), (SMulCommClass.toMulActionHom N α c) x = c • x

structure DistribMulActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (A : Type u_4) [AddMonoid A] [DistribMulAction M A] (B : Type u_5) [AddMonoid B] [DistribMulAction N B] extends MulActionHom , AddMonoidHom , ZeroHom , AddHom : Type (max u_4 u_5)

Equivariant additive monoid homomorphisms.

@[reducible]

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

Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.

Equations

• self.toAddMonoidHom = { toFun := self.toFun, map_zero' := ⋯, map_add' := ⋯ }

def «DistribMulActionHomLocal≺» : Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

def «DistribMulActionHomIdLocal≺» : Lean.TrailingParserDescr

Equivariant additive monoid homomorphisms.

Equations

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

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

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

@[reducible, inline]

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

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

Equations

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

def SMulCommClass.toDistribMulActionHom {M : Type u_13} (N : Type u_11) (A : Type u_12) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) : A →+[N] A

If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

The identity map as an equivariant additive monoid homomorphism.

Equations

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

@[simp]

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

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

Equations

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

instance DistribMulActionHom.instOneId {M : Type u_1} [Monoid M] {A : Type u_4} [AddMonoid A] [DistribMulAction M A] : One (A →+[M] A)

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• DistribMulActionHom.instInhabited = { default := 0 }

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

Composition of two equivariant additive monoid homomorphisms.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

Equations

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

@[simp]

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

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

structure MulSemiringActionHom {M : Type u_1} [Monoid M] {N : Type u_2} [Monoid N] (φ : M →* N) (R : Type u_10) [Semiring R] [MulSemiringAction M R] (S : Type u_12) [Semiring S] [MulSemiringAction N S] extends DistribMulActionHom , RingHom , MulActionHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom : Type (max u_10 u_12)

Equivariant ring homomorphisms.

@[reducible]

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

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

Equations

• self.toRingHom = { toFun := self.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def «MulSemiringActionHomLocal≺» : Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

def «MulSemiringActionHomIdLocal≺» : Lean.TrailingParserDescr

Equivariant ring homomorphisms.

Equations

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

class MulSemiringActionSemiHomClass (F : Type u_15) {M : outParam (Type u_16)} {N : outParam (Type u_17)} [Monoid M] [Monoid N] (φ : outParam (M → N)) (R : outParam (Type u_18)) (S : outParam (Type u_19)) [Semiring R] [Semiring S] [DistribMulAction M R] [DistribMulAction N S] [FunLike F R S] extends DistribMulActionSemiHomClass , RingHomClass , MulActionSemiHomClass , MonoidHomClass , AddMonoidHomClass , MonoidWithZeroHomClass , AddHomClass , ZeroHomClass , MulHomClass , OneHomClass : Prop

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

You should extend this class when you extend MulSemiringActionHom.

@[reducible, inline]

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Turn an element of a type F satisfying MulSemiringActionHomClass F M R S into an actual MulSemiringActionHom. This is declared as the default coercion from F to MulSemiringActionHom M X Y.

Equations

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

The identity map as an equivariant ring homomorphism.

Equations

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

@[simp]

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

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

Composition of two equivariant additive ring homomorphisms.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

Equations

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

@[simp]

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

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

The inverse of a bijective MulSemiringActionHom is a MulSemiringActionHom.

Equations

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

@[simp]

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