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

@[simp]

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

@[simp]

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

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.

@[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) : Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S)

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

@[simp]

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

@[simp]

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

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.

@[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) : AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

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

comap and map

theorem AddSubmonoid.comap.proof_2 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) : f 0 ∈ S

theorem AddSubmonoid.comap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) : ∀ {a b : M}, a ∈ ⇑f ⁻¹' ↑S → b ∈ ⇑f ⁻¹' ↑S → f (a + b) ∈ S

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

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

@[simp]

theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F) : ↑(AddSubmonoid.comap f S) = ⇑f ⁻¹' ↑S

@[simp]

theorem Submonoid.coe_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F) : ↑(Submonoid.comap f S) = ⇑f ⁻¹' ↑S

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem AddSubmonoid.map.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) : ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a + b ∈ ⇑f '' ↑S

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

theorem AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) : ∃ a ∈ ↑S, f a = 0

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

@[simp]

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

@[simp]

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

@[simp]

theorem AddSubmonoid.mem_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N} : y ∈ AddSubmonoid.map f S ↔ ∃ x ∈ S, f x = y

@[simp]

theorem Submonoid.mem_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N} : y ∈ Submonoid.map f S ↔ ∃ x ∈ S, f x = y

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

abbrev AddSubmonoid.map_id.match_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ∀ (x : M) (motive : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S → Prop) (x_1 : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S), (∀ (h : x ∈ ↑S), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (S : AddSubmonoid M) (x : M) : x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S

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

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

Equations

• AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

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

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

Equations

• Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) (S : AddSubmonoid N) (x : N) (h : x ∈ S) : x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S)

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

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

Equations

• AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} {F : Type u_3} [FunLike F M N] {f : F} (x : N) (motive : (∃ (a : M), f a = x) → Prop) : ∀ (x_1 : ∃ (a : M), f a = x), (∀ (y : M) (hy : f y = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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

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

Equations

• Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance ZeroMemClass.zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : Zero ↥S'

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

• ZeroMemClass.zero S' = { zero := ⟨0, ⋯⟩ }

instance OneMemClass.one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : One ↥S'

A submonoid of a monoid inherits a 1.

Equations

• OneMemClass.one S' = { one := ⟨1, ⋯⟩ }

@[simp]

theorem ZeroMemClass.coe_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : ↑0 = 0

@[simp]

theorem OneMemClass.coe_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : ↑1 = 1

@[simp]

theorem ZeroMemClass.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : ↥S'} : ↑x = 0 ↔ x = 0

@[simp]

theorem OneMemClass.coe_eq_one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] {S' : A} {x : ↥S'} : ↑x = 1 ↔ x = 1

theorem ZeroMemClass.zero_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : 0 = ⟨0, ⋯⟩

theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : 1 = ⟨1, ⋯⟩

instance AddSubmonoidClass.nSMul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ ↥S

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

Equations

• AddSubmonoidClass.nSMul S = { smul := fun (n : ℕ) (a : ↥S) => ⟨n • ↑a, ⋯⟩ }

instance SubmonoidClass.nPow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow ↥S ℕ

A submonoid of a monoid inherits a power operator.

Equations

• SubmonoidClass.nPow S = { pow := fun (a : ↥S) (n : ℕ) => ⟨↑a ^ n, ⋯⟩ }

@[simp]

theorem AddSubmonoidClass.coe_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : ↥S) (n : ℕ) : ↑(n • x) = n • ↑x

@[simp]

theorem SubmonoidClass.coe_pow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] {S : A} (x : ↥S) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem AddSubmonoidClass.mk_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩

@[simp]

theorem SubmonoidClass.mk_pow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩

theorem AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

@[instance 75]

