Operations on `Submonoid`s #

In this file we define various operations on Submonoids and MonoidHoms.

Main definitions #

Conversion between multiplicative and additive definitions #

Submonoid.toAddSubmonoid, Submonoid.toAddSubmonoid', AddSubmonoid.toSubmonoid, AddSubmonoid.toSubmonoid': convert between multiplicative and additive submonoids of M, Multiplicative M, and Additive M. These are stated as OrderIsos.

(Commutative) monoid structure on a submonoid #

Submonoid.toMonoid, Submonoid.toCommMonoid: a submonoid inherits a (commutative) monoid structure.

Group actions by submonoids #

Submonoid.MulAction, Submonoid.DistribMulAction: a submonoid inherits (distributive) multiplicative actions.

Operations on submonoids #

Submonoid.comap: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;
Submonoid.map: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
Submonoid.prod: product of two submonoids s : Submonoid M and t : Submonoid N as a submonoid of M × N;

Monoid homomorphisms between submonoid #

Submonoid.subtype: embedding of a submonoid into the ambient monoid.
Submonoid.inclusion: given two submonoids S, T such that S ≤ T, S.inclusion T is the inclusion of S into T as a monoid homomorphism;
MulEquiv.submonoidCongr: converts a proof of S = T into a monoid isomorphism between S and T.
Submonoid.prodEquiv: monoid isomorphism between s.prod t and s × t;

Operations on `MonoidHom`s #

MonoidHom.mrange: range of a monoid homomorphism as a submonoid of the codomain;
MonoidHom.mker: kernel of a monoid homomorphism as a submonoid of the domain;
MonoidHom.restrict: restrict a monoid homomorphism to a submonoid;
MonoidHom.codRestrict: restrict the codomain of a monoid homomorphism to a submonoid;
MonoidHom.mrangeRestrict: restrict a monoid homomorphism to its range;

Tags #

submonoid, range, product, map, comap

Conversion to/from `Additive`/`Multiplicative` #

source

@[simp]

theorem Submonoid.toAddSubmonoid_symm_apply_coe {M : Type u_1} [MulOneClass M] (S : AddSubmonoid (Additive M)) :

↑((RelIso.symm Submonoid.toAddSubmonoid) S) = ⇑Additive.ofMul ⁻¹' ↑S

source

@[simp]

theorem Submonoid.toAddSubmonoid_apply_coe {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

↑(Submonoid.toAddSubmonoid S) = ⇑Additive.toMul ⁻¹' ↑S

source

def Submonoid.toAddSubmonoid {M : Type u_1} [MulOneClass M] :

Submonoid M ≃o AddSubmonoid (Additive M)

Submonoids of monoid M are isomorphic to additive submonoids of Additive M.

Equations

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

Instances For

source

@[reducible, inline]

abbrev AddSubmonoid.toSubmonoid' {M : Type u_1} [MulOneClass M] :

AddSubmonoid (Additive M) ≃o Submonoid M

Additive submonoids of an additive monoid Additive M are isomorphic to submonoids of M.

Equations

AddSubmonoid.toSubmonoid' = Submonoid.toAddSubmonoid.symm

Instances For

source

theorem Submonoid.toAddSubmonoid_closure {M : Type u_1} [MulOneClass M] (S : Set M) :

Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S)

source

theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [MulOneClass M] (S : Set (Additive M)) :

AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.ofAdd ⁻¹' S)

source

@[simp]

theorem AddSubmonoid.toSubmonoid_apply_coe {A : Type u_4} [AddZeroClass A] (S : AddSubmonoid A) :

↑(AddSubmonoid.toSubmonoid S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

source

@[simp]

theorem AddSubmonoid.toSubmonoid_symm_apply_coe {A : Type u_4} [AddZeroClass A] (S : Submonoid (Multiplicative A)) :

↑((RelIso.symm AddSubmonoid.toSubmonoid) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S

source

def AddSubmonoid.toSubmonoid {A : Type u_4} [AddZeroClass A] :

AddSubmonoid A ≃o Submonoid (Multiplicative A)

Additive submonoids of an additive monoid A are isomorphic to multiplicative submonoids of Multiplicative A.

Equations

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

Instances For

source

@[reducible, inline]

abbrev Submonoid.toAddSubmonoid' {A : Type u_4} [AddZeroClass A] :

Submonoid (Multiplicative A) ≃o AddSubmonoid A

Submonoids of a monoid Multiplicative A are isomorphic to additive submonoids of A.

Equations

Submonoid.toAddSubmonoid' = AddSubmonoid.toSubmonoid.symm

Instances For

source

theorem AddSubmonoid.toSubmonoid_closure {A : Type u_4} [AddZeroClass A] (S : Set A) :

AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

source

theorem Submonoid.toAddSubmonoid'_closure {A : Type u_4} [AddZeroClass A] (S : Set (Multiplicative A)) :

Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.ofMul ⁻¹' S)

`comap` and `map` #

source

def AddSubmonoid.comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

AddSubmonoid M

The preimage of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations

AddSubmonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

def Submonoid.comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N) :

Submonoid M

The preimage of a submonoid along a monoid homomorphism is a submonoid.

Equations

Submonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

@[simp]

theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F) :

↑(AddSubmonoid.comap f S) = ⇑f ⁻¹' ↑S

source

@[simp]

theorem Submonoid.coe_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F) :

↑(Submonoid.comap f S) = ⇑f ⁻¹' ↑S

source

@[simp]

theorem AddSubmonoid.mem_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M} :

x ∈ AddSubmonoid.comap f S ↔ f x ∈ S

source

@[simp]

theorem Submonoid.mem_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M} :

x ∈ Submonoid.comap f S ↔ f x ∈ S

source

theorem AddSubmonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N) :

AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (g.comp f) S

source

theorem Submonoid.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (S : Submonoid P) (g : N →* P) (f : M →* N) :

Submonoid.comap f (Submonoid.comap g S) = Submonoid.comap (g.comp f) S

source

@[simp]

theorem AddSubmonoid.comap_id {P : Type u_3} [AddZeroClass P] (S : AddSubmonoid P) :

AddSubmonoid.comap (AddMonoidHom.id P) S = S

source

@[simp]

theorem Submonoid.comap_id {P : Type u_3} [MulOneClass P] (S : Submonoid P) :

Submonoid.comap (MonoidHom.id P) S = S

source

def AddSubmonoid.map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

AddSubmonoid N

