Operations on Submonoids

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 MonoidHoms

• 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.domRestrict: restrict a monoid homomorphism to a submonoid of its domain;
• MonoidHom.restrict: restrict the domain and codomain of a monoid homomorphism;
• 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

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.

@[simp]

theorem Submonoid.coe_toAddSubmonoid_apply {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ↑(toAddSubmonoid S) = ⇑Additive.toMul ⁻¹' ↑S

@[simp]

theorem Submonoid.coe_toAddSubmonoid_symm_apply {M : Type u_1} [MulOneClass M] (S : AddSubmonoid (Additive M)) : ↑((RelIso.symm toAddSubmonoid) S) = ⇑Additive.ofMul ⁻¹' ↑S

@[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.

theorem Submonoid.toAddSubmonoid_closure {M : Type u_1} [MulOneClass M] (S : Set M) : toAddSubmonoid (closure S) = AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S)

theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [MulOneClass M] (S : Set (Additive M)) : toSubmonoid' (closure S) = Submonoid.closure (⇑Additive.ofMul ⁻¹' S)

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.

@[simp]

theorem AddSubmonoid.coe_toSubmonoid_apply {A : Type u_4} [AddZeroClass A] (S : AddSubmonoid A) : ↑(toSubmonoid S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem AddSubmonoid.coe_toSubmonoid_symm_apply {A : Type u_4} [AddZeroClass A] (S : Submonoid (Multiplicative A)) : ↑((RelIso.symm toSubmonoid) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S

@[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.

theorem AddSubmonoid.toSubmonoid_closure {A : Type u_4} [AddZeroClass A] (S : Set A) : toSubmonoid (closure S) = Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

theorem Submonoid.toAddSubmonoid'_closure {A : Type u_4} [AddZeroClass A] (S : Set (Multiplicative A)) : toAddSubmonoid' (closure S) = AddSubmonoid.closure (⇑Multiplicative.ofAdd ⁻¹' S)

comap and map

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 MonoidHom is a Submonoid.

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 AddMonoidHom is an AddSubmonoid.

@[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) : ↑(comap f S) = ⇑f ⁻¹' ↑S

@[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) : ↑(comap f S) = ⇑f ⁻¹' ↑S

@[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 ∈ comap f S ↔ f x ∈ S

@[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 ∈ comap f S ↔ f x ∈ S

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) : comap f (comap g S) = comap (g.comp f) S

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) : comap f (comap g S) = comap (g.comp f) S

@[simp]

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

@[simp]

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

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 MonoidHom is a Submonoid.

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 AddMonoidHom is an AddSubmonoid.

@[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) : ↑(map f S) = ⇑f '' ↑S

@[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) : ↑(map f S) = ⇑f '' ↑S

@[simp]

theorem Submonoid.map_coe_toMonoidHom {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) : map (↑f) S = map f S

@[simp]

theorem AddSubmonoid.map_coe_toAddMonoidHom {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) : map (↑f) S = map f S

@[simp]

theorem Submonoid.map_coe_toMulEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [EquivLike F M N] [MulEquivClass F M N] (f : F) (S : Submonoid M) : map (↑f) S = map f S

@[simp]

theorem AddSubmonoid.map_coe_toAddEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [EquivLike F M N] [AddEquivClass F M N] (f : F) (S : AddSubmonoid M) : map (↑f) S = map f S

@[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 ∈ map f S ↔ ∃ x ∈ S, f x = y

@[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 ∈ map f S ↔ ∃ x ∈ S, f x = y

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 ∈ map f S

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 ∈ map f S

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 ∈ map f S

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 ∈ map f S

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) : map g (map f S) = map (g.comp f) S

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) : map g (map f S) = map (g.comp f) S

@[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 ∈ map f S ↔ x ∈ S

@[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 ∈ map f S ↔ x ∈ S

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} : map f S ≤ T ↔ S ≤ comap f T

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} : map f S ≤ T ↔ S ≤ comap f T

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 (map f) (comap f)

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 (map f) (comap f)

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 ≤ comap f T → map f S ≤ T

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 ≤ comap f T → map f S ≤ T

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} : map f S ≤ T → S ≤ comap f T

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} : map f S ≤ T → S ≤ comap f T

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 ≤ comap f (map f S)

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 ≤ comap f (map f S)

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} : map f (comap f S) ≤ S

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} : map f (comap f S) ≤ S

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 (map f)

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 (map f)

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 (comap f)

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 (comap f)

@[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} : map f (comap f (map f S)) = map f S

@[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} : map f (comap f (map f S)) = map f S

@[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} : comap f (map f (comap f S)) = comap f S

