Operations on `Submonoid`s #

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

Main definitions #

Conversion between multiplicative and additive definitions #

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

(Commutative) monoid structure on a submonoid #

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

Group actions by submonoids #

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

Operations on submonoids #

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

Monoid homomorphisms between submonoid #

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

Operations on `MonoidHom`s #

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

Tags #

submonoid, range, product, map, comap

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

source

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

Submonoid M ≃o AddSubmonoid (Additive M)

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[reducible, inline]

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

AddSubmonoid (Additive M) ≃o Submonoid M

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

Equations

AddSubmonoid.toSubmonoid' = Submonoid.toAddSubmonoid.symm

Instances For

source

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

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

source

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

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

source

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

AddSubmonoid A ≃o Submonoid (Multiplicative A)

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[reducible, inline]

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

Submonoid (Multiplicative A) ≃o AddSubmonoid A

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

Equations

Submonoid.toAddSubmonoid' = AddSubmonoid.toSubmonoid.symm

Instances For

source

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

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

source

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

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

`comap` and `map` #

source

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

Submonoid M

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

Equations

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

Instances For

source

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

AddSubmonoid M

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

x ∈ comap f S ↔ f x ∈ S

source

@[simp]

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

x ∈ comap f S ↔ f x ∈ S

source

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

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

source

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

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

source

@[simp]

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

comap (MonoidHom.id P) S = S

source

@[simp]

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

comap (AddMonoidHom.id P) S = S

source

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

Submonoid N

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

Equations

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

Instances For

source

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

AddSubmonoid N

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

map (↑f) S = map f S

source

@[simp]

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

map (↑f) S = map f S

source

@[simp]

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

map (↑f) S = map f S

source

@[simp]

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

map (↑f) S = map f S

source

@[simp]

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

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

source

@[simp]

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

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

source

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

f x ∈ map f S

source

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

f x ∈ map f S

source

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

f ↑x ∈ map f S

source

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

f ↑x ∈ map f S

source

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

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

source

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

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

source

@[simp]

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

f x ∈ map f S ↔ x ∈ S

source

@[simp]

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

f x ∈ map f S ↔ x ∈ S

source

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

map f S ≤ T ↔ S ≤ comap f T

source

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

map f S ≤ T ↔ S ≤ comap f T

source

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

GaloisConnection (map f) (comap f)

source

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

GaloisConnection (map f) (comap f)

source

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

S ≤ comap f T → map f S ≤ T

source

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

S ≤ comap f T → map f S ≤ T

source

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

map f S ≤ T → S ≤ comap f T

source

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

map f S ≤ T → S ≤ comap f T

source

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

S ≤ comap f (map f S)

source

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

S ≤ comap f (map f S)

source

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

map f (comap f S) ≤ S

source

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

map f (comap f S) ≤ S

source

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

Monotone (map f)

source

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

Monotone (map f)

source

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

Monotone (comap f)

source

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

Monotone (comap f)

source

@[simp]

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

map f (comap f (map f S)) = map f S

source

@[simp]

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

map f (comap f (map f S)) = map f S

source

@[simp]

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

comap f (map f (comap f S)) = comap f S

source

@[simp]

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

comap f (map f (comap f S)) = comap f S

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

map f ⊥ = ⊥

source

@[simp]

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

map f ⊥ = ⊥

source

@[simp]

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

comap f ⊤ = ⊤

source

@[simp]

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

comap f ⊤ = ⊤

source

@[simp]

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

map (MonoidHom.id M) S = S

source

@[simp]

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

map (AddMonoidHom.id M) S = S

source

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

GaloisCoinsertion (map f) (comap f)

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

Equations

Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

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

GaloisCoinsertion (map f) (comap f)

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

Equations

AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

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

comap f (map f S) = S

source

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

comap f (map f S) = S

source

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

Function.Surjective (comap f)

source

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

Function.Surjective (comap f)

source

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

Function.Injective (map f)

source

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

Function.Injective (map f)

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

map f S ≤ map f T ↔ S ≤ T

source

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

map f S ≤ map f T ↔ S ≤ T

source

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

StrictMono (map f)

source

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

StrictMono (map f)

source

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

GaloisInsertion (map f) (comap f)

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

Equations

Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

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

GaloisInsertion (map f) (comap f)

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

Equations

AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

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

map f (comap f S) = S

source

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

map f (comap f S) = S

source

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

Function.Surjective (map f)

source

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

Function.Surjective (map f)

source

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

Function.Injective (comap f)

source

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

Function.Injective (comap f)

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

comap f S ≤ comap f T ↔ S ≤ T

source

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

comap f S ≤ comap f T ↔ S ≤ T

source

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

StrictMono (comap f)

source

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

StrictMono (comap f)

source

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

↥⊤ ≃* M

The top submonoid is isomorphic to the monoid.

Equations

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

Instances For

source

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

↥⊤ ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

Equations

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

Instances For

source

@[simp]

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

topEquiv x = ↑x

source

@[simp]

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

↑(topEquiv.symm x) = x

source

@[simp]

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

topEquiv x = ↑x

source

@[simp]

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

↑(topEquiv.symm x) = x