The image of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations

AddSubmonoid.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

def Submonoid.map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

Submonoid N

The image of a submonoid along a monoid homomorphism is a submonoid.

Equations

Submonoid.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

@[simp]

theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

↑(AddSubmonoid.map f S) = ⇑f '' ↑S

source

@[simp]

theorem Submonoid.coe_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

↑(Submonoid.map f S) = ⇑f '' ↑S

source

@[simp]

theorem AddSubmonoid.mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N} :

y ∈ AddSubmonoid.map f S ↔ ∃ x ∈ S, f x = y

source

@[simp]

theorem Submonoid.mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N} :

y ∈ Submonoid.map f S ↔ ∃ x ∈ S, f x = y

source

theorem AddSubmonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M} (hx : x ∈ S) :

f x ∈ AddSubmonoid.map f S

source

theorem Submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M} (hx : x ∈ S) :

f x ∈ Submonoid.map f S

source

theorem AddSubmonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : ↥S) :

f ↑x ∈ AddSubmonoid.map f S

source

theorem Submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : ↥S) :

f ↑x ∈ Submonoid.map f S

source

theorem AddSubmonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N) :

AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (g.comp f) S

source

theorem Submonoid.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (S : Submonoid M) (g : N →* P) (f : M →* N) :

Submonoid.map g (Submonoid.map f S) = Submonoid.map (g.comp f) S

source

@[simp]

theorem AddSubmonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {S : AddSubmonoid M} {x : M} :

f x ∈ AddSubmonoid.map f S ↔ x ∈ S

source

@[simp]

theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {S : Submonoid M} {x : M} :

f x ∈ Submonoid.map f S ↔ x ∈ S

source

theorem AddSubmonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N} :

AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T

source

theorem Submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N} :

Submonoid.map f S ≤ T ↔ S ≤ Submonoid.comap f T

source

theorem AddSubmonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)

source

theorem Submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

GaloisConnection (Submonoid.map f) (Submonoid.comap f)

source

theorem AddSubmonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :

S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T

source

theorem Submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :

S ≤ Submonoid.comap f T → Submonoid.map f S ≤ T

source

theorem AddSubmonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :

AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T

source

theorem Submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :

Submonoid.map f S ≤ T → S ≤ Submonoid.comap f T

source

theorem AddSubmonoid.le_comap_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :

S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)

source

theorem Submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :

S ≤ Submonoid.comap f (Submonoid.map f S)

source

theorem AddSubmonoid.map_comap_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} :

AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S

source

theorem Submonoid.map_comap_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :

Submonoid.map f (Submonoid.comap f S) ≤ S

source

theorem AddSubmonoid.monotone_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :

Monotone (AddSubmonoid.map f)

source

theorem Submonoid.monotone_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :

Monotone (Submonoid.map f)

source

theorem AddSubmonoid.monotone_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :

Monotone (AddSubmonoid.comap f)

source

theorem Submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :

Monotone (Submonoid.comap f)

source

@[simp]

theorem AddSubmonoid.map_comap_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :

AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S

source

@[simp]

theorem Submonoid.map_comap_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :

Submonoid.map f (Submonoid.comap f (Submonoid.map f S)) = Submonoid.map f S

source

@[simp]

theorem AddSubmonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} :

AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S

source

@[simp]

theorem Submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :

Submonoid.comap f (Submonoid.map f (Submonoid.comap f S)) = Submonoid.comap f S

source

theorem AddSubmonoid.map_sup {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid M) (T : AddSubmonoid M) (f : F) :

AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T

source

theorem Submonoid.map_sup {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (S : Submonoid M) (T : Submonoid M) (f : F) :

Submonoid.map f (S ⊔ T) = Submonoid.map f S ⊔ Submonoid.map f T

source

theorem AddSubmonoid.map_iSup {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid M) :

AddSubmonoid.map f (iSup s) = ⨆ (i : ι), AddSubmonoid.map f (s i)

source

theorem Submonoid.map_iSup {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid M) :

Submonoid.map f (iSup s) = ⨆ (i : ι), Submonoid.map f (s i)

source

theorem AddSubmonoid.map_inf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid M) (T : AddSubmonoid M) (f : F) (hf : Function.Injective ⇑f) :

AddSubmonoid.map f (S ⊓ T) = AddSubmonoid.map f S ⊓ AddSubmonoid.map f T

source

theorem Submonoid.map_inf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (S : Submonoid M) (T : Submonoid M) (f : F) (hf : Function.Injective ⇑f) :

Submonoid.map f (S ⊓ T) = Submonoid.map f S ⊓ Submonoid.map f T

source

theorem AddSubmonoid.map_iInf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} [Nonempty ι] (f : F) (hf : Function.Injective ⇑f) (s : ι → AddSubmonoid M) :

AddSubmonoid.map f (iInf s) = ⨅ (i : ι), AddSubmonoid.map f (s i)

source

theorem Submonoid.map_iInf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Sort u_5} [Nonempty ι] (f : F) (hf : Function.Injective ⇑f) (s : ι → Submonoid M) :

Submonoid.map f (iInf s) = ⨅ (i : ι), Submonoid.map f (s i)

source

theorem AddSubmonoid.comap_inf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (T : AddSubmonoid N) (f : F) :

AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T

source

theorem Submonoid.comap_inf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (S : Submonoid N) (T : Submonoid N) (f : F) :

Submonoid.comap f (S ⊓ T) = Submonoid.comap f S ⊓ Submonoid.comap f T

source

theorem AddSubmonoid.comap_iInf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid N) :

AddSubmonoid.comap f (iInf s) = ⨅ (i : ι), AddSubmonoid.comap f (s i)

source

theorem Submonoid.comap_iInf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid N) :

Submonoid.comap f (iInf s) = ⨅ (i : ι), Submonoid.comap f (s i)

source

@[simp]