instance AddSubmonoidClass.toAddZeroClass {M : Type u_5} [AddZeroClass M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddZeroClass ↥S

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations

• AddSubmonoidClass.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val ⋯ ⋯ ⋯

@[instance 75]

instance SubmonoidClass.toMulOneClass {M : Type u_5} [MulOneClass M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) : MulOneClass ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

• SubmonoidClass.toMulOneClass S = Function.Injective.mulOneClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddMonoid.proof_1 {M : Type u_2} [AddMonoid M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

theorem AddSubmonoidClass.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

@[instance 75]

instance AddSubmonoidClass.toAddMonoid {M : Type u_5} [AddMonoid M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddMonoid ↥S

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

• AddSubmonoidClass.toAddMonoid S = Function.Injective.addMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoidClass.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

@[instance 75]

instance SubmonoidClass.toMonoid {M : Type u_5} [Monoid M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) : Monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

• SubmonoidClass.toMonoid S = Function.Injective.monoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toAddCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

@[instance 75]

instance AddSubmonoidClass.toAddCommMonoid {M : Type u_6} [AddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddCommMonoid ↥S

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

• AddSubmonoidClass.toAddCommMonoid S = Function.Injective.addCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddCommMonoid.proof_1 {M : Type u_2} [AddCommMonoid M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

@[instance 75]

instance SubmonoidClass.toCommMonoid {M : Type u_6} [CommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : CommMonoid ↥S

A submonoid of a CommMonoid is a CommMonoid.

Equations

• SubmonoidClass.toCommMonoid S = Function.Injective.commMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

def AddSubmonoidClass.subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ↥S' →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations

• AddSubmonoidClass.subtype S' = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

theorem AddSubmonoidClass.subtype.proof_1 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ↑0 = ↑0

theorem AddSubmonoidClass.subtype.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] (S' : A) : ∀ (x x_1 : ↥S'), ↑x + ↑x_1 = ↑x + ↑x_1

def SubmonoidClass.subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [SetLike A M] [hA : SubmonoidClass A M] (S' : A) : ↥S' →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

• SubmonoidClass.subtype S' = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubmonoidClass.coe_subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ⇑(AddSubmonoidClass.subtype S') = Subtype.val

@[simp]

theorem SubmonoidClass.coe_subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [SetLike A M] [hA : SubmonoidClass A M] (S' : A) : ⇑(SubmonoidClass.subtype S') = Subtype.val

theorem AddSubmonoid.add.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (a : ↥S) (b : ↥S) : ↑a + ↑b ∈ S

instance AddSubmonoid.add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Add ↥S

An AddSubmonoid of an AddMonoid inherits an addition.

Equations

• S.add = { add := fun (a b : ↥S) => ⟨↑a + ↑b, ⋯⟩ }

instance Submonoid.mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) : Mul ↥S

A submonoid of a monoid inherits a multiplication.

Equations

• S.mul = { mul := fun (a b : ↥S) => ⟨↑a * ↑b, ⋯⟩ }

instance AddSubmonoid.zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Zero ↥S

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

• S.zero = { zero := ⟨0, ⋯⟩ }

instance Submonoid.one {M : Type u_1} [MulOneClass M] (S : Submonoid M) : One ↥S

A submonoid of a monoid inherits a 1.

Equations

• S.one = { one := ⟨1, ⋯⟩ }

@[simp]

theorem AddSubmonoid.coe_add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : ↥S) (y : ↥S) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Submonoid.coe_mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : ↥S) (y : ↥S) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem AddSubmonoid.coe_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = 0

@[simp]

theorem Submonoid.coe_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ↑1 = 1

@[simp]

theorem AddSubmonoid.mk_eq_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) {a : M} {ha : a ∈ S} : ⟨a, ha⟩ = 0 ↔ a = 0

@[simp]

theorem Submonoid.mk_eq_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) {a : M} {ha : a ∈ S} : ⟨a, ha⟩ = 1 ↔ a = 1

@[simp]

theorem AddSubmonoid.mk_add_mk {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩

@[simp]

theorem Submonoid.mk_mul_mk {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

theorem AddSubmonoid.add_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : ↥S) (y : ↥S) : x + y = ⟨↑x + ↑y, ⋯⟩

theorem Submonoid.mul_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : ↥S) (y : ↥S) : x * y = ⟨↑x * ↑y, ⋯⟩

theorem AddSubmonoid.zero_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : 0 = ⟨0, ⋯⟩

