Operations on `Submonoid`s #

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

Main definitions #

Conversion between multiplicative and additive definitions #

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

(Commutative) monoid structure on a submonoid #

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

Group actions by submonoids #

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

Operations on submonoids #

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

Monoid homomorphisms between submonoid #

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

Operations on `MonoidHom`s #

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

Tags #

submonoid, range, product, map, comap

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

Submonoid M ≃o AddSubmonoid (Additive M)

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

Equations

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

source

@[inline, reducible]

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' = OrderIso.symm Submonoid.toAddSubmonoid

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

AddSubmonoid A ≃o Submonoid (Multiplicative A)

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

Equations

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

source

@[inline, reducible]

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' = OrderIso.symm AddSubmonoid.toSubmonoid

source

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

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

source

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

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

`comap` and `map` #

source

theorem AddSubmonoid.comap.proof_2 {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 N) :

f 0 ∈ S

source

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

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 = { toAddSubsemigroup := { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯ }, zero_mem' := ⋯ }

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 = { toSubsemigroup := { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯ }, one_mem' := ⋯ }

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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 = { toAddSubsemigroup := { carrier := ⇑f '' ↑S, add_mem' := ⋯ }, zero_mem' := ⋯ }

source

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

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 = { toSubsemigroup := { carrier := ⇑f '' ↑S, mul_mem' := ⋯ }, one_mem' := ⋯ }

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

f x ∈ AddSubmonoid.map f S

source

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

f x ∈ Submonoid.map f S

source

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

f ↑x ∈ AddSubmonoid.map f S

source

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

f ↑x ∈ Submonoid.map f S

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

Monotone (AddSubmonoid.map f)

source

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

Monotone (Submonoid.map f)

source

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

Monotone (AddSubmonoid.comap f)

source

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

Monotone (Submonoid.comap f)

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

AddSubmonoid.map f ⊥ = ⊥

source

@[simp]

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

Submonoid.map f ⊥ = ⊥

source

@[simp]

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

AddSubmonoid.comap f ⊤ = ⊤

source

@[simp]

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

Submonoid.comap f ⊤ = ⊤

source

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

⋯ = ⋯

source

@[simp]

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

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

source

@[simp]

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

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

source

theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [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

source

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

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

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

Equations

AddSubmonoid.gciMapComap hf = GaloisConnection.toGaloisCoinsertion ⋯ ⋯

source

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

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

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

Equations

Submonoid.gciMapComap hf = GaloisConnection.toGaloisCoinsertion ⋯ ⋯

source

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

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

source

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

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

source

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

Function.Surjective (AddSubmonoid.comap f)

source

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

Function.Surjective (Submonoid.comap f)

source

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

Function.Injective (AddSubmonoid.map f)

source

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

Function.Injective (Submonoid.map f)

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

StrictMono (AddSubmonoid.map f)

source

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

StrictMono (Submonoid.map f)

source

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

⋯ = ⋯

source

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

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

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

Equations

AddSubmonoid.giMapComap hf = GaloisConnection.toGaloisInsertion ⋯ ⋯

source

theorem AddSubmonoid.giMapComap.proof_1 {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} (hf : Function.Surjective ⇑f) (S : AddSubmonoid N) (x : N) (h : x ∈ S) :

x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S)

source

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

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

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

Equations

Submonoid.giMapComap hf = GaloisConnection.toGaloisInsertion ⋯ ⋯

source

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

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

source

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

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

source

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

Function.Surjective (AddSubmonoid.map f)

source

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

Function.Surjective (Submonoid.map f)

source

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

Function.Injective (AddSubmonoid.comap f)

source

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

Function.Injective (Submonoid.comap f)

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

StrictMono (AddSubmonoid.comap f)

source

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

StrictMono (Submonoid.comap f)

source

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 := { val := 0, property := ⋯ } }

source

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 := { val := 1, property := ⋯ } }

source

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

source

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

source

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

source

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

source

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

0 = { val := 0, property := ⋯ }

source

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

1 = { val := 1, property := ⋯ }

source

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) => { val := n • ↑a, property := ⋯ } }

source

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 : ℕ) => { val := ↑a ^ n, property := ⋯ } }