source

@[simp]

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

↑topEquiv = ⊤.subtype

source

@[simp]

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

↑topEquiv = ⊤.subtype

source

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

↥S ≃* ↥(map f S)

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

Equations

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

Instances For

source

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

↥S ≃+ ↥(map f S)

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

Submonoid (M × N)

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

Equations

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

Instances For

source

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

AddSubmonoid (M × N)

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

Equations

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

Instances For

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

⊤.prod ⊤ = ⊤

source

@[simp]

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

⊤.prod ⊤ = ⊤

source

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

⊥.prod ⊥ = ⊥

source

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

⊥.prod ⊥ = ⊥

source

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

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

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

Equations

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

Instances For

source

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

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

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

Equations

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

Instances For

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

map f K = comap f.symm K

source

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

map f K = comap f.symm K

source

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

comap f K = map f.symm K

source

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

comap f K = map f.symm K

source

@[simp]

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

map f ⊤ = ⊤

source

@[simp]

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

map f ⊤ = ⊤

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

closure (s ×ˢ {1}) = (closure s).prod ⊥

source

@[simp]

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

closure (s ×ˢ {0}) = (closure s).prod ⊥

source

@[simp]

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

closure ({1} ×ˢ t) = ⊥.prod (closure t)

source

@[simp]

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

closure ({0} ×ˢ t) = ⊥.prod (closure t)

source

def MonoidHom.Mathlib.LibraryNote.«range copy pattern» :

LibraryNote

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

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

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

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

and then finally define:

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

Equations

MonoidHom.Mathlib.LibraryNote.«range copy pattern» = ()

Instances For

source

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

Submonoid N

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

Equations

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

Instances For

source

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

AddSubmonoid N

The range of an AddMonoidHom is an AddSubmonoid.

Equations

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

Instances For

source

@[simp]

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

↑(mrange f) = Set.range ⇑f

source

@[simp]

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

↑(mrange f) = Set.range ⇑f

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

mrange f = Submonoid.map f ⊤

source

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

mrange f = AddSubmonoid.map f ⊤

source

@[simp]

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

mrange (id M) = ⊤

source

@[simp]

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

mrange (id M) = ⊤

source

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

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

source

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

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

source

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

mrange f = ⊤ ↔ Function.Surjective ⇑f

source

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

mrange f = ⊤ ↔ Function.Surjective ⇑f

source

@[simp]

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

mrange f = ⊤

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

source

@[simp]

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

mrange f = ⊤

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

source

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

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

source

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

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

source

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

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

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

source

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

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

↥s →* N

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

Equations

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

Instances For

source

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

↥s →+ N

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

Equations

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

Instances For

source

@[simp]

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

(f.restrict s) x = f ↑x

source

@[simp]

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

(f.restrict s) x = f ↑x

source

@[simp]

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

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

source

@[simp]

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

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

source

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

M →* ↥s

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

Equations

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

Instances For

source

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

M →+ ↥s

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

M →* ↥(mrange f)

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

Equations

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

Instances For

source

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

M →+ ↥(mrange f)

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

Equations

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

Instances For

source

@[simp]

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

↑(f.mrangeRestrict x) = f x

source

@[simp]

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

↑(f.mrangeRestrict x) = f x

source

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

Function.Surjective ⇑f.mrangeRestrict

source

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

Function.Surjective ⇑f.mrangeRestrict

source

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

Submonoid M

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

Equations

MonoidHom.mker f = Submonoid.comap f ⊥

Instances For

source

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

AddSubmonoid M

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

Equations

AddMonoidHom.mker f = AddSubmonoid.comap f ⊥

Instances For

source

@[simp]

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

x ∈ mker f ↔ f x = 1

source

@[simp]

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

x ∈ mker f ↔ f x = 0

source

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

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

source

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

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

source

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

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

Equations

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

source

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

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

Equations

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

source

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

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

source

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

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

source

@[simp]

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

Submonoid.comap f ⊥ = mker f

source

@[simp]

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

AddSubmonoid.comap f ⊥ = mker f

source

@[simp]

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

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

source

@[simp]

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

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

source

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

mker f.mrangeRestrict = mker f

source

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

mker f.mrangeRestrict = mker f

source

@[simp]

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

mker 1 = ⊤

source

@[simp]

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

mker 0 = ⊤

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

mker (inl M N) = ⊥

source

@[simp]

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

mker (inl M N) = ⊥

source

@[simp]

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

mker (inr M N) = ⊥

source

@[simp]

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

mker (inr M N) = ⊥

source

@[simp]

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

mker (fst M N) = ⊥.prod ⊤

source

@[simp]

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

mker (fst M N) = ⊥.prod ⊤

source

@[simp]

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

mker (snd M N) = ⊤.prod ⊥

source

@[simp]

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

mker (snd M N) = ⊤.prod ⊥

source

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

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

The MonoidHom from the preimage of a submonoid to itself.

Equations

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

Instances For

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

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