theorem AddSubmonoid.map_bot {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.map f ⊥ = ⊥

source

@[simp]

theorem Submonoid.map_bot {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid.map f ⊥ = ⊥

source

@[simp]

theorem AddSubmonoid.comap_top {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.comap f ⊤ = ⊤

source

@[simp]

theorem Submonoid.comap_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid.comap f ⊤ = ⊤

source

@[simp]

theorem AddSubmonoid.map_id {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

AddSubmonoid.map (AddMonoidHom.id M) S = S

source

@[simp]

theorem Submonoid.map_id {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

Submonoid.map (MonoidHom.id M) S = S

source

def AddSubmonoid.gciMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)

map f and comap f form a GaloisCoinsertion when f is injective.

Equations

AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

def Submonoid.gciMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

GaloisCoinsertion (Submonoid.map f) (Submonoid.comap f)

map f and comap f form a GaloisCoinsertion when f is injective.

Equations

Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

theorem AddSubmonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S) = S

source

theorem Submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : Submonoid M) :

Submonoid.comap f (Submonoid.map f S) = S

source

theorem AddSubmonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

Function.Surjective (AddSubmonoid.comap f)

source

theorem Submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

Function.Surjective (Submonoid.comap f)

source

theorem AddSubmonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

Function.Injective (AddSubmonoid.map f)

source

theorem Submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

Function.Injective (Submonoid.map f)

source

theorem AddSubmonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : AddSubmonoid M) (T : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S ⊓ AddSubmonoid.map f T) = S ⊓ T

source

theorem Submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : Submonoid M) (T : Submonoid M) :

Submonoid.comap f (Submonoid.map f S ⊓ Submonoid.map f T) = S ⊓ T

source

theorem AddSubmonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ⇑f) (S : ι → AddSubmonoid M) :

AddSubmonoid.comap f (⨅ (i : ι), AddSubmonoid.map f (S i)) = iInf S

source

theorem Submonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ⇑f) (S : ι → Submonoid M) :

Submonoid.comap f (⨅ (i : ι), Submonoid.map f (S i)) = iInf S

source

theorem AddSubmonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : AddSubmonoid M) (T : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S ⊔ AddSubmonoid.map f T) = S ⊔ T

source

theorem Submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : Submonoid M) (T : Submonoid M) :

Submonoid.comap f (Submonoid.map f S ⊔ Submonoid.map f T) = S ⊔ T

source

theorem AddSubmonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ⇑f) (S : ι → AddSubmonoid M) :

AddSubmonoid.comap f (⨆ (i : ι), AddSubmonoid.map f (S i)) = iSup S

source

theorem Submonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ⇑f) (S : ι → Submonoid M) :

Submonoid.comap f (⨆ (i : ι), Submonoid.map f (S i)) = iSup S

source

theorem AddSubmonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {S : AddSubmonoid M} {T : AddSubmonoid M} :

AddSubmonoid.map f S ≤ AddSubmonoid.map f T ↔ S ≤ T

source

theorem Submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {S : Submonoid M} {T : Submonoid M} :

Submonoid.map f S ≤ Submonoid.map f T ↔ S ≤ T

source

theorem AddSubmonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

StrictMono (AddSubmonoid.map f)

source

theorem Submonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) :

StrictMono (Submonoid.map f)

source

def AddSubmonoid.giMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

GaloisInsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Equations

AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

def Submonoid.giMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

GaloisInsertion (Submonoid.map f) (Submonoid.comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Equations

Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

theorem AddSubmonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S) = S

source

theorem Submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : Submonoid N) :

Submonoid.map f (Submonoid.comap f S) = S

source

theorem AddSubmonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

Function.Surjective (AddSubmonoid.map f)

source

theorem Submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

Function.Surjective (Submonoid.map f)

source

theorem AddSubmonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

Function.Injective (AddSubmonoid.comap f)

source

theorem Submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

Function.Injective (Submonoid.comap f)

source

theorem AddSubmonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : AddSubmonoid N) (T : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T) = S ⊓ T

source

theorem Submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : Submonoid N) (T : Submonoid N) :

Submonoid.map f (Submonoid.comap f S ⊓ Submonoid.comap f T) = S ⊓ T

source

theorem AddSubmonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ⇑f) (S : ι → AddSubmonoid N) :

AddSubmonoid.map f (⨅ (i : ι), AddSubmonoid.comap f (S i)) = iInf S

source

theorem Submonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ⇑f) (S : ι → Submonoid N) :

Submonoid.map f (⨅ (i : ι), Submonoid.comap f (S i)) = iInf S

source

theorem AddSubmonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : AddSubmonoid N) (T : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S ⊔ AddSubmonoid.comap f T) = S ⊔ T

source

theorem Submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : Submonoid N) (T : Submonoid N) :

Submonoid.map f (Submonoid.comap f S ⊔ Submonoid.comap f T) = S ⊔ T

source

theorem AddSubmonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ⇑f) (S : ι → AddSubmonoid N) :

AddSubmonoid.map f (⨆ (i : ι), AddSubmonoid.comap f (S i)) = iSup S

source

theorem Submonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ⇑f) (S : ι → Submonoid N) :

Submonoid.map f (⨆ (i : ι), Submonoid.comap f (S i)) = iSup S

source

theorem AddSubmonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) {S : AddSubmonoid N} {T : AddSubmonoid N} :

AddSubmonoid.comap f S ≤ AddSubmonoid.comap f T ↔ S ≤ T

source

theorem Submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) {S : Submonoid N} {T : Submonoid N} :

Submonoid.comap f S ≤ Submonoid.comap f T ↔ S ≤ T

source

theorem AddSubmonoid.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

StrictMono (AddSubmonoid.comap f)

source

theorem Submonoid.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) :

StrictMono (Submonoid.comap f)

source

def AddSubmonoid.topEquiv {M : Type u_5} [AddZeroClass M] :

↥⊤ ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

Equations

AddSubmonoid.topEquiv = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Submonoid.topEquiv_apply {M : Type u_5} [MulOneClass M] (x : ↥⊤) :

Submonoid.topEquiv x = ↑x

source

@[simp]

theorem AddSubmonoid.topEquiv_apply {M : Type u_5} [AddZeroClass M] (x : ↥⊤) :

AddSubmonoid.topEquiv x = ↑x

source

@[simp]

theorem Submonoid.topEquiv_symm_apply_coe {M : Type u_5} [MulOneClass M] (x : M) :

↑(Submonoid.topEquiv.symm x) = x

source

@[simp]

theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_5} [AddZeroClass M] (x : M) :

↑(AddSubmonoid.topEquiv.symm x) = x

source

def Submonoid.topEquiv {M : Type u_5} [MulOneClass M] :

↥⊤ ≃* M

The top submonoid is isomorphic to the monoid.

Equations

Submonoid.topEquiv = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddSubmonoid.topEquiv_toAddMonoidHom {M : Type u_5} [AddZeroClass M] :