source

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

source

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

source

@[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 • { val := x, property := hx } = { val := n • x, property := ⋯ }

source

@[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 : ℕ) :

{ val := x, property := hx } ^ n = { val := x ^ n, property := ⋯ }

source

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)

source

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

source

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

source

theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :

Function.Injective fun (a : ↥S) => ↑a

source

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

source

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)

source

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

source

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

ZeroMemClass A M

source

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

source

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)

source

theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :

Function.Injective fun (a : ↥S) => ↑a

source

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

source

theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :

Function.Injective fun (a : ↥S) => ↑a

source

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)

source

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

source

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

source

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

ZeroMemClass A M

source

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)

source

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

source

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

source

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

source

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' = { toZeroHom := { toFun := Subtype.val, map_zero' := ⋯ }, map_add' := ⋯ }

source

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' = { toOneHom := { toFun := Subtype.val, map_one' := ⋯ }, map_mul' := ⋯ }

source

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

source

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

source

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

↑a + ↑b ∈ S

source

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

Add ↥S

An AddSubmonoid of an AddMonoid inherits an addition.

Equations

AddSubmonoid.add S = { add := fun (a b : ↥S) => { val := ↑a + ↑b, property := ⋯ } }

source

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

Mul ↥S

A submonoid of a monoid inherits a multiplication.

Equations

Submonoid.mul S = { mul := fun (a b : ↥S) => { val := ↑a * ↑b, property := ⋯ } }

source

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

Zero ↥S

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

AddSubmonoid.zero S = { zero := { val := 0, property := ⋯ } }

source

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

One ↥S

A submonoid of a monoid inherits a 1.

Equations

Submonoid.one S = { one := { val := 1, property := ⋯ } }

source

@[simp]

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

↑(x + y) = ↑x + ↑y

source

@[simp]

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

↑(x * y) = ↑x * ↑y

source

@[simp]

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

↑0 = 0

source

@[simp]

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

↑1 = 1

source

@[simp]

theorem AddSubmonoid.mk_eq_zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) {a : M} {ha : a ∈ S} :

{ val := a, property := ha } = 0 ↔ a = 0

source

@[simp]

theorem Submonoid.mk_eq_one {M : Type u_1} [MulOneClass M] (S : Submonoid M) {a : M} {ha : a ∈ S} :

{ val := a, property := ha } = 1 ↔ a = 1

source

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

{ val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := ⋯ }

source

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

{ val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := ⋯ }

source

theorem AddSubmonoid.add_def {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (x : ↥S) (y : ↥S) :

x + y = { val := ↑x + ↑y, property := ⋯ }

source

theorem Submonoid.mul_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) (x : ↥S) (y : ↥S) :

x * y = { val := ↑x * ↑y, property := ⋯ }

source

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

0 = { val := 0, property := ⋯ }

source

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

1 = { val := 1, property := ⋯ }

source

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

Function.Injective fun (a : ↥S) => ↑a

source

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

↑0 = ↑0

source

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

∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

source

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

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

source

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

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

source

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

n • x ∈ S

source

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

x ^ n ∈ S

source

theorem AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

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

↑0 = ↑0

source

theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

source

theorem AddSubmonoid.toAddMonoid.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :

Function.Injective fun (a : ↥S) => ↑a

source

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

AddMonoid ↥S

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

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

source

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

AddSubmonoidClass (AddSubmonoid M) M

source

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

Monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

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

source

theorem AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

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

AddSubmonoidClass (AddSubmonoid M) M

source

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

AddCommMonoid ↥S

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

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

source

theorem AddSubmonoid.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

source

theorem AddSubmonoid.toAddCommMonoid.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun (a : ↥S) => ↑a

source

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

↑0 = ↑0

source

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

CommMonoid ↥S

A submonoid of a CommMonoid is a CommMonoid.

Equations

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

source

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

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

source

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

↑0 = ↑0

source

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

∀ (x x_1 : ↥S), ↑x + ↑x_1 = ↑x + ↑x_1

source

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

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

source

@[simp]

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

⇑(AddSubmonoid.subtype S) = Subtype.val

source

@[simp]

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