theorem Submonoid.one_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) : 1 = ⟨1, ⋯⟩

theorem AddSubmonoid.toAddZeroClass.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toAddZeroClass.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = ↑0

instance AddSubmonoid.toAddZeroClass {M : Type u_5} [AddZeroClass M] (S : AddSubmonoid M) : AddZeroClass ↥S

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations

• S.toAddZeroClass = Function.Injective.addZeroClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

instance Submonoid.toMulOneClass {M : Type u_5} [MulOneClass M] (S : Submonoid M) : MulOneClass ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

• S.toMulOneClass = Function.Injective.mulOneClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoid.nsmul_mem {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : n • x ∈ S

theorem Submonoid.pow_mem {M : Type u_5} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S

instance AddSubmonoid.toAddMonoid {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) : AddMonoid ↥S

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

• S.toAddMonoid = Function.Injective.addMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toAddMonoid.proof_1 {M : Type u_1} [AddMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toAddMonoid.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

instance Submonoid.toMonoid {M : Type u_5} [Monoid M] (S : Submonoid M) : Monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

• S.toMonoid = Function.Injective.monoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddCommMonoid.proof_1 {M : Type u_1} [AddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toAddCommMonoid.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toAddCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

instance AddSubmonoid.toAddCommMonoid {M : Type u_5} [AddCommMonoid M] (S : AddSubmonoid M) : AddCommMonoid ↥S

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

• S.toAddCommMonoid = Function.Injective.addCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

instance Submonoid.toCommMonoid {M : Type u_5} [CommMonoid M] (S : Submonoid M) : CommMonoid ↥S

A submonoid of a CommMonoid is a CommMonoid.

Equations

• S.toCommMonoid = Function.Injective.commMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

def AddSubmonoid.subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↥S →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations

• S.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑x + ↑x_1 = ↑x + ↑x_1

def Submonoid.subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ↥S →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

• S.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ⇑S.subtype = Subtype.val

@[simp]

theorem Submonoid.coe_subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ⇑S.subtype = Subtype.val

theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] : ∀ (x : M), (fun (x : ↥⊤) => ↑x) ((fun (x : M) => ⟨x, ⋯⟩) x) = (fun (x : ↥⊤) => ↑x) ((fun (x : M) => ⟨x, ⋯⟩) x)

def AddSubmonoid.topEquiv {M : Type u_1} [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' := ⋯ }

theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [AddZeroClass M] : ∀ (x x_1 : ↥⊤), { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1)

theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [AddZeroClass M] (x : ↥⊤) : ⟨↑x, ⋯⟩ = x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Submonoid.topEquiv {M : Type u_1} [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' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

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

theorem AddSubmonoid.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ⇑f) : ∀ (x x_1 : ↥S), (Equiv.Set.image (⇑f) (↑S) hf).toFun (x + x_1) = (Equiv.Set.image (⇑f) (↑S) hf).toFun x + (Equiv.Set.image (⇑f) (↑S) hf).toFun x_1

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : 0.1 ∈ ↑s ∧ 0.2 ∈ ↑t

theorem AddSubmonoid.prod.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : ∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a + b).1 ∈ ↑s ∧ (a + b).2 ∈ ↑t

def AddSubmonoid.prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (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' := ⋯ }

def Submonoid.prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (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' := ⋯ }

theorem AddSubmonoid.coe_prod {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.coe_prod {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.mem_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {p : M × N} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

theorem Submonoid.mem_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {p : M × N} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : ∀ (x x_1 : ↥(s.prod t)), (Equiv.Set.prod ↑s ↑t).toFun (x + x_1) = (Equiv.Set.prod ↑s ↑t).toFun (x + x_1)

def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (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 = let __src := Equiv.Set.prod ↑s ↑t; { toEquiv := __src, map_add' := ⋯ }

def Submonoid.prodEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (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 = let __src := Equiv.Set.prod ↑s ↑t; { toEquiv := __src, map_mul' := ⋯ }

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

abbrev AddSubmonoid.map_inl.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p ∈ s.prod ⊥ → Prop) : ∀ (x : p ∈ s.prod ⊥), (∀ (hps : p.1 ∈ ↑s) (hp1 : p.2 ∈ ↑⊥), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubmonoid.map_inl.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p ∈ AddSubmonoid.map (AddMonoidHom.inl M N) s → Prop) : ∀ (x : p ∈ AddSubmonoid.map (AddMonoidHom.inl M N) s), (∀ (w : M) (hx : w ∈ ↑s) (hp : (AddMonoidHom.inl M N) w = p), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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

abbrev AddSubmonoid.map_inr.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p ∈ AddSubmonoid.map (AddMonoidHom.inr M N) s → Prop) : ∀ (x : p ∈ AddSubmonoid.map (AddMonoidHom.inr M N) s), (∀ (w : N) (hx : w ∈ ↑s) (hp : (AddMonoidHom.inr M N) w = p), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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

abbrev AddSubmonoid.map_inr.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p ∈ ⊥.prod s → Prop) : ∀ (x : p ∈ ⊥.prod s), (∀ (hp1 : p.1 ∈ ↑⊥) (hps : p.2 ∈ ↑s), motive ⋯) → motive x

Equations

• ⋯ = ⋯

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

@[simp]

theorem AddSubmonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : s.prod ⊥ ⊔ ⊥.prod t = s.prod t

@[simp]

theorem Submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (s : Submonoid M) (t : Submonoid N) : s.prod ⊥ ⊔ ⊥.prod t = s.prod t

theorem AddSubmonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {f : M ≃+ N} {K : AddSubmonoid M} {x : N} : x ∈ AddSubmonoid.map f.toAddMonoidHom K ↔ f.symm x ∈ K

theorem Submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {f : M ≃* N} {K : Submonoid M} {x : N} : x ∈ Submonoid.map f.toMonoidHom K ↔ f.symm x ∈ K

theorem AddSubmonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) (K : AddSubmonoid M) : AddSubmonoid.map f.toAddMonoidHom K = AddSubmonoid.comap f.symm.toAddMonoidHom K

theorem Submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M ≃* N) (K : Submonoid M) : Submonoid.map f.toMonoidHom K = Submonoid.comap f.symm.toMonoidHom K

theorem AddSubmonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : N ≃+ M) (K : AddSubmonoid M) : AddSubmonoid.comap f K = AddSubmonoid.map f.symm K

theorem Submonoid.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : N ≃* M) (K : Submonoid M) : Submonoid.comap f K = Submonoid.map f.symm K

@[simp]

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

@[simp]

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

theorem AddSubmonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} : u ≤ s.prod t ↔ AddSubmonoid.map (AddMonoidHom.fst M N) u ≤ s ∧ AddSubmonoid.map (AddMonoidHom.snd M N) u ≤ t

theorem Submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : u ≤ s.prod t ↔ Submonoid.map (MonoidHom.fst M N) u ≤ s ∧ Submonoid.map (MonoidHom.snd M N) u ≤ t

theorem AddSubmonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} : s.prod t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u

theorem Submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : s.prod t ≤ u ↔ Submonoid.map (MonoidHom.inl M N) s ≤ u ∧ Submonoid.map (MonoidHom.inr M N) t ≤ u

theorem AddMonoidHom.mrange.proof_1 {M : Type u_2} {N : Type u_1} {F : Type u_3} [FunLike F M N] (f : F) : Set.range ⇑f = ⇑f '' Set.univ

def AddMonoidHom.mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [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) ⋯

def MonoidHom.mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [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) ⋯

@[simp]

theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : ↑(AddMonoidHom.mrange f) = Set.range ⇑f

@[simp]

theorem MonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : ↑(MonoidHom.mrange f) = Set.range ⇑f

@[simp]

theorem AddMonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {y : N} : y ∈ AddMonoidHom.mrange f ↔ ∃ (x : M), f x = y

@[simp]

theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {y : N} : y ∈ MonoidHom.mrange f ↔ ∃ (x : M), f x = y

theorem AddMonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : AddMonoidHom.mrange f = AddSubmonoid.map f ⊤

theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : MonoidHom.mrange f = Submonoid.map f ⊤

@[simp]

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

@[simp]

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

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

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

theorem AddMonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} : AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f

theorem MonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] {f : F} : MonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f

@[simp]

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

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

@[simp]

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

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

theorem AddMonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [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.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [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.map_mclosure {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [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.

theorem MonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [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.

@[simp]

theorem AddMonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid.closure (Set.range ⇑f) = AddMonoidHom.mrange f

@[simp]

theorem MonoidHom.mclosure_range {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : Submonoid.closure (Set.range ⇑f) = MonoidHom.mrange f

def AddMonoidHom.restrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [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)

def MonoidHom.restrict {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [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)

@[simp]

theorem AddMonoidHom.restrict_apply {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [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_apply {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [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_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) : AddMonoidHom.mrange (f.restrict S) = AddSubmonoid.map f S

@[simp]

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

def AddMonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_6} [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' := ⋯ }

theorem AddMonoidHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) : (fun (n : M) => ⟨f n, ⋯⟩) 0 = 0

theorem AddMonoidHom.codRestrict.proof_2 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s) (x : M) (y : M) : { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_zero' := ⋯ }.toFun x + { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_zero' := ⋯ }.toFun y

@[simp]

theorem MonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [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_6} [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, ⋯⟩

def MonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [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.mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} [AddZeroClass N] (f : M →+ N) : M →+ ↥(AddMonoidHom.mrange f)

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

Equations

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

theorem AddMonoidHom.mrangeRestrict.proof_1 {M : Type u_1} [AddZeroClass M] {N : Type u_2} [AddZeroClass N] (f : M →+ N) (x : M) : ∃ (y : M), f y = f x

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

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

Equations

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

@[simp]

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

@[simp]

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

abbrev AddMonoidHom.mrangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (motive : ↥(AddMonoidHom.mrange f) → Prop) : ∀ (x : ↥(AddMonoidHom.mrange f)), (∀ (x : M), motive ⟨f x, ⋯⟩) → motive x

Equations

• ⋯ = ⋯

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

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

def AddMonoidHom.mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [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 ⊥

def MonoidHom.mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [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 ⊥

theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) {x : M} : x ∈ AddMonoidHom.mker f ↔ f x = 0

theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) {x : M} : x ∈ MonoidHom.mker f ↔ f x = 1

theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : ↑(AddMonoidHom.mker f) = ⇑f ⁻¹' {0}

theorem MonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : ↑(MonoidHom.mker f) = ⇑f ⁻¹' {1}

instance AddMonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] [DecidableEq N] (f : F) : DecidablePred fun (x : M) => x ∈ AddMonoidHom.mker f

Equations

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

instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] [DecidableEq N] (f : F) : DecidablePred fun (x : M) => x ∈ MonoidHom.mker f

Equations

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

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

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

@[simp]

theorem AddMonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid.comap f ⊥ = AddMonoidHom.mker f

@[simp]

theorem MonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : Submonoid.comap f ⊥ = MonoidHom.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) : AddMonoidHom.mker (f.restrict S) = AddSubmonoid.comap S.subtype (AddMonoidHom.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) : MonoidHom.mker (f.restrict S) = Submonoid.comap S.subtype (MonoidHom.mker f)

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

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

@[simp]

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

@[simp]

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

theorem AddMonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [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.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [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.mker_prod_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') : AddMonoidHom.mker (f.prodMap g) = (AddMonoidHom.mker f).prod (AddMonoidHom.mker g)

theorem MonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') : MonoidHom.mker (f.prodMap g) = (MonoidHom.mker f).prod (MonoidHom.mker g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AddMonoidHom.addSubmonoidComap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : ↥(AddSubmonoid.comap f N')) (y : ↥(AddSubmonoid.comap f N')) : { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun x + { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun y

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

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

theorem AddMonoidHom.addSubmonoidComap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) : (fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩) 0 = 0

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

theorem AddMonoidHom.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : ↥M') : ∃ a ∈ ↑M', f a = f ↑x

theorem AddMonoidHom.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : ↥M') (y : ↥M') : { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun x + { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_zero' := ⋯ }.toFun y

theorem AddMonoidHom.addSubmonoidMap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) : (fun (x : ↥M') => ⟨f ↑x, ⋯⟩) 0 = 0

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

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

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

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_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 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_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inl 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_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.inr 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) = AddSubmonoid.comap (AddMonoidHom.snd M N) ⊥

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

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

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

@[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_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mrange (MonoidHom.fst 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) = ⊤

@[simp]

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

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

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

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

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

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

The AddMonoid hom associated to an inclusion of submonoids.

Equations

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

theorem AddSubmonoid.inclusion.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S ≤ T) (x : ↥S) : S.subtype x ∈ T

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

The monoid hom associated to an inclusion of submonoids.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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 AddEquiv.addSubmonoidCongr.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) : ↑S = ↑T

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

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

Equations

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

theorem AddEquiv.addSubmonoidCongr.proof_2 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) : ∀ (x x_1 : ↥S), (Equiv.setCongr ⋯).toFun (x + x_1) = (Equiv.setCongr ⋯).toFun (x + x_1)

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

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

Equations

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

theorem AddEquiv.ofLeftInverse'.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) (x : ↥(AddMonoidHom.mrange f)) : f.mrangeRestrict ((g ∘ ⇑(AddMonoidHom.mrange f).subtype) x) = x

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 = let __src := f.mrangeRestrict; { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(AddMonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }

abbrev AddEquiv.ofLeftInverse'.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : ↥(AddMonoidHom.mrange f)) (motive : (∃ (x_1 : M), f x_1 = ↑x) → Prop) : ∀ (x_1 : ∃ (x_1 : M), f x_1 = ↑x), (∀ (x' : M) (hx' : f x' = ↑x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddEquiv.ofLeftInverse'.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : M) (y : M) : (↑f.mrangeRestrict).toFun (x + y) = (↑f.mrangeRestrict).toFun x + (↑f.mrangeRestrict).toFun y

@[simp]

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

@[simp]

theorem AddEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) : ∀ (a : ↥(AddMonoidHom.mrange f)), (AddEquiv.ofLeftInverse' f h).symm a = g ↑a

@[simp]

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

@[simp]

theorem MulEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ⇑f) : ∀ (a : ↥(MonoidHom.mrange f)), (MulEquiv.ofLeftInverse' f h).symm a = g ↑a

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 = let __src := f.mrangeRestrict; { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(MonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

theorem AddEquiv.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHomClass (M ≃+ N) M N

theorem AddEquiv.addSubmonoidMap.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ((↑e).image ↑S).toFun (x + x_1) = ((↑e).image ↑S).toFun x + ((↑e).image ↑S).toFun x_1

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 = let __src := (↑e).image ↑S; { toEquiv := __src, map_add' := ⋯ }

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 = let __src := (↑e).image ↑S; { toEquiv := __src, map_mul' := ⋯ }

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

@[simp]

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

Actions by Submonoids

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

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem AddSubmonoid.vadd_def {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : ↥S) (a : α) : g +ᵥ a = ↑g +ᵥ a

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

@[simp]

theorem AddSubmonoid.mk_vadd {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ +ᵥ a = g +ᵥ a

@[simp]

theorem Submonoid.mk_smul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ • a = g • a

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

Equations

• ⋯ = ⋯

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

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

Equations

• S.addAction = AddAction.compHom α S.subtype

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

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

Equations

• S.mulAction = MulAction.compHom α S.subtype

theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.proof_3 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : (fun (x : AddUnits M) => ⟨↑x, ⋯⟩) ((fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯) x) = x

theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.proof_2 {M : Type u_1} [AddMonoid M] (x : AddUnits M) : IsAddUnit.addUnit ⋯ = x

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

theorem AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (x : AddUnits M) (y : AddUnits M) : { toFun := fun (x : AddUnits M) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := fun (x : AddUnits M) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (x : AddUnits M) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

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 AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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