↑AddSubmonoid.topEquiv = ⊤.subtype

source

@[simp]

theorem Submonoid.topEquiv_toMonoidHom {M : Type u_5} [MulOneClass M] :

↑Submonoid.topEquiv = ⊤.subtype

source

noncomputable def AddSubmonoid.equivMapOfInjective {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ⇑f) :

↥S ≃+ ↥(AddSubmonoid.map f S)

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubmonoidMap for better definitional equalities.

Equations

S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }

Instances For

source

noncomputable def Submonoid.equivMapOfInjective {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (S : Submonoid M) (f : M →* N) (hf : Function.Injective ⇑f) :

↥S ≃* ↥(Submonoid.map f S)

A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.submonoidMap for better definitional equalities.

Equations

S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddSubmonoid.coe_equivMapOfInjective_apply {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ⇑f) (x : ↥S) :

↑((S.equivMapOfInjective f hf) x) = f ↑x

source

@[simp]

theorem Submonoid.coe_equivMapOfInjective_apply {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (S : Submonoid M) (f : M →* N) (hf : Function.Injective ⇑f) (x : ↥S) :

↑((S.equivMapOfInjective f hf) x) = f ↑x

source

@[simp]

theorem AddSubmonoid.closure_closure_coe_preimage {M : Type u_5} [AddZeroClass M] {s : Set M} :

AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤

source

@[simp]

theorem Submonoid.closure_closure_coe_preimage {M : Type u_5} [MulOneClass M] {s : Set M} :

Submonoid.closure (Subtype.val ⁻¹' s) = ⊤

source

def AddSubmonoid.prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) (t : AddSubmonoid N) :

AddSubmonoid (M × N)

Given AddSubmonoids s, t of AddMonoids A, B respectively, s × t as an AddSubmonoid of A × B.

Equations

s.prod t = { carrier := ↑s ×ˢ ↑t, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

def Submonoid.prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) (t : Submonoid N) :

Submonoid (M × N)

Given submonoids s, t of monoids M, N respectively, s × t as a submonoid of M × N.

Equations

s.prod t = { carrier := ↑s ×ˢ ↑t, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

theorem AddSubmonoid.coe_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) (t : AddSubmonoid N) :

↑(s.prod t) = ↑s ×ˢ ↑t

source

theorem Submonoid.coe_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) (t : Submonoid N) :

↑(s.prod t) = ↑s ×ˢ ↑t

source

theorem AddSubmonoid.mem_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {s : AddSubmonoid M} {t : AddSubmonoid N} {p : M × N} :

p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

theorem Submonoid.mem_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {s : Submonoid M} {t : Submonoid N} {p : M × N} :

p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

theorem AddSubmonoid.prod_mono {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {s₁ : AddSubmonoid M} {s₂ : AddSubmonoid M} {t₁ : AddSubmonoid N} {t₂ : AddSubmonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁.prod t₁ ≤ s₂.prod t₂

source

theorem Submonoid.prod_mono {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {s₁ : Submonoid M} {s₂ : Submonoid M} {t₁ : Submonoid N} {t₂ : Submonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁.prod t₁ ≤ s₂.prod t₂

source

theorem AddSubmonoid.prod_top {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) :

s.prod ⊤ = AddSubmonoid.comap (AddMonoidHom.fst M N) s

source

theorem Submonoid.prod_top {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) :

s.prod ⊤ = Submonoid.comap (MonoidHom.fst M N) s

source

theorem AddSubmonoid.top_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid N) :

⊤.prod s = AddSubmonoid.comap (AddMonoidHom.snd M N) s

source

theorem Submonoid.top_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid N) :

⊤.prod s = Submonoid.comap (MonoidHom.snd M N) s

source

@[simp]

theorem AddSubmonoid.top_prod_top {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] :

⊤.prod ⊤ = ⊤

source

@[simp]

theorem Submonoid.top_prod_top {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] :

⊤.prod ⊤ = ⊤

source

theorem AddSubmonoid.bot_prod_bot {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] :

⊥.prod ⊥ = ⊥

source

theorem Submonoid.bot_prod_bot {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] :

⊥.prod ⊥ = ⊥

source

def AddSubmonoid.prodEquiv {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) (t : AddSubmonoid N) :

↥(s.prod t) ≃+ ↥s × ↥t

The product of additive submonoids is isomorphic to their product as additive monoids

Equations

s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }

Instances For

source

def Submonoid.prodEquiv {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) (t : Submonoid N) :

↥(s.prod t) ≃* ↥s × ↥t

The product of submonoids is isomorphic to their product as monoids.

Equations

s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }

Instances For

source

theorem AddSubmonoid.map_inl {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) :

AddSubmonoid.map (AddMonoidHom.inl M N) s = s.prod ⊥

source

theorem Submonoid.map_inl {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) :

Submonoid.map (MonoidHom.inl M N) s = s.prod ⊥

source

theorem AddSubmonoid.map_inr {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid N) :

AddSubmonoid.map (AddMonoidHom.inr M N) s = ⊥.prod s

source

theorem Submonoid.map_inr {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid N) :

Submonoid.map (MonoidHom.inr M N) s = ⊥.prod s

source

@[simp]

theorem AddSubmonoid.prod_bot_sup_bot_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) (t : AddSubmonoid N) :

s.prod ⊥ ⊔ ⊥.prod t = s.prod t

source

@[simp]

theorem Submonoid.prod_bot_sup_bot_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) (t : Submonoid N) :

s.prod ⊥ ⊔ ⊥.prod t = s.prod t

source