⇑(Submonoid.subtype S) = Subtype.val

source

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

↥⊤ ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

Equations

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

source

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

{ val := ↑x, property := ⋯ } = x

source

theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] :

∀ (x : M), (fun (x : ↥⊤) => ↑x) ((fun (x : M) => { val := x, property := ⋯ }) x) = (fun (x : ↥⊤) => ↑x) ((fun (x : M) => { val := x, property := ⋯ }) x)

source

theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [AddZeroClass M] :

∀ (x x_1 : ↥⊤), { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1)

source

@[simp]

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

AddSubmonoid.topEquiv x = ↑x

source

@[simp]

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

↑((MulEquiv.symm Submonoid.topEquiv) x) = x

source

@[simp]

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

Submonoid.topEquiv x = ↑x

source

@[simp]

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

↑((AddEquiv.symm AddSubmonoid.topEquiv) x) = x

source

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

↥⊤ ≃* M

The top submonoid is isomorphic to the monoid.

Equations

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

source

@[simp]

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

AddEquiv.toAddMonoidHom AddSubmonoid.topEquiv = AddSubmonoid.subtype ⊤

source

@[simp]

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

MulEquiv.toMonoidHom Submonoid.topEquiv = Submonoid.subtype ⊤

source

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

source

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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 ∈ AddSubmonoid.prod s t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

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 ∈ Submonoid.prod s t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

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₂) :

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

source

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₂) :

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

AddSubmonoid.prod ⊤ ⊤ = ⊤

source

@[simp]

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

Submonoid.prod ⊤ ⊤ = ⊤

source

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

AddSubmonoid.prod ⊥ ⊥ = ⊥

source

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

Submonoid.prod ⊥ ⊥ = ⊥

source

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

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

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

Equations

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

source

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 : ↥(AddSubmonoid.prod s t)), (Equiv.Set.prod ↑s ↑t).toFun (x + x_1) = (Equiv.Set.prod ↑s ↑t).toFun (x + x_1)

source

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

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

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

Equations

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

source

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 ∈ AddSubmonoid.prod s ⊥ → Prop) :

∀ (x : p ∈ AddSubmonoid.prod s ⊥), (∀ (hps : p.1 ∈ ↑s) (hp1 : p.2 ∈ ↑⊥), motive ⋯) → motive x

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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 = AddSubmonoid.prod s ⊥

source

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 = Submonoid.prod s ⊥

source

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

⋯ = ⋯

source

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 = AddSubmonoid.prod ⊥ s

source

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 ∈ AddSubmonoid.prod ⊥ s → Prop) :

∀ (x : p ∈ AddSubmonoid.prod ⊥ s), (∀ (hp1 : p.1 ∈ ↑⊥) (hps : p.2 ∈ ↑s), motive ⋯) → motive x

Equations

⋯ = ⋯

source

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 = Submonoid.prod ⊥ s

source

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

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

source

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

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

source

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

source

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

source

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

source

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

source

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 (AddEquiv.toAddMonoidHom f) K = AddSubmonoid.map (AddEquiv.toAddMonoidHom (AddEquiv.symm f)) K

source

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 (MulEquiv.toMonoidHom f) K = Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.symm f)) K

source

@[simp]

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

AddSubmonoid.map (AddEquiv.toAddMonoidHom f) ⊤ = ⊤

source

@[simp]

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

Submonoid.map (MulEquiv.toMonoidHom f) ⊤ = ⊤

source

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

source

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

source

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)} :

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

source

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)} :

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

source

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

source

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.copy (AddSubmonoid.map f ⊤) (Set.range ⇑f) ⋯

source

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.copy (Submonoid.map 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_5} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

AddMonoidHom.mrange f = AddSubmonoid.map f ⊤

source

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

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

source

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

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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.

source

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.

source

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

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

source

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

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

source

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

(AddMonoidHom.restrict f s) x = f ↑x

source

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

(MonoidHom.restrict f s) x = f ↑x

source

@[simp]

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

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

source

@[simp]

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

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

source

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) => { val := f n, property := ⋯ }, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_zero' := ⋯ }.toFun x + { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_zero' := ⋯ }.toFun y