Function.Surjective ⇑(f.submonoidComap N')

source

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

Function.Surjective ⇑(f.addSubmonoidComap N')

source

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

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

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

Equations

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

Instances For

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

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

Function.Surjective ⇑(f.submonoidMap M')

source

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

Function.Surjective ⇑(f.addSubmonoidMap M')

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

↥S →* ↥T

The monoid hom associated to an inclusion of submonoids.

Equations

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

Instances For

source

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

↥S →+ ↥T

The AddMonoid hom associated to an inclusion of submonoids.

Equations

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

Instances For

source

@[simp]

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

↑((inclusion h) a) = ↑a

source

@[simp]

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

↑((inclusion h) a) = ↑a

source

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

Function.Injective ⇑(inclusion h)

source

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

Function.Injective ⇑(inclusion h)

source

@[simp]

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

(inclusion h) x = (inclusion h) y ↔ x = y

source

@[simp]

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

(inclusion h) x = (inclusion h) y ↔ x = y

source

@[simp]

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

T.subtype.comp (inclusion h) = S.subtype

source

@[simp]

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

T.subtype.comp (inclusion h) = S.subtype

source

@[simp]

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

MonoidHom.mrange s.subtype = s

source

@[simp]

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

AddMonoidHom.mrange s.subtype = s

source

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

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

source

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

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

source

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

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

source

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

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

source

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

S = ⊥

source

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

S = ⊥

source

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

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

source

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

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

source

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

S = ⊥ ∨ Nontrivial ↥S

A submonoid is either the trivial submonoid or nontrivial.

source

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

S = ⊥ ∨ Nontrivial ↥S

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

source

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

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

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

source

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

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

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

source

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

Submonoid ((i : ι) → M i)

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

Equations

Submonoid.pi I S = { carrier := I.pi fun (i : ι) => (S i).carrier, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

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

AddSubmonoid ((i : ι) → M i)

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

Equations

AddSubmonoid.pi I S = { carrier := I.pi fun (i : ι) => (S i).carrier, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

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

↑(pi I S) = I.pi fun (i : ι) => ↑(S i)

source

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

↑(pi I S) = I.pi fun (i : ι) => ↑(S i)

source

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

p ∈ pi I S ↔ ∀ i ∈ I, p i ∈ S i

source

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

p ∈ pi I S ↔ ∀ i ∈ I, p i ∈ S i

source

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

(pi I fun (i : ι) => ⊤) = ⊤

source

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

(pi I fun (i : ι) => ⊤) = ⊤

source

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

pi ∅ H = ⊤

source

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

pi ∅ H = ⊤

source

theorem Submonoid.pi_bot {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] :

(pi Set.univ fun (i : ι) => ⊥) = ⊥

source

theorem AddSubmonoid.pi_bot {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] :

(pi Set.univ fun (i : ι) => ⊥) = ⊥

source

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

J ≤ pi I S ↔ ∀ i ∈ I, J ≤ comap (Pi.evalMonoidHom M i) (S i)

source

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

J ≤ pi I S ↔ ∀ i ∈ I, J ≤ comap (Pi.evalAddMonoidHom M i) (S i)

source

@[simp]

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

Pi.mulSingle i x ∈ pi I S ↔ i ∈ I → x ∈ S i

source

@[simp]

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

Pi.single i x ∈ pi I S ↔ i ∈ I → x ∈ S i

source

theorem Submonoid.pi_eq_bot_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → MulOneClass (M i)] (S : (i : ι) → Submonoid (M i)) :

pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

source

theorem AddSubmonoid.pi_eq_bot_iff {ι : Type u_4} {M : ι → Type u_5} [(i : ι) → AddZeroClass (M i)] (S : (i : ι) → AddSubmonoid (M i)) :

pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

source

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

S i ≤ comap (MonoidHom.mulSingle M i) (pi I S)

source

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

S i ≤ comap (AddMonoidHom.single M i) (pi I S)

source

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

⨆ (i : ι), map (MonoidHom.mulSingle M i) (S i) ≤ pi I S

source

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

⨆ (i : ι), map (AddMonoidHom.single M i) (S i) ≤ pi I S

source

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

↥S ≃* ↥T

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

Equations

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

Instances For

source

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

↥S ≃+ ↥T

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

Equations

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

Instances For

source

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

M ≃* ↥(MonoidHom.mrange f)

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

Equations

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

Instances For

source

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

M ≃+ ↥(AddMonoidHom.mrange f)

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

Equations

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

Instances For

source

@[simp]

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

(ofLeftInverse' f h).symm a✝ = g ↑a✝

source

@[simp]

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

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

source

@[simp]

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

(ofLeftInverse' f h).symm a✝ = g ↑a✝

source

@[simp]

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

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

source

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

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

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

Equations

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

Instances For

source

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[deprecated AddEquiv.addSubmonoidMap_symm_apply (since := "2025-08-20")]

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

Alias of AddEquiv.addSubmonoidMap_symm_apply.

source

@[simp]

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

S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

source

@[simp]

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

S.equivMapOfInjective ↑e ⋯ = e.addSubmonoidMap S

source

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

FaithfulSMul (↥S) α

source

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

FaithfulVAdd (↥S) α

source

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

Mˣ ≃* ↥(IsUnit.submonoid M)

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

Equations

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