theorem AddSubmonoid.mem_map_equiv {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {f : M ≃+ N} {K : AddSubmonoid M} {x : N} :

x ∈ AddSubmonoid.map f.toAddMonoidHom K ↔ f.symm x ∈ K

source

theorem Submonoid.mem_map_equiv {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {f : M ≃* N} {K : Submonoid M} {x : N} :

x ∈ Submonoid.map f.toMonoidHom K ↔ f.symm x ∈ K

source

theorem AddSubmonoid.map_equiv_eq_comap_symm {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (f : M ≃+ N) (K : AddSubmonoid M) :

AddSubmonoid.map f.toAddMonoidHom K = AddSubmonoid.comap f.symm.toAddMonoidHom K

source

theorem Submonoid.map_equiv_eq_comap_symm {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (f : M ≃* N) (K : Submonoid M) :

Submonoid.map f.toMonoidHom K = Submonoid.comap f.symm.toMonoidHom K

source

theorem AddSubmonoid.comap_equiv_eq_map_symm {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (f : N ≃+ M) (K : AddSubmonoid M) :

AddSubmonoid.comap f K = AddSubmonoid.map f.symm K

source

theorem Submonoid.comap_equiv_eq_map_symm {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (f : N ≃* M) (K : Submonoid M) :

Submonoid.comap f K = Submonoid.map f.symm K

source

@[simp]

theorem AddSubmonoid.map_equiv_top {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (f : M ≃+ N) :

AddSubmonoid.map f ⊤ = ⊤

source

@[simp]

theorem Submonoid.map_equiv_top {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (f : M ≃* N) :

Submonoid.map f ⊤ = ⊤

source

theorem AddSubmonoid.le_prod_iff {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} :

u ≤ s.prod t ↔ AddSubmonoid.map (AddMonoidHom.fst M N) u ≤ s ∧ AddSubmonoid.map (AddMonoidHom.snd M N) u ≤ t

source

theorem Submonoid.le_prod_iff {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :

u ≤ s.prod t ↔ Submonoid.map (MonoidHom.fst M N) u ≤ s ∧ Submonoid.map (MonoidHom.snd M N) u ≤ t

source

theorem AddSubmonoid.prod_le_iff {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} :

s.prod t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u

source

theorem Submonoid.prod_le_iff {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :

s.prod t ≤ u ↔ Submonoid.map (MonoidHom.inl M N) s ≤ u ∧ Submonoid.map (MonoidHom.inr M N) t ≤ u

source

theorem AddSubmonoid.closure_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] {s : Set M} {t : Set N} (hs : 0 ∈ s) (ht : 0 ∈ t) :

AddSubmonoid.closure (s ×ˢ t) = (AddSubmonoid.closure s).prod (AddSubmonoid.closure t)

source

theorem Submonoid.closure_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] {s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :

Submonoid.closure (s ×ˢ t) = (Submonoid.closure s).prod (Submonoid.closure t)

source

def AddMonoidHom.mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid N

The range of an AddMonoidHom is an AddSubmonoid.

Equations

AddMonoidHom.mrange f = (AddSubmonoid.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source

def MonoidHom.mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid N

The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].

Equations

MonoidHom.mrange f = (Submonoid.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source

@[simp]

theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

↑(AddMonoidHom.mrange f) = Set.range ⇑f

source

@[simp]

theorem MonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

↑(MonoidHom.mrange f) = Set.range ⇑f

source

@[simp]

theorem AddMonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {y : N} :

y ∈ AddMonoidHom.mrange f ↔ ∃ (x : M), f x = y

source

@[simp]

theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {y : N} :

y ∈ MonoidHom.mrange f ↔ ∃ (x : M), f x = y

source

theorem AddMonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddMonoidHom.mrange f = AddSubmonoid.map f ⊤

source

theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

MonoidHom.mrange f = Submonoid.map f ⊤

source

@[simp]

theorem AddMonoidHom.mrange_id {M : Type u_1} [AddZeroClass M] :

AddMonoidHom.mrange (AddMonoidHom.id M) = ⊤

source

@[simp]

theorem MonoidHom.mrange_id {M : Type u_1} [MulOneClass M] :

MonoidHom.mrange (MonoidHom.id M) = ⊤

source

theorem AddMonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) :

AddSubmonoid.map g (AddMonoidHom.mrange f) = AddMonoidHom.mrange (g.comp f)

source

theorem MonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) :

Submonoid.map g (MonoidHom.mrange f) = MonoidHom.mrange (g.comp f)

source

theorem AddMonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} :

AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f

source

theorem MonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} :

MonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f

source

@[simp]

theorem AddMonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (hf : Function.Surjective ⇑f) :

AddMonoidHom.mrange f = ⊤

The range of a surjective AddMonoid hom is the whole of the codomain.

source

@[simp]

theorem MonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (hf : Function.Surjective ⇑f) :

MonoidHom.mrange f = ⊤

The range of a surjective monoid hom is the whole of the codomain.

source

theorem AddMonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (s : Set N) :

AddSubmonoid.closure (⇑f ⁻¹' s) ≤ AddSubmonoid.comap f (AddSubmonoid.closure s)

source

theorem MonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (s : Set N) :

Submonoid.closure (⇑f ⁻¹' s) ≤ Submonoid.comap f (Submonoid.closure s)

source

theorem AddMonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (s : Set M) :

AddSubmonoid.map f (AddSubmonoid.closure s) = AddSubmonoid.closure (⇑f '' s)

The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set.

source

theorem MonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (s : Set M) :

Submonoid.map f (Submonoid.closure s) = Submonoid.closure (⇑f '' s)

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.

source

@[simp]

theorem AddMonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.closure (Set.range ⇑f) = AddMonoidHom.mrange f

source

@[simp]

theorem MonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid.closure (Set.range ⇑f) = MonoidHom.mrange f

source

def AddMonoidHom.restrict {M : Type u_1} [AddZeroClass M] {N : Type u_5} {S : Type u_6} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) :

↥s →+ N

Restriction of an AddMonoid hom to an AddSubmonoid of the domain.

Equations

f.restrict s = f.comp (AddSubmonoidClass.subtype s)

Instances For

source

def MonoidHom.restrict {M : Type u_1} [MulOneClass M] {N : Type u_5} {S : Type u_6} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) :

↥s →* N

Restriction of a monoid hom to a submonoid of the domain.

Equations

f.restrict s = f.comp (SubmonoidClass.subtype s)

Instances For

source

@[simp]

theorem AddMonoidHom.restrict_apply {M : Type u_1} [AddZeroClass M] {N : Type u_5} {S : Type u_6} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : ↥s) :

(f.restrict s) x = f ↑x

source

@[simp]

theorem MonoidHom.restrict_apply {M : Type u_1} [MulOneClass M] {N : Type u_5} {S : Type u_6} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) (x : ↥s) :

(f.restrict s) x = f ↑x

source

@[simp]

theorem AddMonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) :

AddMonoidHom.mrange (f.restrict S) = AddSubmonoid.map f S

source

@[simp]

theorem MonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) :

MonoidHom.mrange (f.restrict S) = Submonoid.map f S

source

def AddMonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_5} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) :

M →+ ↥s

Restriction of an AddMonoid hom to an AddSubmonoid of the codomain.

Equations