source

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

AddMonoidHom.codRestrict f s h = { toZeroHom := { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_zero' := ⋯ }, map_add' := ⋯ }

source

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) => { val := f n, property := ⋯ }) 0 = 0

source

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

(MonoidHom.codRestrict f s h) n = { val := f n, property := ⋯ }

source

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

(AddMonoidHom.codRestrict f s h) n = { val := f n, property := ⋯ }

source

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

MonoidHom.codRestrict f s h = { toOneHom := { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_one' := ⋯ }, map_mul' := ⋯ }

source

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

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

source

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

source

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

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

source

@[simp]

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

↑((AddMonoidHom.mrangeRestrict f) x) = f x

source

@[simp]

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

↑((MonoidHom.mrangeRestrict f) x) = f x

source

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 { val := f x, property := ⋯ }) → motive x

Equations

⋯ = ⋯

source

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

Function.Surjective ⇑(AddMonoidHom.mrangeRestrict f)

source

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

Function.Surjective ⇑(MonoidHom.mrangeRestrict f)

source

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 ⊥

source

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 ⊥

source

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

source

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

source

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}

source

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}

source

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

source

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

source

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

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

source

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

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

source

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

source

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

AddMonoidHom.mker (AddMonoidHom.mrangeRestrict f) = AddMonoidHom.mker f

source

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

MonoidHom.mker (MonoidHom.mrangeRestrict f) = MonoidHom.mker f

source

@[simp]

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

AddMonoidHom.mker 0 = ⊤

source

@[simp]

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

MonoidHom.mker 1 = ⊤

source

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

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

source

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

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

source

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

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

source

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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')) => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun x + { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun y

source

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')) => { val := f ↑x, property := ⋯ }) 0 = 0

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

AddMonoidHom.addSubmonoidComap f N' = { toZeroHom := { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }, map_add' := ⋯ }

source

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'

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

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

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

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

source

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

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

The MonoidHom from the preimage of a submonoid to itself.

Equations

MonoidHom.submonoidComap f N' = { toOneHom := { toFun := fun (x : ↥(Submonoid.comap f N')) => { val := f ↑x, property := ⋯ }, map_one' := ⋯ }, map_mul' := ⋯ }

source

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') => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : ↥M') => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun x + { toFun := fun (x : ↥M') => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }.toFun y

source

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') => { val := f ↑x, property := ⋯ }) 0 = 0

source

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

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

AddMonoidHom.addSubmonoidMap f M' = { toZeroHom := { toFun := fun (x : ↥M') => { val := f ↑x, property := ⋯ }, map_zero' := ⋯ }, map_add' := ⋯ }

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

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

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

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

source

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

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

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

Equations

MonoidHom.submonoidMap f M' = { toOneHom := { toFun := fun (x : ↥M') => { val := f ↑x, property := ⋯ }, map_one' := ⋯ }, map_mul' := ⋯ }

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 ⇑(AddMonoidHom.addSubmonoidMap f M')

source

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

Function.Surjective ⇑(MonoidHom.submonoidMap f M')

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

Submonoid.prod s 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} :

AddSubmonoid.prod s 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} :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

(AddSubmonoid.subtype S) x ∈ T

source

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

↥S →+ ↥T

The AddMonoid hom associated to an inclusion of submonoids.

Equations

AddSubmonoid.inclusion h = AddMonoidHom.codRestrict (AddSubmonoid.subtype S) T ⋯

source

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

↥S →* ↥T

The monoid hom associated to an inclusion of submonoids.

Equations

Submonoid.inclusion h = MonoidHom.codRestrict (Submonoid.subtype S) T ⋯

source

@[simp]

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

AddMonoidHom.mrange (AddSubmonoid.subtype s) = s

source

@[simp]

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

MonoidHom.mrange (Submonoid.subtype s) = s

source

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

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

source

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

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

source

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

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

source

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

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

source

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

S = ⊥

source

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

S = ⊥

source

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

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

source

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

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

source

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

S = ⊥ ∨ Nontrivial ↥S

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

source

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

S = ⊥ ∨ Nontrivial ↥S

A submonoid is either the trivial submonoid or nontrivial.

