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

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.

@[simp]

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

@[simp]

theorem Submonoid.coe_toAddSubmonoid_apply {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ↑(toAddSubmonoid S) = ⇑Additive.toMul ⁻¹' ↑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.

Equations

• AddSubmonoid.toSubmonoid' = Submonoid.toAddSubmonoid.symm

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 (⇑Multiplicative.ofAdd ⁻¹' 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.

Equations

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

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

Equations

• Submonoid.toAddSubmonoid' = AddSubmonoid.toSubmonoid.symm

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 (⇑Additive.ofMul ⁻¹' 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 monoid homomorphism is a submonoid.

Equations

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

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' := ⋯ }

@[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 monoid homomorphism is a submonoid.

Equations

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

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' := ⋯ }

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

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

Equations

• Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

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.

Equations

• AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

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.

Equations

• Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

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.

Equations

• AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

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.

Equations

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

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' := ⋯ }

@[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_symm_apply_coe {M : Type u_5} [MulOneClass 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_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.

Equations

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

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 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' := ⋯ }

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

Equations

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

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' := ⋯ }

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.

Equations

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

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' := ⋯ }

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.toMonoidHom K = comap f.symm.toMonoidHom 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.toAddMonoidHom K = comap f.symm.toAddMonoidHom 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)

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

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

@[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} [Monoid 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} [AddMonoid 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

@[deprecated MonoidHom.mrange_eq_top (since := "2024-11-11")]

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

Alias of MonoidHom.mrange_eq_top.

@[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 monoid hom 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 AddMonoid hom is the whole of the codomain.

@[deprecated MonoidHom.mrange_eq_top_of_surjective (since := "2024-11-11")]

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

Alias of MonoidHom.mrange_eq_top_of_surjective.

---

The range of a surjective monoid hom 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 monoid hom 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 AddMonoid hom 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.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)

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)

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

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

@[simp]

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

@[simp]

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

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' := ⋯ }

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' := ⋯ }

@[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.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 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 monoid hom to its range interpreted as a submonoid.

Equations

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

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

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

Equations

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

@[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 monoid hom is the submonoid of elements x : G such that f x = 1

Equations

• MonoidHom.mker f = Submonoid.comap f ⊥

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 ⊥

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

Equations

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

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

Equations

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

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.restrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) : mker (f.restrict S) = Submonoid.comap S.subtype (mker f)

@[simp]

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

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.

Equations

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

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' := ⋯ }

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

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' := ⋯ }

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' := ⋯ }

@[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 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 monoid hom associated to an inclusion of submonoids.

Equations

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

def AddSubmonoid.inclusion {M : Type u_1} [AddZeroClass M] {S 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 ⋯

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

@[deprecated Submonoid.mrange_subtype (since := "2024-11-25")]

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

Alias of Submonoid.mrange_subtype.

@[deprecated AddSubmonoid.mrange_subtype (since := "2024-11-25")]

theorem AddSubmonoid.range_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 additive submonoid is either the trivial additive submonoid 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 additive submonoid is either the trivial additive submonoid or contains a nonzero element.

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.

Equations

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

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.

Equations

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

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' := ⋯ }

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' := ⋯ }

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

Equations

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

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' := ⋯ }

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

@[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_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' := ⋯ }

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.addSubmonoid_closure_one : AddSubmonoid.closure {1} = ⊤

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