f.codRestrict s h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_5} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) (n : M) :

(f.codRestrict s h) n = ⟨f n, ⋯⟩

source

@[simp]

theorem MonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_5} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s) (n : M) :

(f.codRestrict s h) n = ⟨f n, ⋯⟩

source

def MonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_5} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s) :

M →* ↥s

Restriction of a monoid hom to a submonoid of the codomain.

Equations

f.codRestrict s h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.injective_codRestrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_5} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) :

Function.Injective ⇑(f.codRestrict s h) ↔ Function.Injective ⇑f

source

@[simp]

theorem MonoidHom.injective_codRestrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_5} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s) :

Function.Injective ⇑(f.codRestrict s h) ↔ Function.Injective ⇑f

source

def AddMonoidHom.mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_5} [AddZeroClass N] (f : M →+ N) :

M →+ ↥(AddMonoidHom.mrange f)

Restriction of an AddMonoid hom to its range interpreted as a submonoid.

Equations

f.mrangeRestrict = f.codRestrict (AddMonoidHom.mrange f) ⋯

Instances For

source

def MonoidHom.mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_5} [MulOneClass N] (f : M →* N) :

M →* ↥(MonoidHom.mrange f)

Restriction of a monoid hom to its range interpreted as a submonoid.

Equations

f.mrangeRestrict = f.codRestrict (MonoidHom.mrange f) ⋯

Instances For

source

@[simp]

theorem AddMonoidHom.coe_mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_5} [AddZeroClass N] (f : M →+ N) (x : M) :

↑(f.mrangeRestrict x) = f x

source

@[simp]

theorem MonoidHom.coe_mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_5} [MulOneClass N] (f : M →* N) (x : M) :

↑(f.mrangeRestrict x) = f x

source

theorem AddMonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

Function.Surjective ⇑f.mrangeRestrict

source

theorem MonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :

Function.Surjective ⇑f.mrangeRestrict

source

def AddMonoidHom.mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid M

The additive kernel of an AddMonoid hom is the AddSubmonoid of elements such that f x = 0

Equations

AddMonoidHom.mker f = AddSubmonoid.comap f ⊥

Instances For

source

def MonoidHom.mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid M

The multiplicative kernel of a monoid hom is the submonoid of elements x : G such that f x = 1

Equations

MonoidHom.mker f = Submonoid.comap f ⊥

Instances For

source

@[simp]

theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {x : M} :

x ∈ AddMonoidHom.mker f ↔ f x = 0

source

@[simp]

theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {x : M} :

x ∈ MonoidHom.mker f ↔ f x = 1

source

theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

↑(AddMonoidHom.mker f) = ⇑f ⁻¹' {0}

source

theorem MonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

↑(MonoidHom.mker f) = ⇑f ⁻¹' {1}

source

instance AddMonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] [DecidableEq N] (f : F) :

DecidablePred fun (x : M) => x ∈ AddMonoidHom.mker f

Equations

AddMonoidHom.decidableMemMker f x = decidable_of_iff (f x = 0) ⋯

source

instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] [DecidableEq N] (f : F) :

DecidablePred fun (x : M) => x ∈ MonoidHom.mker f

Equations

MonoidHom.decidableMemMker f x = decidable_of_iff (f x = 1) ⋯

source

theorem AddMonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) :

AddSubmonoid.comap f (AddMonoidHom.mker g) = AddMonoidHom.mker (g.comp f)

source

theorem MonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) :

Submonoid.comap f (MonoidHom.mker g) = MonoidHom.mker (g.comp f)

source

@[simp]

theorem AddMonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.comap f ⊥ = AddMonoidHom.mker f

source

@[simp]

theorem MonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) :

Submonoid.comap f ⊥ = MonoidHom.mker f

source

@[simp]

theorem AddMonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) :

AddMonoidHom.mker (f.restrict S) = AddSubmonoid.comap S.subtype (AddMonoidHom.mker f)

source

@[simp]

theorem MonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) :

MonoidHom.mker (f.restrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)

source

theorem AddMonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

AddMonoidHom.mker f.mrangeRestrict = AddMonoidHom.mker f

source

theorem MonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) :

MonoidHom.mker f.mrangeRestrict = MonoidHom.mker f

source

@[simp]

theorem AddMonoidHom.mker_zero {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker 0 = ⊤

source

@[simp]

theorem MonoidHom.mker_one {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker 1 = ⊤

source

theorem AddMonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_5} {N' : Type u_6} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') (S : AddSubmonoid N) (S' : AddSubmonoid N') :

AddSubmonoid.comap (f.prodMap g) (S.prod S') = (AddSubmonoid.comap f S).prod (AddSubmonoid.comap g S')

source

theorem MonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_5} {N' : Type u_6} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') (S : Submonoid N) (S' : Submonoid N') :

Submonoid.comap (f.prodMap g) (S.prod S') = (Submonoid.comap f S).prod (Submonoid.comap g S')

source

theorem AddMonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_5} {N' : Type u_6} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') :

AddMonoidHom.mker (f.prodMap g) = (AddMonoidHom.mker f).prod (AddMonoidHom.mker g)

source

theorem MonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_5} {N' : Type u_6} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') :

MonoidHom.mker (f.prodMap g) = (MonoidHom.mker f).prod (MonoidHom.mker g)

source

@[simp]

theorem AddMonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.inl M N) = ⊥

source

@[simp]

theorem MonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.inl M N) = ⊥

source

@[simp]

theorem AddMonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.inr M N) = ⊥

source

@[simp]

theorem MonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.inr M N) = ⊥

source

@[simp]

theorem AddMonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.fst M N) = ⊥.prod ⊤

source

@[simp]

theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.fst M N) = ⊥.prod ⊤

source

@[simp]

theorem AddMonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.snd M N) = ⊤.prod ⊥

source

@[simp]

theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.snd M N) = ⊤.prod ⊥

source

def AddMonoidHom.addSubmonoidComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) :

↥(AddSubmonoid.comap f N') →+ ↥N'

the AddMonoidHom from the preimage of an additive submonoid to itself.

Equations

f.addSubmonoidComap N' = { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MonoidHom.submonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (x : ↥(Submonoid.comap f N')) :