@[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} : comap f (map f (comap f S)) = comap f S

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 T : Submonoid M) (f : F) : map f (S ⊔ T) = map f S ⊔ map f T

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 T : AddSubmonoid M) (f : F) : map f (S ⊔ T) = map f S ⊔ map f T

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) : map f (iSup s) = ⨆ (i : ι), map f (s i)

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) : map f (iSup s) = ⨆ (i : ι), map f (s i)

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 T : Submonoid M) (f : F) (hf : Function.Injective ⇑f) : map f (S ⊓ T) = map f S ⊓ map f T

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 T : AddSubmonoid M) (f : F) (hf : Function.Injective ⇑f) : map f (S ⊓ T) = map f S ⊓ map f T

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) : map f (iInf s) = ⨅ (i : ι), map f (s i)

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) : map f (iInf s) = ⨅ (i : ι), map f (s i)

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 T : Submonoid N) (f : F) : comap f (S ⊓ T) = comap f S ⊓ comap f T

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 T : AddSubmonoid N) (f : F) : comap f (S ⊓ T) = comap f S ⊓ comap f T

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) : comap f (iInf s) = ⨅ (i : ι), comap f (s i)

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) : comap f (iInf s) = ⨅ (i : ι), comap f (s i)

@[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) : map f ⊥ = ⊥

@[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) : map f ⊥ = ⊥

theorem Submonoid.disjoint_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} (hf : Function.Injective ⇑f) {H K : Submonoid M} (h : Disjoint H K) : Disjoint (map f H) (map f K)

theorem AddSubmonoid.disjoint_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} (hf : Function.Injective ⇑f) {H K : AddSubmonoid M} (h : Disjoint H K) : Disjoint (map f H) (map f K)

@[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) : comap f ⊤ = ⊤

@[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) : comap f ⊤ = ⊤

@[simp]

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

@[simp]

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

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 (map f) (comap f)

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

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 (map f) (comap f)

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

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) : comap f (map f S) = S

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) : comap f (map f S) = S

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 (comap f)

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 (comap f)

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 (map f)

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 (map f)

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 T : Submonoid M) : comap f (map f S ⊓ map f T) = S ⊓ T

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 T : AddSubmonoid M) : comap f (map f S ⊓ map f T) = S ⊓ T

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) : comap f (⨅ (i : ι), map f (S i)) = iInf S

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) : comap f (⨅ (i : ι), map f (S i)) = iInf S

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 T : Submonoid M) : comap f (map f S ⊔ map f T) = S ⊔ T

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 T : AddSubmonoid M) : comap f (map f S ⊔ map f T) = S ⊔ T

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) : comap f (⨆ (i : ι), map f (S i)) = iSup S

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) : comap f (⨆ (i : ι), map f (S i)) = iSup S

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 T : Submonoid M} : map f S ≤ map f T ↔ S ≤ T

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 T : AddSubmonoid M} : map f S ≤ map f T ↔ S ≤ T

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 (map f)

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 (map f)

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 (map f) (comap f)

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

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 (map f) (comap f)

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

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) : map f (comap f S) = S

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) : map f (comap f S) = S

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 (map f)

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 (map f)

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 (comap f)

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 (comap f)

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 T : Submonoid N) : map f (comap f S ⊓ comap f T) = S ⊓ T

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 T : AddSubmonoid N) : map f (comap f S ⊓ comap f T) = S ⊓ T

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) : map f (⨅ (i : ι), comap f (S i)) = iInf S

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) : map f (⨅ (i : ι), comap f (S i)) = iInf S

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 T : Submonoid N) : map f (comap f S ⊔ comap f T) = S ⊔ T

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 T : AddSubmonoid N) : map f (comap f S ⊔ comap f T) = S ⊔ T

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) : map f (⨆ (i : ι), comap f (S i)) = iSup S

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) : map f (⨆ (i : ι), comap f (S i)) = iSup S

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 T : Submonoid N} : comap f S ≤ comap f T ↔ S ≤ T

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 T : AddSubmonoid N} : comap f S ≤ comap f T ↔ S ≤ T

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 (comap f)

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 (comap f)

def Submonoid.topEquiv {M : Type u_5} [MulOneClass M] : ↥⊤ ≃* M

The top Submonoid is isomorphic to the Monoid.

def AddSubmonoid.topEquiv {M : Type u_5} [AddZeroClass M] : ↥⊤ ≃+ M

The top AddSubmonoid is isomorphic to the AddMonoid.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Submonoid.topEquiv_toMonoidHom {M : Type u_5} [MulOneClass M] : ↑topEquiv = ⊤.subtype

@[simp]