source

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

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

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

source

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

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

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

source

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

↥S ≃+ ↥T

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

Equations

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

source

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

↑S = ↑T

source

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)

source

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

↥S ≃* ↥T

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

Equations

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

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

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

source

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

⋯ = ⋯

source

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

(AddMonoidHom.mrangeRestrict f).toFun (x + y) = (AddMonoidHom.mrangeRestrict f).toFun x + (AddMonoidHom.mrangeRestrict f).toFun y

source

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

(AddMonoidHom.mrangeRestrict f) ((g ∘ ⇑(AddSubmonoid.subtype (AddMonoidHom.mrange f))) x) = x

source

@[simp]

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

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

M ≃* ↥(MonoidHom.mrange f)

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

Equations

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

source

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

∀ (x x_1 : ↥S), (Equiv.image ↑e ↑S).toFun (x + x_1) = (Equiv.image ↑e ↑S).toFun x + (Equiv.image ↑e ↑S).toFun x_1

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 (AddEquiv.toAddMonoidHom 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

AddEquiv.addSubmonoidMap e S = let __src := Equiv.image ↑e ↑S; { toEquiv := __src, map_add' := ⋯ }

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 (MulEquiv.toMonoidHom 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

MulEquiv.submonoidMap e S = let __src := Equiv.image ↑e ↑S; { toEquiv := __src, map_mul' := ⋯ }

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

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

source

@[simp]

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

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

source

@[simp]

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

(AddEquiv.symm (AddEquiv.addSubmonoidMap e S)) g = { val := (AddEquiv.symm e) ↑g, property := ⋯ }

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

(MulEquiv.symm (MulEquiv.submonoidMap e S)) g = { val := (MulEquiv.symm e) ↑g, property := ⋯ }

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

AddSubmonoid.equivMapOfInjective S ↑e ⋯ = AddEquiv.addSubmonoidMap e S

source

@[simp]

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

Submonoid.equivMapOfInjective S ↑e ⋯ = MulEquiv.submonoidMap e S

Actions by `Submonoid`s #

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

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

source

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

VAdd (↥S) α

Equations

AddSubmonoid.vadd S = VAdd.comp α ⇑(AddSubmonoid.subtype S)

source

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

SMul (↥S) α

Equations

Submonoid.smul S = SMul.comp α ⇑(Submonoid.subtype S)

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

source

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

source

@[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 : α) :

{ val := g, property := hg } +ᵥ a = g +ᵥ a

source

@[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 : α) :

{ val := g, property := hg } • a = g • a

source

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

FaithfulSMul (↥S) α

Equations

⋯ = ⋯

source

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

AddSubmonoid.addAction S = AddAction.compHom α (AddSubmonoid.subtype S)

source

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

Submonoid.mulAction S = MulAction.compHom α (Submonoid.subtype S)

source

instance Submonoid.distribMulAction {M' : Type u_5} {α : Type u_6} [Monoid M'] [AddMonoid α] [DistribMulAction M' α] (S : Submonoid M') :

DistribMulAction (↥S) α

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

Equations

Submonoid.distribMulAction S = DistribMulAction.compHom α (Submonoid.subtype S)

source

instance Submonoid.mulDistribMulAction {M' : Type u_5} {α : Type u_6} [Monoid M'] [Monoid α] [MulDistribMulAction M' α] (S : Submonoid M') :

MulDistribMulAction (↥S) α

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

Equations

Submonoid.mulDistribMulAction S = MulDistribMulAction.compHom α (Submonoid.subtype S)

source

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

(fun (x : AddUnits M) => { val := ↑x, property := ⋯ }) ((fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯) x) = x

source

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

AddUnits M ≃+ ↥(IsAddUnit.addSubmonoid M)

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

Equations

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

source

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

{ toFun := fun (x : AddUnits M) => { val := ↑x, property := ⋯ }, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := fun (x : AddUnits M) => { val := ↑x, property := ⋯ }, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (x : AddUnits M) => { val := ↑x, property := ⋯ }, invFun := fun (x : ↥(IsAddUnit.addSubmonoid M)) => IsAddUnit.addUnit ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

source