↑((f.submonoidComap N') x) = f ↑x

source

@[simp]

theorem AddMonoidHom.addSubmonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : ↥(AddSubmonoid.comap f N')) :

↑((f.addSubmonoidComap N') x) = f ↑x

source

def MonoidHom.submonoidComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) :

↥(Submonoid.comap f N') →* ↥N'

The MonoidHom from the preimage of a submonoid to itself.

Equations

f.submonoidComap N' = { toFun := fun (x : ↥(Submonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.addSubmonoidMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :

↥M' →+ ↥(AddSubmonoid.map f M')

the AddMonoidHom from an additive submonoid to its image. See AddEquiv.AddSubmonoidMap for a variant for AddEquivs.

Equations

f.addSubmonoidMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.addSubmonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : ↥M') :

↑((f.addSubmonoidMap M') x) = f ↑x

source

@[simp]

theorem MonoidHom.submonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) (x : ↥M') :

↑((f.submonoidMap M') x) = f ↑x

source

def MonoidHom.submonoidMap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) :

↥M' →* ↥(Submonoid.map f M')

The MonoidHom from a submonoid to its image. See MulEquiv.SubmonoidMap for a variant for MulEquivs.

Equations

f.submonoidMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem AddMonoidHom.addSubmonoidMap_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :

Function.Surjective ⇑(f.addSubmonoidMap M')

source

theorem MonoidHom.submonoidMap_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) :

Function.Surjective ⇑(f.submonoidMap M')

source

theorem AddSubmonoid.mrange_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inl M N) = ⊤.prod ⊥

source

theorem Submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inl M N) = ⊤.prod ⊥

source

theorem AddSubmonoid.mrange_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊥.prod ⊤

source

theorem Submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inr M N) = ⊥.prod ⊤

source

theorem AddSubmonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inl M N) = AddSubmonoid.comap (AddMonoidHom.snd M N) ⊥

source

theorem Submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inl M N) = Submonoid.comap (MonoidHom.snd M N) ⊥

source

theorem AddSubmonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inr M N) = AddSubmonoid.comap (AddMonoidHom.fst M N) ⊥

source

theorem Submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inr M N) = Submonoid.comap (MonoidHom.fst M N) ⊥

source

@[simp]

theorem AddSubmonoid.mrange_fst {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.fst M N) = ⊤

source

@[simp]

theorem Submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.fst M N) = ⊤

source

@[simp]

theorem AddSubmonoid.mrange_snd {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.snd M N) = ⊤

source

@[simp]

theorem Submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.snd M N) = ⊤

source

theorem AddSubmonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} :

s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

source

theorem Submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :

s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

source

theorem AddSubmonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} :

s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

source

theorem Submonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :

s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

source

@[simp]

theorem AddSubmonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inl M N) ⊔ AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊤

source

@[simp]

theorem Submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inl M N) ⊔ MonoidHom.mrange (MonoidHom.inr M N) = ⊤

source

def AddSubmonoid.inclusion {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S ≤ T) :

↥S →+ ↥T

The AddMonoid hom associated to an inclusion of submonoids.

Equations

AddSubmonoid.inclusion h = S.subtype.codRestrict T ⋯

Instances For

source

def Submonoid.inclusion {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S ≤ T) :

↥S →* ↥T

The monoid hom associated to an inclusion of submonoids.

Equations

Submonoid.inclusion h = S.subtype.codRestrict T ⋯

Instances For

source

@[simp]

theorem AddSubmonoid.range_subtype {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) :

AddMonoidHom.mrange s.subtype = s

source

@[simp]

theorem Submonoid.range_subtype {M : Type u_1} [MulOneClass M] (s : Submonoid M) :

MonoidHom.mrange s.subtype = s

source

theorem AddSubmonoid.eq_top_iff' {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

source

theorem Submonoid.eq_top_iff' {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

source