theorem AddSubmonoid.topEquiv_toAddMonoidHom {M : Type u_5} [AddZeroClass M] : ↑topEquiv = ⊤.subtype

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 ≃* ↥(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.

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 ≃+ ↥(map f S)

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

@[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

@[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

@[simp]

theorem Submonoid.closure_closure_coe_preimage {M : Type u_5} [MulOneClass M] {s : Set M} : closure (Subtype.val ⁻¹' s) = ⊤

@[simp]

theorem AddSubmonoid.closure_closure_coe_preimage {M : Type u_5} [AddZeroClass M] {s : Set M} : closure (Subtype.val ⁻¹' s) = ⊤

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.

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.

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

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

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

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

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

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

theorem Submonoid.prod_top {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) : s.prod ⊤ = comap (MonoidHom.fst M N) s

theorem AddSubmonoid.prod_top {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) : s.prod ⊤ = comap (AddMonoidHom.fst M N) s

theorem Submonoid.top_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid N) : ⊤.prod s = comap (MonoidHom.snd M N) s

theorem AddSubmonoid.top_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid N) : ⊤.prod s = comap (AddMonoidHom.snd M N) s

@[simp]

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

@[simp]

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

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

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

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.

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 AddSubmonoids is isomorphic to their product as AddMonoids.

theorem Submonoid.map_inl {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid M) : map (MonoidHom.inl M N) s = s.prod ⊥

theorem AddSubmonoid.map_inl {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid M) : map (AddMonoidHom.inl M N) s = s.prod ⊥

theorem Submonoid.map_inr {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Submonoid N) : map (MonoidHom.inr M N) s = ⊥.prod s

theorem AddSubmonoid.map_inr {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : AddSubmonoid N) : map (AddMonoidHom.inr M N) s = ⊥.prod s

@[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

@[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

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 ∈ map f.toMonoidHom K ↔ f.symm x ∈ K

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 ∈ map f.toAddMonoidHom K ↔ f.symm x ∈ K

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) : map f K = comap f.symm K

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) : map f K = comap f.symm K

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) : comap f K = map f.symm K

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) : comap f K = map f.symm K

@[simp]

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

@[simp]

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

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 ↔ map (MonoidHom.fst M N) u ≤ s ∧ map (MonoidHom.snd M N) u ≤ t

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 ↔ map (AddMonoidHom.fst M N) u ≤ s ∧ map (AddMonoidHom.snd M N) u ≤ t

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 ↔ map (MonoidHom.inl M N) s ≤ u ∧ map (MonoidHom.inr M N) t ≤ u

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 ↔ map (AddMonoidHom.inl M N) s ≤ u ∧ map (AddMonoidHom.inr M N) t ≤ u

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) : closure (s ×ˢ t) = (closure s).prod (closure t)

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) : closure (s ×ˢ t) = (closure s).prod (closure t)

@[simp]

theorem Submonoid.closure_prod_one {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (s : Set M) : closure (s ×ˢ {1}) = (closure s).prod ⊥

@[simp]

theorem AddSubmonoid.closure_prod_zero {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (s : Set M) : closure (s ×ˢ {0}) = (closure s).prod ⊥

@[simp]

theorem Submonoid.closure_one_prod {N : Type u_2} [MulOneClass N] {M : Type u_5} [MulOneClass M] (t : Set N) : closure ({1} ×ˢ t) = ⊥.prod (closure t)

@[simp]

theorem AddSubmonoid.closure_zero_prod {N : Type u_2} [AddZeroClass N] {M : Type u_5} [AddZeroClass M] (t : Set N) : closure ({0} ×ˢ t) = ⊥.prod (closure t)

def LibraryNote.range_copy_pattern : Batteries.Util.LibraryNote

For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism f is a subobject of the codomain. When this is the case, it is useful to define the range of a morphism in such a way that the underlying carrier set of the range subobject is definitionally Set.range f. In particular this means that the types ↥(Set.range f) and ↥f.range are interchangeable without proof obligations.

A convenient candidate definition for range which is mathematically correct is map ⊤ f, just as Set.range could have been defined as f '' Set.univ. However, this lacks the desired definitional convenience, in that it both does not match Set.range, and that it introduces a redundant x ∈ ⊤ term which clutters proofs. In such a case one may resort to the copy pattern. A copy function converts the definitional problem for the carrier set of a subobject into a one-off propositional proof obligation which one discharges while writing the definition of the definitionally convenient range (the parameter hs in the example below).

A good example is the case of a morphism of monoids. A convenient definition for MonoidHom.mrange would be (⊤ : Submonoid M).map f. However since this lacks the required definitional convenience, we first define Submonoid.copy as follows:

protected def copy (S : Submonoid M) (s : Set M) (hs : s = S) : Submonoid M :=
  { carrier  := s,
    one_mem' := hs.symm ▸ S.one_mem',
    mul_mem' := hs.symm ▸ S.mul_mem' }

and then finally define:

def mrange (f : M →* N) : Submonoid N :=
  ((⊤ : Submonoid M).map f).copy (Set.range f) Set.image_univ.symm

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 MonoidHom is a Submonoid. See Note [range copy pattern].

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.

@[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) : ↑(mrange f) = Set.range ⇑f

@[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) : ↑(mrange f) = Set.range ⇑f

@[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 ∈ mrange f ↔ ∃ (x : M), f x = y

@[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 ∈ mrange f ↔ ∃ (x : M), f x = y

theorem MonoidHom.mrange_comp {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {O : Type u_5} [MulOneClass O] (f : N →* O) (g : M →* N) : mrange (f.comp g) = Submonoid.map f (mrange g)

theorem AddMonoidHom.mrange_comp {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {O : Type u_5} [AddZeroClass O] (f : N →+ O) (g : M →+ N) : mrange (f.comp g) = AddSubmonoid.map f (mrange g)

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) : mrange f = Submonoid.map f ⊤

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) : mrange f = AddSubmonoid.map f ⊤

@[simp]

theorem MonoidHom.mrange_id {M : Type u_1} [MulOneClass M] : mrange (id M) = ⊤

@[simp]

theorem AddMonoidHom.mrange_id {M : Type u_1} [AddZeroClass M] : mrange (id M) = ⊤

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 (mrange f) = mrange (g.comp f)

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 (mrange f) = mrange (g.comp f)

theorem MonoidHom.mrange_eq_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} : mrange f = ⊤ ↔ Function.Surjective ⇑f

theorem AddMonoidHom.mrange_eq_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} : mrange f = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem MonoidHom.mrange_prodMap {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') : mrange (f.prodMap g) = (mrange f).prod (mrange g)

@[simp]

theorem AddMonoidHom.mrange_prodMap {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') : mrange (f.prodMap g) = (mrange f).prod (mrange g)

@[simp]

theorem MonoidHom.mrange_eq_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) : mrange f = ⊤

The range of a surjective MonoidHom is the whole of the codomain.

@[simp]

theorem AddMonoidHom.mrange_eq_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) : mrange f = ⊤

The range of a surjective AddMonoidHom is the whole of the codomain.

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)

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)

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 MonoidHom of the Submonoid generated by a set equals the Submonoid generated by the image of the set.

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 AddMonoidHom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set.

@[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) = mrange f

@[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) = mrange f

def MonoidHom.domRestrict {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 MonoidHom to a Submonoid of the domain.

def AddMonoidHom.domRestrict {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 AddMonoidHom to an AddSubmonoid of the domain.

@[simp]

theorem MonoidHom.domRestrict_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.domRestrict s) x = f ↑x

@[simp]

theorem AddMonoidHom.domRestrict_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.domRestrict s) x = f ↑x

@[deprecated MonoidHom.domRestrict_apply (since := "2026-07-19")]

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.domRestrict s) x = f ↑x

Alias of MonoidHom.domRestrict_apply.

@[deprecated AddMonoidHom.domRestrict_apply (since := "2026-07-19")]

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.domRestrict s) x = f ↑x

Alias of AddMonoidHom.domRestrict_apply.

@[simp]

theorem MonoidHom.domRestrict_eq_one_iff {M : Type u_1} [MulOneClass M] {N : Type u_5} {S : Type u_6} [MulOneClass N] {f : M →* N} [SetLike S M] [SubmonoidClass S M] {s : S} : f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1

@[simp]

theorem AddMonoidHom.domRestrict_eq_zero_iff {M : Type u_1} [AddZeroClass M] {N : Type u_5} {S : Type u_6} [AddZeroClass N] {f : M →+ N} [SetLike S M] [AddSubmonoidClass S M] {s : S} : f.domRestrict s = 0 ↔ ∀ x ∈ s, f x = 0

@[deprecated MonoidHom.domRestrict_eq_one_iff (since := "2026-07-19")]

theorem MonoidHom.restrict_eq_one_iff {M : Type u_1} [MulOneClass M] {N : Type u_5} {S : Type u_6} [MulOneClass N] {f : M →* N} [SetLike S M] [SubmonoidClass S M] {s : S} : f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1

Alias of MonoidHom.domRestrict_eq_one_iff.

@[deprecated AddMonoidHom.domRestrict_eq_zero_iff (since := "2026-07-19")]

theorem AddMonoidHom.restrict_eq_zero_iff {M : Type u_1} [AddZeroClass M] {N : Type u_5} {S : Type u_6} [AddZeroClass N] {f : M →+ N} [SetLike S M] [AddSubmonoidClass S M] {s : S} : f.domRestrict s = 0 ↔ ∀ x ∈ s, f x = 0

Alias of AddMonoidHom.domRestrict_eq_zero_iff.

@[simp]

theorem MonoidHom.domRestrict_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) : mrange (f.domRestrict S) = Submonoid.map f S

@[simp]

theorem AddMonoidHom.domRestrict_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) : mrange (f.domRestrict S) = AddSubmonoid.map f S

@[deprecated MonoidHom.domRestrict_mrange (since := "2026-07-19")]

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

Alias of MonoidHom.domRestrict_mrange.

@[deprecated AddMonoidHom.domRestrict_mrange (since := "2026-07-19")]

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

Alias of AddMonoidHom.domRestrict_mrange.

def MonoidHom.domRestrictHom {M : Type u_1} [MulOneClass M] {S : Type u_5} [SetLike S M] [SubmonoidClass S M] (M' : S) (A : Type u_6) [CommMonoid A] : (M →* A) →* ↥M' →* A

A version of MonoidHom.domRestrict as a homomorphism.

def AddMonoidHom.domRestrictHom {M : Type u_1} [AddZeroClass M] {S : Type u_5} [SetLike S M] [AddSubmonoidClass S M] (M' : S) (A : Type u_6) [AddCommMonoid A] : (M →+ A) →+ ↥M' →+ A

A version of AddMonoidHom.domRestrict as a homomorphism.

@[simp]

theorem AddMonoidHom.domRestrictHom_apply {M : Type u_1} [AddZeroClass M] {S : Type u_5} [SetLike S M] [AddSubmonoidClass S M] (M' : S) (A : Type u_6) [AddCommMonoid A] (f : M →+ A) : (domRestrictHom M' A) f = f.domRestrict M'

@[simp]

theorem MonoidHom.domRestrictHom_apply {M : Type u_1} [MulOneClass M] {S : Type u_5} [SetLike S M] [SubmonoidClass S M] (M' : S) (A : Type u_6) [CommMonoid A] (f : M →* A) : (domRestrictHom M' A) f = f.domRestrict M'

@[deprecated MonoidHom.domRestrictHom (since := "2026-07-19")]

def MonoidHom.restrictHom {M : Type u_1} [MulOneClass M] {S : Type u_5} [SetLike S M] [SubmonoidClass S M] (M' : S) (A : Type u_6) [CommMonoid A] : (M →* A) →* ↥M' →* A

Alias of MonoidHom.domRestrictHom.

---

A version of MonoidHom.domRestrict as a homomorphism.

@[deprecated AddMonoidHom.domRestrictHom (since := "2026-07-19")]

def AddMonoidHom.restrictHom {M : Type u_1} [AddZeroClass M] {S : Type u_5} [SetLike S M] [AddSubmonoidClass S M] (M' : S) (A : Type u_6) [AddCommMonoid A] : (M →+ A) →+ ↥M' →+ A

Alias of AddMonoidHom.domRestrictHom.

---

A version of AddMonoidHom.domRestrict as a homomorphism.

@[deprecated MonoidHom.domRestrictHom_apply (since := "2026-07-19")]

theorem MonoidHom.restrictHom_apply {M : Type u_1} [MulOneClass M] {S : Type u_5} [SetLike S M] [SubmonoidClass S M] (M' : S) (A : Type u_6) [CommMonoid A] (f : M →* A) : (domRestrictHom M' A) f = f.domRestrict M'

Alias of MonoidHom.domRestrictHom_apply.

@[deprecated AddMonoidHom.domRestrictHom_apply (since := "2026-07-19")]

theorem AddMonoidHom.restrictHom_apply {M : Type u_1} [AddZeroClass M] {S : Type u_5} [SetLike S M] [AddSubmonoidClass S M] (M' : S) (A : Type u_6) [AddCommMonoid A] (f : M →+ A) : (domRestrictHom M' A) f = f.domRestrict M'

Alias of AddMonoidHom.domRestrictHom_apply.

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 MonoidHom to a Submonoid of the codomain.

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 AddMonoidHom to an AddSubmonoid of the codomain.

@[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, ⋯⟩

@[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, ⋯⟩

@[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

@[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

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

Restriction of a MonoidHom to its range interpreted as a Submonoid.

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

Restriction of an AddMonoidHom to its range interpreted as an AddSubmonoid.

@[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

@[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

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

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

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 MonoidHom is the Submonoid of elements x : G such that f x = 1.

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 AddMonoidHom is the AddSubmonoid of elements such that f x = 0.

@[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 ∈ mker f ↔ f x = 1

@[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 ∈ mker f ↔ f x = 0

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) : ↑(mker f) = ⇑f ⁻¹' {1}

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) : ↑(mker f) = ⇑f ⁻¹' {0}

@[instance_reducible]

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 ∈ mker f

@[instance_reducible]

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 ∈ mker f

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 (mker g) = mker (g.comp f)

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 (mker g) = mker (g.comp f)

@[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 ⊥ = mker f

@[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 ⊥ = mker f

@[simp]

theorem MonoidHom.domRestrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) : mker (f.domRestrict S) = Submonoid.comap S.subtype (mker f)

@[simp]

theorem AddMonoidHom.domRestrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) : mker (f.domRestrict S) = AddSubmonoid.comap S.subtype (mker f)

@[deprecated MonoidHom.domRestrict_mker (since := "2026-07-19")]

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

Alias of MonoidHom.domRestrict_mker.

@[deprecated AddMonoidHom.domRestrict_mker (since := "2026-07-19")]

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

Alias of AddMonoidHom.domRestrict_mker.

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

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

@[simp]

theorem MonoidHom.mker_one {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : mker 1 = ⊤

@[simp]

theorem AddMonoidHom.mker_zero {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : mker 0 = ⊤

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')

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')

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') : mker (f.prodMap g) = (mker f).prod (mker g)

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') : mker (f.prodMap g) = (mker f).prod (mker g)

@[simp]

theorem MonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : mker (inl M N) = ⊥

@[simp]

theorem AddMonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : mker (inl M N) = ⊥

@[simp]

theorem MonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : mker (inr M N) = ⊥

@[simp]

theorem AddMonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : mker (inr M N) = ⊥

@[simp]

theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : mker (fst M N) = ⊥.prod ⊤

@[simp]

theorem AddMonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : mker (fst M N) = ⊥.prod ⊤

@[simp]

theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : mker (snd M N) = ⊤.prod ⊥

@[simp]

theorem AddMonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : mker (snd M N) = ⊤.prod ⊥

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.

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 AddSubmonoid to itself.

@[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

@[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

theorem MonoidHom.submonoidComap_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.submonoidComap N')

theorem AddMonoidHom.addSubmonoidComap_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.addSubmonoidComap N')

@[deprecated MonoidHom.submonoidComap_surjective (since := "2026-09-09")]

theorem MonoidHom.submonoidComap_surjective_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.submonoidComap N')

Alias of MonoidHom.submonoidComap_surjective.

@[deprecated AddMonoidHom.addSubmonoidComap_surjective (since := "2026-09-09")]

theorem AddMonoidHom.addSubmonoidComap_surjective_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.addSubmonoidComap N')

Alias of AddMonoidHom.addSubmonoidComap_surjective.

theorem MonoidHom.submonoidComap_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (hf : Function.Injective ⇑f) : Function.Injective ⇑(f.submonoidComap N')

theorem AddMonoidHom.addSubmonoidComap_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (hf : Function.Injective ⇑f) : Function.Injective ⇑(f.addSubmonoidComap N')

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.

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 AddSubmonoid to its image. See AddEquiv.AddSubmonoidMap for a variant for AddEquivs.

@[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

@[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

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')

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')

theorem MonoidHom.submonoidMap_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M →* N} (hf : Function.Injective ⇑f) (M' : Submonoid M) : Function.Injective ⇑(f.submonoidMap M')

theorem AddMonoidHom.addSubmonoidMap_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M →+ N} (hf : Function.Injective ⇑f) (M' : AddSubmonoid M) : Function.Injective ⇑(f.addSubmonoidMap M')

theorem Submonoid.surjOn_iff_le_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M →* N} {H : Submonoid M} {K : Submonoid N} : Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ map f H

theorem AddSubmonoid.surjOn_iff_le_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M →+ N} {H : AddSubmonoid M} {K : AddSubmonoid N} : Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ map f H

theorem Submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inl M N) = ⊤.prod ⊥

theorem AddSubmonoid.mrange_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.inl M N) = ⊤.prod ⊥

theorem Submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inr M N) = ⊥.prod ⊤

theorem AddSubmonoid.mrange_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊥.prod ⊤

theorem Submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inl M N) = comap (MonoidHom.snd M N) ⊥

theorem AddSubmonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.inl M N) = comap (AddMonoidHom.snd M N) ⊥

theorem Submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inr M N) = comap (MonoidHom.fst M N) ⊥

theorem AddSubmonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.inr M N) = comap (AddMonoidHom.fst M N) ⊥

@[simp]

theorem Submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.fst M N) = ⊤

@[simp]

theorem AddSubmonoid.mrange_fst {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.fst M N) = ⊤

@[simp]

theorem Submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.snd M N) = ⊤

@[simp]

theorem AddSubmonoid.mrange_snd {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mrange (AddMonoidHom.snd M N) = ⊤

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 = ⊥

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 = ⊥

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 = ⊤

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 = ⊤

@[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) = ⊤

@[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) = ⊤

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

The MonoidHom associated to an inclusion of Submonoids.

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

The AddMonoidHom associated to an inclusion of AddSubmonoids.

@[simp]

theorem Submonoid.coe_inclusion {M : Type u_1} [MulOneClass M] {S T : Submonoid M} (h : S ≤ T) (a : ↥S) : ↑((inclusion h) a) = ↑a

@[simp]

theorem AddSubmonoid.coe_inclusion {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) (a : ↥S) : ↑((inclusion h) a) = ↑a

theorem Submonoid.inclusion_injective {M : Type u_1} [MulOneClass M] {S T : Submonoid M} (h : S ≤ T) : Function.Injective ⇑(inclusion h)

theorem AddSubmonoid.inclusion_injective {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) : Function.Injective ⇑(inclusion h)

@[simp]

theorem Submonoid.inclusion_inj {M : Type u_1} [MulOneClass M] {S T : Submonoid M} (h : S ≤ T) {x y : ↥S} : (inclusion h) x = (inclusion h) y ↔ x = y

@[simp]

theorem AddSubmonoid.inclusion_inj {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) {x y : ↥S} : (inclusion h) x = (inclusion h) y ↔ x = y

@[simp]

theorem Submonoid.subtype_comp_inclusion {M : Type u_1} [MulOneClass M] {S T : Submonoid M} (h : S ≤ T) : T.subtype.comp (inclusion h) = S.subtype

@[simp]

theorem AddSubmonoid.subtype_comp_inclusion {M : Type u_1} [AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T) : T.subtype.comp (inclusion h) = S.subtype

@[simp]

theorem Submonoid.mrange_subtype {M : Type u_1} [MulOneClass M] (s : Submonoid M) : MonoidHom.mrange s.subtype = s

@[simp]

theorem AddSubmonoid.mrange_subtype {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) : AddMonoidHom.mrange s.subtype = s

theorem Submonoid.eq_top_iff' {M : Type u_1} [MulOneClass M] (S : Submonoid M) : S = ⊤ ↔ ∀ (x : M), x ∈ S

theorem AddSubmonoid.eq_top_iff' {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : S = ⊤ ↔ ∀ (x : M), x ∈ S

theorem Submonoid.eq_bot_iff_forall {M : Type u_1} [MulOneClass M] (S : Submonoid M) : S = ⊥ ↔ ∀ x ∈ S, x = 1

theorem AddSubmonoid.eq_bot_iff_forall {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : S = ⊥ ↔ ∀ x ∈ S, x = 0

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

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

theorem Submonoid.nontrivial_iff_exists_ne_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) : Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 1

theorem AddSubmonoid.nontrivial_iff_exists_ne_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Nontrivial ↥S ↔ ∃ x ∈ S, x ≠ 0

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.

theorem AddSubmonoid.bot_or_nontrivial {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : S = ⊥ ∨ Nontrivial ↥S

An AddSubmonoid is either the trivial AddSubmonoid or nontrivial.

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.

theorem AddSubmonoid.bot_or_exists_ne_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ 0

An AddSubmonoid is either the trivial AddSubmonoid or contains a nonzero element.

theorem Submonoid.codisjoint_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [MonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) {H K : Submonoid M} (h : Codisjoint H K) : Codisjoint (map f H) (map f K)

theorem AddSubmonoid.codisjoint_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) {H K : AddSubmonoid M} (h : Codisjoint H K) : Codisjoint (map f H) (map f K)

def Submonoid.pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (I : Set ι) (S : (i : ι) → Submonoid (M i)) : Submonoid ((i : ι) → M i)

A version of Set.pi for Submonoids. Given an index set I and a family of Submonoids s : Π i, Submonoid f i, pi I s is the Submonoid of dependent functions f : Π i, f i such that f i belongs to Pi I s whenever i ∈ I.

def AddSubmonoid.pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (I : Set ι) (S : (i : ι) → AddSubmonoid (M i)) : AddSubmonoid ((i : ι) → M i)

A version of Set.pi for AddSubmonoids. Given an index set I and a family of AddSubmonoids s : Π i, AddSubmonoid f i, pi I s is the AddSubmonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

theorem Submonoid.coe_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (I : Set ι) (S : (i : ι) → Submonoid (M i)) : ↑(pi I S) = I.pi fun (i : ι) => ↑(S i)

theorem AddSubmonoid.coe_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (I : Set ι) (S : (i : ι) → AddSubmonoid (M i)) : ↑(pi I S) = I.pi fun (i : ι) => ↑(S i)

theorem Submonoid.mem_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (I : Set ι) {S : (i : ι) → Submonoid (M i)} {p : (i : ι) → M i} : p ∈ pi I S ↔ ∀ i ∈ I, p i ∈ S i

theorem AddSubmonoid.mem_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (I : Set ι) {S : (i : ι) → AddSubmonoid (M i)} {p : (i : ι) → M i} : p ∈ pi I S ↔ ∀ i ∈ I, p i ∈ S i

theorem Submonoid.pi_top {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (I : Set ι) : (pi I fun (i : ι) => ⊤) = ⊤

theorem AddSubmonoid.pi_top {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (I : Set ι) : (pi I fun (i : ι) => ⊤) = ⊤

theorem Submonoid.pi_empty {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (H : (i : ι) → Submonoid (M i)) : pi ∅ H = ⊤

theorem AddSubmonoid.pi_empty {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (H : (i : ι) → AddSubmonoid (M i)) : pi ∅ H = ⊤

theorem Submonoid.pi_bot {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] : (pi Set.univ fun (i : ι) => ⊥) = ⊥

theorem AddSubmonoid.pi_bot {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] : (pi Set.univ fun (i : ι) => ⊥) = ⊥

theorem Submonoid.le_pi_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] {I : Set ι} {S : (i : ι) → Submonoid (M i)} {J : Submonoid ((i : ι) → M i)} : J ≤ pi I S ↔ ∀ i ∈ I, J ≤ comap (Pi.evalMonoidHom M i) (S i)

theorem AddSubmonoid.le_pi_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] {I : Set ι} {S : (i : ι) → AddSubmonoid (M i)} {J : AddSubmonoid ((i : ι) → M i)} : J ≤ pi I S ↔ ∀ i ∈ I, J ≤ comap (Pi.evalAddMonoidHom M i) (S i)

@[simp]

theorem Submonoid.mulSingle_mem_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] [DecidableEq ι] {I : Set ι} {S : (i : ι) → Submonoid (M i)} (i : ι) (x : M i) : Pi.mulSingle i x ∈ pi I S ↔ i ∈ I → x ∈ S i

@[simp]

theorem AddSubmonoid.single_mem_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] [DecidableEq ι] {I : Set ι} {S : (i : ι) → AddSubmonoid (M i)} (i : ι) (x : M i) : Pi.single i x ∈ pi I S ↔ i ∈ I → x ∈ S i

theorem Submonoid.pi_eq_bot_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (S : (i : ι) → Submonoid (M i)) : pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

theorem AddSubmonoid.pi_eq_bot_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (S : (i : ι) → AddSubmonoid (M i)) : pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

theorem Submonoid.le_comap_mulSingle_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] [DecidableEq ι] (S : (i : ι) → Submonoid (M i)) {I : Set ι} {i : ι} : S i ≤ comap (MonoidHom.mulSingle M i) (pi I S)

theorem AddSubmonoid.le_comap_single_pi {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] [DecidableEq ι] (S : (i : ι) → AddSubmonoid (M i)) {I : Set ι} {i : ι} : S i ≤ comap (AddMonoidHom.single M i) (pi I S)

theorem Submonoid.iSup_map_mulSingle_le {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] [DecidableEq ι] {I : Set ι} {S : (i : ι) → Submonoid (M i)} : ⨆ (i : ι), map (MonoidHom.mulSingle M i) (S i) ≤ pi I S

theorem AddSubmonoid.iSup_map_single_le {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] [DecidableEq ι] {I : Set ι} {S : (i : ι) → AddSubmonoid (M i)} : ⨆ (i : ι), map (AddMonoidHom.single M i) (S i) ≤ pi I S

def MonoidHom.restrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Submonoid M} {N' : Submonoid N} {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N') : ↥M' →* ↥N'

Restrict the domain and codomain of a MonoidHom.

def AddMonoidHom.restrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : AddSubmonoid M} {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N') : ↥M' →+ ↥N'

Restrict the domain and codomain of an AddMonoidHom.

theorem MonoidHom.restrict_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Submonoid M} {N' : Submonoid N} {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N') (hf' : Function.Injective ⇑f) : Function.Injective ⇑(restrict h)

theorem AddMonoidHom.restrict_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : AddSubmonoid M} {N' : AddSubmonoid N} {f : M →+ N} (h : Set.MapsTo ⇑f ↑M' ↑N') (hf' : Function.Injective ⇑f) : Function.Injective ⇑(restrict h)

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

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

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

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

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.mrangeRestrict.

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.mrangeRestrict.

@[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)) : (ofLeftInverse' f h).symm a✝ = g ↑a✝

@[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) : (ofLeftInverse' f h) a = f.mrangeRestrict a

@[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)) : (ofLeftInverse' f h).symm a✝ = g ↑a✝

@[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) : (ofLeftInverse' f h) a = f.mrangeRestrict a

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.

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.

@[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

@[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

@[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, ⋯⟩

@[simp]

theorem AddEquiv.addSubmonoidMap_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, ⋯⟩

@[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

@[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

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

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

noncomputable def Submonoid.unitsTypeEquivIsUnitSubmonoid {M : Type u_4} [Monoid M] : Mˣ ≃* ↥(IsUnit.submonoid M)

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

noncomputable def AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid {M : Type u_4} [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.

@[simp]

theorem Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_4} [Monoid M] (x : ↥(IsUnit.submonoid M)) : ↑(unitsTypeEquivIsUnitSubmonoid.symm x) = ↑x

@[simp]

theorem AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_4} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑(addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑x

@[simp]

theorem AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_4} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑(-addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑(-Classical.choose ⋯)

@[simp]

theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe {M : Type u_4} [AddMonoid M] (x : AddUnits M) : ↑(addUnitsTypeEquivIsAddUnitAddSubmonoid x) = ↑x

@[simp]

theorem Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe {M : Type u_4} [Monoid M] (x : Mˣ) : ↑(unitsTypeEquivIsUnitSubmonoid x) = ↑x

@[simp]

theorem Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply {M : Type u_4} [Monoid M] (x : ↥(IsUnit.submonoid M)) : ↑(unitsTypeEquivIsUnitSubmonoid.symm x)⁻¹ = ↑(Classical.choose ⋯)⁻¹

theorem Submonoid.map_comap_eq {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) : map f (comap f S) = S ⊓ MonoidHom.mrange f

theorem AddSubmonoid.map_comap_eq {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) : map f (comap f S) = S ⊓ AddMonoidHom.mrange f

theorem Submonoid.map_comap_eq_self {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} (h : S ≤ MonoidHom.mrange f) : map f (comap f S) = S

theorem AddSubmonoid.map_comap_eq_self {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} (h : S ≤ AddMonoidHom.mrange f) : map f (comap f S) = S

theorem Submonoid.map_comap_eq_self_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} (h : Function.Surjective ⇑f) {S : Submonoid N} : map f (comap f S) = S

theorem AddSubmonoid.map_comap_eq_self_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} (h : Function.Surjective ⇑f) {S : AddSubmonoid N} : map f (comap f S) = S