theorem AddSubmonoid.eq_bot_iff_forall {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

S = ⊥ ↔ ∀ x ∈ S, x = 0

source

theorem Submonoid.eq_bot_iff_forall {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

S = ⊥ ↔ ∀ x ∈ S, x = 1

source

theorem AddSubmonoid.eq_bot_of_subsingleton {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) [Subsingleton ↥S] :

S = ⊥

source

theorem Submonoid.eq_bot_of_subsingleton {M : Type u_1} [MulOneClass M] (S : Submonoid M) [Subsingleton ↥S] :

S = ⊥

source

theorem AddSubmonoid.nontrivial_iff_exists_ne_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 0

source

theorem Submonoid.nontrivial_iff_exists_ne_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 1

source

theorem AddSubmonoid.bot_or_nontrivial {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

S = ⊥ ∨ Nontrivial ↥S

An additive submonoid is either the trivial additive submonoid or nontrivial.

source

theorem Submonoid.bot_or_nontrivial {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

S = ⊥ ∨ Nontrivial ↥S

A submonoid is either the trivial submonoid or nontrivial.

source

theorem AddSubmonoid.bot_or_exists_ne_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

S = ⊥ ∨ ∃ x ∈ S, x ≠ 0

An additive submonoid is either the trivial additive submonoid or contains a nonzero element.

source

theorem Submonoid.bot_or_exists_ne_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

S = ⊥ ∨ ∃ x ∈ S, x ≠ 1

A submonoid is either the trivial submonoid or contains a nonzero element.

source

def AddEquiv.addSubmonoidCongr {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

↥S ≃+ ↥T

Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.

Equations

AddEquiv.addSubmonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }

Instances For

source

def MulEquiv.submonoidCongr {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S = T) :

↥S ≃* ↥T

Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.

Equations

MulEquiv.submonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

M ≃+ ↥(AddMonoidHom.mrange f)

An additive monoid homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.mrange. This is a bidirectional version of AddMonoidHom.mrange_restrict.

Equations

AddEquiv.ofLeftInverse' f h = { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(AddMonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a : M) :

(AddEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a

source

@[simp]

theorem MulEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

∀ (a : ↥(MonoidHom.mrange f)), (MulEquiv.ofLeftInverse' f h).symm a = g ↑a

source

@[simp]

theorem MulEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a : M) :

(MulEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a

source

@[simp]

theorem AddEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

∀ (a : ↥(AddMonoidHom.mrange f)), (AddEquiv.ofLeftInverse' f h).symm a = g ↑a

source

def MulEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

M ≃* ↥(MonoidHom.mrange f)

A monoid homomorphism f : M →* N with a left-inverse g : N → M defines a multiplicative equivalence between M and f.mrange. This is a bidirectional version of MonoidHom.mrange_restrict.

Equations

MulEquiv.ofLeftInverse' f h = { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(MonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.addSubmonoidMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :

↥S ≃+ ↥(AddSubmonoid.map e S)

An AddEquiv φ between two additive monoids M and N induces an AddEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See AddMonoidHom.addSubmonoidMap for a variant for AddMonoidHoms.

Equations

e.addSubmonoidMap S = { toEquiv := (↑e).image ↑S, map_add' := ⋯ }

Instances For

source

def MulEquiv.submonoidMap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) :

↥S ≃* ↥(Submonoid.map e S)

A MulEquiv φ between two monoids M and N induces a MulEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See MonoidHom.submonoidMap for a variant for MonoidHoms.

Equations

e.submonoidMap S = { toEquiv := (↑e).image ↑S, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.coe_addSubmonoidMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : ↥S) :

↑((e.addSubmonoidMap S) g) = e ↑g

source

@[simp]

theorem MulEquiv.coe_submonoidMap_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : ↥S) :

↑((e.submonoidMap S) g) = e ↑g

source

@[simp]

theorem AddEquiv.add_submonoid_map_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : ↥(AddSubmonoid.map (↑e) S)) :

(e.addSubmonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩

source

@[simp]

theorem MulEquiv.submonoidMap_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : ↥(Submonoid.map (↑e) S)) :

(e.submonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩

source

@[simp]

theorem AddSubmonoid.equivMapOfInjective_coe_addEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (e : M ≃+ N) :

S.equivMapOfInjective ↑e ⋯ = e.addSubmonoidMap S

source

@[simp]

theorem Submonoid.equivMapOfInjective_coe_mulEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (e : M ≃* N) :

S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Actions by `Submonoid`s #

These instances transfer the action by an element m : M of a monoid M written as m • a onto the action by an element s : S of a submonoid S : Submonoid M such that s • a = (s : M) • a.

These instances work particularly well in conjunction with Monoid.toMulAction, enabling s • m as an alias for ↑s * m.

source

instance AddSubmonoid.vadd {M' : Type u_4} {α : Type u_5} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') :

VAdd (↥S) α

Equations

S.vadd = VAdd.comp α ⇑S.subtype

source

instance Submonoid.smul {M' : Type u_4} {α : Type u_5} [MulOneClass M'] [SMul M' α] (S : Submonoid M') :

SMul (↥S) α

Equations

S.smul = SMul.comp α ⇑S.subtype

source

instance AddSubmonoid.vaddCommClass_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') :

VAddCommClass (↥S) α β

Equations

⋯ = ⋯

source

instance Submonoid.smulCommClass_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [MulOneClass M'] [SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') :

SMulCommClass (↥S) α β

Equations

⋯ = ⋯

source

instance AddSubmonoid.vaddCommClass_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') :

VAddCommClass α (↥S) β

Equations

⋯ = ⋯

source

instance Submonoid.smulCommClass_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [MulOneClass M'] [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') :

SMulCommClass α (↥S) β

Equations

⋯ = ⋯

source

instance Submonoid.isScalarTower {M' : Type u_4} {α : Type u_5} {β : Type u_6} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') :

IsScalarTower (↥S) α β

Note that this provides IsScalarTower S M' M' which is needed by SMulMulAssoc.

Equations

⋯ = ⋯

source

theorem AddSubmonoid.vadd_def {M' : Type u_4} {α : Type u_5} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : ↥S) (a : α) :

g +ᵥ a = ↑g +ᵥ a

source

theorem Submonoid.smul_def {M' : Type u_4} {α : Type u_5} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α) :

g • a = ↑g • a

source

@[simp]

theorem AddSubmonoid.mk_vadd {M' : Type u_4} {α : Type u_5} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : M') (hg : g ∈ S) (a : α) :

⟨g, hg⟩ +ᵥ a = g +ᵥ a

source

@[simp]

theorem Submonoid.mk_smul {M' : Type u_4} {α : Type u_5} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : M') (hg : g ∈ S) (a : α) :

⟨g, hg⟩ • a = g • a

source

instance Submonoid.faithfulSMul {M' : Type u_4} {α : Type u_5} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} [FaithfulSMul M' α] :

FaithfulSMul (↥S) α

Equations

⋯ = ⋯

source

instance AddSubmonoid.addAction {M' : Type u_4} {α : Type u_5} [AddMonoid M'] [AddAction M' α] (S : AddSubmonoid M') :

AddAction (↥S) α

The additive action by an AddSubmonoid is the action by the underlying AddMonoid.

Equations

S.addAction = AddAction.compHom α S.subtype

source

instance Submonoid.mulAction {M' : Type u_4} {α : Type u_5} [Monoid M'] [MulAction M' α] (S : Submonoid M') :

MulAction (↥S) α

The action by a submonoid is the action by the underlying monoid.

Equations

S.mulAction = MulAction.compHom α S.subtype

source

noncomputable def AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid {M : Type u_1} [AddMonoid M] :

AddUnits M ≃+ ↥(IsAddUnit.addSubmonoid M)

The additive equivalence between the type of additive units of M and the additive submonoid whose elements are the additive units of M.

Equations

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

Instances For

source

@[simp]

theorem AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :

↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑x

source

@[simp]

theorem Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_1} [Monoid M] (x : ↥(IsUnit.submonoid M)) :

↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x)⁻¹ = ↑(Classical.choose ⋯)⁻¹

source

@[simp]

theorem AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) :

↑(-AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑(-Classical.choose ⋯)

source

@[simp]

theorem Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_1} [Monoid M] (x : ↥(IsUnit.submonoid M)) :

↑(Submonoid.unitsTypeEquivIsUnitSubmonoid.symm x) = ↑x

source

@[simp]

theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe {M : Type u_1} [AddMonoid M] (x : AddUnits M) :

↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid x) = ↑x

source

@[simp]

theorem Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe {M : Type u_1} [Monoid M] (x : Mˣ) :

↑(Submonoid.unitsTypeEquivIsUnitSubmonoid x) = ↑x

source

noncomputable def Submonoid.unitsTypeEquivIsUnitSubmonoid {M : Type u_1} [Monoid M] :

Mˣ ≃* ↥(IsUnit.submonoid M)

The multiplicative equivalence between the type of units of M and the submonoid of unit elements of M.

Equations

Submonoid.unitsTypeEquivIsUnitSubmonoid = { toFun := fun (x : Mˣ) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥(IsUnit.submonoid M)) => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }