Operations on submonoids
In this file we define various operations on submonoids and monoid_homs.
Main definitions
Conversion between multiplicative and additive definitions
submonoid.to_add_submonoid,submonoid.of_add_submonoid,add_submonoid.to_submonoid,add_submonoid.of_submonoid: convert between multiplicative and additive submonoids ofM,multiplicative M, andadditive M.submonoid.add_submonoid_equiv: equivalence betweensubmonoid Mandadd_submonoid (additive M).
(Commutative) monoid structure on a submonoid
submonoid.to_monoid,submonoid.to_comm_monoid: a submonoid inherits a (commutative) monoid structure.
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 submonoidss : submonoid Mandt : submonoid Nas a submonoid ofM × N;
Monoid homomorphisms between submonoid
submonoid.subtype: embedding of a submonoid into the ambient monoid.submonoid.inclusion: given two submonoidsS,Tsuch thatS ≤ T,S.inclusion Tis the inclusion ofSintoTas a monoid homomorphism;mul_equiv.submonoid_congr: converts a proof ofS = Tinto a monoid isomorphism betweenSandT.submonoid.prod_equiv: monoid isomorphism betweens.prod tands × t;
Operations on monoid_homs
monoid_hom.mrange: range of a monoid homomorphism as a submonoid of the codomain;monoid_hom.mrestrict: restrict a monoid homomorphism to a submonoid;monoid_hom.cod_mrestrict: restrict the codomain of a monoid homomorphism to a submonoid;monoid_hom.mrange_restrict: restrict a monoid homomorphism to its range;
Tags
submonoid, range, product, map, comap
Conversion to/from additive/multiplicative
def
submonoid.to_add_submonoid
{M : Type u_1}
[monoid M] :
submonoid M → add_submonoid (additive M)
Map from submonoids of monoid M to add_submonoids of additive M.
def
submonoid.of_add_submonoid
{M : Type u_1}
[monoid M] :
add_submonoid (additive M) → submonoid M
Map from add_submonoids of additive M to submonoids of M.
def
add_submonoid.to_submonoid
{M : Type u_1}
[add_monoid M] :
add_submonoid M → submonoid (multiplicative M)
Map from add_submonoids of add_monoid M to submonoids of multiplicative M.
def
add_submonoid.of_submonoid
{M : Type u_1}
[add_monoid M] :
submonoid (multiplicative M) → add_submonoid M
Map from submonoids of multiplicative M to add_submonoids of add_monoid M.
def
submonoid.add_submonoid_equiv
(M : Type u_1)
[monoid M] :
submonoid M ≃ add_submonoid (additive M)
Submonoids of monoid M are isomorphic to additive submonoids of additive M.
Equations
- submonoid.add_submonoid_equiv M = {to_fun := submonoid.to_add_submonoid _inst_4, inv_fun := submonoid.of_add_submonoid _inst_4, left_inv := _, right_inv := _}
comap and map
def
add_submonoid.comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(M →+ N) → add_submonoid N → add_submonoid M
The preimage of an add_submonoid along an add_monoid homomorphism is an
add_submonoid.
@[simp]
theorem
add_submonoid.coe_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S : add_submonoid N)
(f : M →+ N) :
@[simp]
theorem
add_submonoid.mem_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{S : add_submonoid N}
{f : M →+ N}
{x : M} :
x ∈ add_submonoid.comap f S ↔ ⇑f x ∈ S
theorem
submonoid.comap_comap
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[monoid M]
[monoid N]
[monoid P]
(S : submonoid P)
(g : N →* P)
(f : M →* N) :
submonoid.comap f (submonoid.comap g S) = submonoid.comap (g.comp f) S
theorem
add_submonoid.comap_comap
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[add_monoid M]
[add_monoid N]
[add_monoid P]
(S : add_submonoid P)
(g : N →+ P)
(f : M →+ N) :
add_submonoid.comap f (add_submonoid.comap g S) = add_submonoid.comap (g.comp f) S
@[simp]
theorem
submonoid.comap_id
{P : Type u_3}
[monoid P]
(S : submonoid P) :
submonoid.comap (monoid_hom.id P) S = S
theorem
add_submonoid.comap_id
{P : Type u_3}
[add_monoid P]
(S : add_submonoid P) :
add_submonoid.comap (add_monoid_hom.id P) S = S
def
add_submonoid.map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(M →+ N) → add_submonoid M → add_submonoid N
The image of an add_submonoid along an add_monoid homomorphism is
an add_submonoid.
@[simp]
theorem
add_submonoid.coe_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(S : add_submonoid M) :
@[simp]
theorem
add_submonoid.mem_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{f : M →+ N}
{S : add_submonoid M}
{y : N} :
theorem
add_submonoid.map_map
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[add_monoid M]
[add_monoid N]
[add_monoid P]
(S : add_submonoid M)
(g : N →+ P)
(f : M →+ N) :
add_submonoid.map g (add_submonoid.map f S) = add_submonoid.map (g.comp f) S
theorem
submonoid.map_map
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[monoid M]
[monoid N]
[monoid P]
(S : submonoid M)
(g : N →* P)
(f : M →* N) :
submonoid.map g (submonoid.map f S) = submonoid.map (g.comp f) S
theorem
submonoid.map_le_iff_le_comap
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
{S : submonoid M}
{T : submonoid N} :
submonoid.map f S ≤ T ↔ S ≤ submonoid.comap f T
theorem
add_submonoid.map_le_iff_le_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{f : M →+ N}
{S : add_submonoid M}
{T : add_submonoid N} :
add_submonoid.map f S ≤ T ↔ S ≤ add_submonoid.comap f T
theorem
add_submonoid.gc_map_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N) :
theorem
submonoid.map_le_of_le_comap
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S : submonoid M)
{T : submonoid N}
{f : M →* N} :
S ≤ submonoid.comap f T → submonoid.map f S ≤ T
theorem
add_submonoid.map_le_of_le_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S : add_submonoid M)
{T : add_submonoid N}
{f : M →+ N} :
S ≤ add_submonoid.comap f T → add_submonoid.map f S ≤ T
theorem
add_submonoid.le_comap_of_map_le
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S : add_submonoid M)
{T : add_submonoid N}
{f : M →+ N} :
add_submonoid.map f S ≤ T → S ≤ add_submonoid.comap f T
theorem
submonoid.le_comap_of_map_le
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S : submonoid M)
{T : submonoid N}
{f : M →* N} :
submonoid.map f S ≤ T → S ≤ submonoid.comap f T
theorem
add_submonoid.le_comap_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S : add_submonoid M)
{f : M →+ N} :
S ≤ add_submonoid.comap f (add_submonoid.map f S)
theorem
submonoid.le_comap_map
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S : submonoid M)
{f : M →* N} :
S ≤ submonoid.comap f (submonoid.map f S)
theorem
submonoid.map_comap_le
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{S : submonoid N}
{f : M →* N} :
submonoid.map f (submonoid.comap f S) ≤ S
theorem
add_submonoid.map_comap_le
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{S : add_submonoid N}
{f : M →+ N} :
add_submonoid.map f (add_submonoid.comap f S) ≤ S
theorem
add_submonoid.monotone_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{f : M →+ N} :
theorem
add_submonoid.monotone_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{f : M →+ N} :
theorem
submonoid.monotone_comap
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
@[simp]
theorem
submonoid.map_comap_map
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S : submonoid M)
{f : M →* N} :
submonoid.map f (submonoid.comap f (submonoid.map f S)) = submonoid.map f S
@[simp]
theorem
add_submonoid.map_comap_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S : add_submonoid M)
{f : M →+ N} :
add_submonoid.map f (add_submonoid.comap f (add_submonoid.map f S)) = add_submonoid.map f S
@[simp]
theorem
add_submonoid.comap_map_comap
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{S : add_submonoid N}
{f : M →+ N} :
add_submonoid.comap f (add_submonoid.map f (add_submonoid.comap f S)) = add_submonoid.comap f S
@[simp]
theorem
submonoid.comap_map_comap
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{S : submonoid N}
{f : M →* N} :
submonoid.comap f (submonoid.map f (submonoid.comap f S)) = submonoid.comap f S
theorem
submonoid.map_sup
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S T : submonoid M)
(f : M →* N) :
submonoid.map f (S ⊔ T) = submonoid.map f S ⊔ submonoid.map f T
theorem
add_submonoid.map_sup
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S T : add_submonoid M)
(f : M →+ N) :
add_submonoid.map f (S ⊔ T) = add_submonoid.map f S ⊔ add_submonoid.map f T
theorem
submonoid.map_supr
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Sort u_3}
(f : M →* N)
(s : ι → submonoid M) :
submonoid.map f (supr s) = ⨆ (i : ι), submonoid.map f (s i)
theorem
add_submonoid.map_supr
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{ι : Sort u_3}
(f : M →+ N)
(s : ι → add_submonoid M) :
add_submonoid.map f (supr s) = ⨆ (i : ι), add_submonoid.map f (s i)
theorem
submonoid.comap_inf
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(S T : submonoid N)
(f : M →* N) :
submonoid.comap f (S ⊓ T) = submonoid.comap f S ⊓ submonoid.comap f T
theorem
add_submonoid.comap_inf
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(S T : add_submonoid N)
(f : M →+ N) :
add_submonoid.comap f (S ⊓ T) = add_submonoid.comap f S ⊓ add_submonoid.comap f T
theorem
add_submonoid.comap_infi
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{ι : Sort u_3}
(f : M →+ N)
(s : ι → add_submonoid N) :
add_submonoid.comap f (infi s) = ⨅ (i : ι), add_submonoid.comap f (s i)
theorem
submonoid.comap_infi
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Sort u_3}
(f : M →* N)
(s : ι → submonoid N) :
submonoid.comap f (infi s) = ⨅ (i : ι), submonoid.comap f (s i)
@[simp]
theorem
submonoid.map_bot
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N) :
submonoid.map f ⊥ = ⊥
@[simp]
theorem
add_submonoid.map_bot
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N) :
add_submonoid.map f ⊥ = ⊥
@[simp]
theorem
submonoid.comap_top
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N) :
submonoid.comap f ⊤ = ⊤
@[simp]
theorem
add_submonoid.comap_top
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N) :
@[simp]
theorem
add_submonoid.map_id
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M) :
add_submonoid.map (add_monoid_hom.id M) S = S
@[simp]
theorem
submonoid.map_id
{M : Type u_1}
[monoid M]
(S : submonoid M) :
submonoid.map (monoid_hom.id M) S = S
map f and comap f form a galois_coinsertion when f is injective.
Equations
theorem
submonoid.comap_map_eq_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.injective ⇑f)
(S : submonoid M) :
submonoid.comap f (submonoid.map f S) = S
theorem
submonoid.comap_surjective_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
theorem
submonoid.map_injective_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
theorem
submonoid.comap_inf_map_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.injective ⇑f)
(S T : submonoid M) :
submonoid.comap f (submonoid.map f S ⊓ submonoid.map f T) = S ⊓ T
theorem
submonoid.comap_infi_map_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Type u_4}
{f : M →* N}
(hf : function.injective ⇑f)
(S : ι → submonoid M) :
submonoid.comap f (⨅ (i : ι), submonoid.map f (S i)) = infi S
theorem
submonoid.comap_sup_map_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.injective ⇑f)
(S T : submonoid M) :
submonoid.comap f (submonoid.map f S ⊔ submonoid.map f T) = S ⊔ T
theorem
submonoid.comap_supr_map_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Type u_4}
{f : M →* N}
(hf : function.injective ⇑f)
(S : ι → submonoid M) :
submonoid.comap f (⨆ (i : ι), submonoid.map f (S i)) = supr S
theorem
submonoid.map_le_map_iff_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.injective ⇑f)
{S T : submonoid M} :
submonoid.map f S ≤ submonoid.map f T ↔ S ≤ T
theorem
submonoid.map_strict_mono_of_injective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
map f and comap f form a galois_insertion when f is surjective.
Equations
theorem
submonoid.map_comap_eq_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.surjective ⇑f)
(S : submonoid N) :
submonoid.map f (submonoid.comap f S) = S
theorem
submonoid.map_surjective_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
theorem
submonoid.comap_injective_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
theorem
submonoid.map_inf_comap_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.surjective ⇑f)
(S T : submonoid N) :
submonoid.map f (submonoid.comap f S ⊓ submonoid.comap f T) = S ⊓ T
theorem
submonoid.map_infi_comap_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Type u_4}
{f : M →* N}
(hf : function.surjective ⇑f)
(S : ι → submonoid N) :
submonoid.map f (⨅ (i : ι), submonoid.comap f (S i)) = infi S
theorem
submonoid.map_sup_comap_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.surjective ⇑f)
(S T : submonoid N) :
submonoid.map f (submonoid.comap f S ⊔ submonoid.comap f T) = S ⊔ T
theorem
submonoid.map_supr_comap_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{ι : Type u_4}
{f : M →* N}
(hf : function.surjective ⇑f)
(S : ι → submonoid N) :
submonoid.map f (⨆ (i : ι), submonoid.comap f (S i)) = supr S
theorem
submonoid.comap_le_comap_iff_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N}
(hf : function.surjective ⇑f)
{S T : submonoid N} :
submonoid.comap f S ≤ submonoid.comap f T ↔ S ≤ T
theorem
submonoid.comap_strict_mono_of_surjective
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
{f : M →* N} :
@[instance]
An add_submonoid of an add_monoid inherits an addition.
@[instance]
An add_submonoid of an add_monoid inherits a zero.
@[simp]
@[simp]
@[instance]
An add_submonoid of an add_monoid inherits an add_monoid
structure.
@[instance]
A submonoid of a monoid inherits a monoid structure.
Equations
- S.to_monoid = function.injective.monoid coe _ _ _
@[instance]
An add_submonoid of an add_comm_monoid is
an add_comm_monoid.
The natural monoid hom from an add_submonoid of add_monoid M to M.
@[simp]
def
add_submonoid.prod
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
add_submonoid M → add_submonoid N → add_submonoid (M × N)
Given add_submonoids s, t of add_monoids A, B respectively, s × t
as an add_submonoid of A × B.
theorem
add_submonoid.coe_prod
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid M)
(t : add_submonoid N) :
theorem
add_submonoid.mem_prod
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{s : add_submonoid M}
{t : add_submonoid N}
{p : M × N} :
theorem
add_submonoid.prod_mono
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{s₁ s₂ : add_submonoid M}
{t₁ t₂ : add_submonoid N} :
theorem
add_submonoid.prod_top
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid M) :
s.prod ⊤ = add_submonoid.comap (add_monoid_hom.fst M N) s
theorem
submonoid.prod_top
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(s : submonoid M) :
s.prod ⊤ = submonoid.comap (monoid_hom.fst M N) s
theorem
add_submonoid.top_prod
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid N) :
⊤.prod s = add_submonoid.comap (add_monoid_hom.snd M N) s
theorem
submonoid.top_prod
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(s : submonoid N) :
⊤.prod s = submonoid.comap (monoid_hom.snd M N) s
@[simp]
def
add_submonoid.prod_equiv
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid M)
(t : add_submonoid N) :
The product of additive submonoids is isomorphic to their product as additive monoids
def
submonoid.prod_equiv
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(s : submonoid M)
(t : submonoid N) :
The product of submonoids is isomorphic to their product as monoids.
theorem
add_submonoid.map_inl
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid M) :
add_submonoid.map (add_monoid_hom.inl M N) s = s.prod ⊥
theorem
submonoid.map_inl
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(s : submonoid M) :
submonoid.map (monoid_hom.inl M N) s = s.prod ⊥
theorem
submonoid.map_inr
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(s : submonoid N) :
submonoid.map (monoid_hom.inr M N) s = ⊥.prod s
theorem
add_submonoid.map_inr
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid N) :
add_submonoid.map (add_monoid_hom.inr M N) s = ⊥.prod s
@[simp]
theorem
add_submonoid.prod_bot_sup_bot_prod
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(s : add_submonoid M)
(t : add_submonoid N) :
def
add_monoid_hom.mrange
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(M →+ N) → add_submonoid N
The range of an add_monoid_hom is an add_submonoid.
The range of a monoid homomorphism is a submonoid.
Equations
- f.mrange = submonoid.map f ⊤
@[simp]
theorem
add_monoid_hom.coe_mrange
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N) :
@[simp]
theorem
add_monoid_hom.mem_mrange
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
{f : M →+ N}
{y : N} :
theorem
add_monoid_hom.map_mrange
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[add_monoid M]
[add_monoid N]
[add_monoid P]
(g : N →+ P)
(f : M →+ N) :
add_submonoid.map g f.mrange = (g.comp f).mrange
theorem
add_monoid_hom.mrange_top_iff_surjective
{M : Type u_1}
[add_monoid M]
{N : Type u_2}
[add_monoid N]
{f : M →+ N} :
theorem
monoid_hom.mrange_top_of_surjective
{M : Type u_1}
[monoid M]
{N : Type u_2}
[monoid N]
(f : M →* N) :
function.surjective ⇑f → f.mrange = ⊤
The range of a surjective monoid hom is the whole of the codomain.
theorem
add_monoid_hom.mrange_top_of_surjective
{M : Type u_1}
[add_monoid M]
{N : Type u_2}
[add_monoid N]
(f : M →+ N) :
function.surjective ⇑f → f.mrange = ⊤
The range of a surjective add_monoid hom is the whole of the codomain.
theorem
monoid_hom.mrange_eq_map
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N) :
f.mrange = submonoid.map f ⊤
theorem
add_monoid_hom.mrange_eq_map
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N) :
f.mrange = add_submonoid.map f ⊤
theorem
monoid_hom.mclosure_preimage_le
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N)
(s : set N) :
submonoid.closure (⇑f ⁻¹' s) ≤ submonoid.comap f (submonoid.closure s)
theorem
add_monoid_hom.mclosure_preimage_le
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(s : set N) :
theorem
add_monoid_hom.map_mclosure
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(s : set M) :
add_submonoid.map f (add_submonoid.closure s) = add_submonoid.closure (⇑f '' s)
The image under an add_monoid hom of the add_submonoid generated by a set equals
the add_submonoid generated by the image of the set.
theorem
monoid_hom.map_mclosure
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N)
(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.
def
add_monoid_hom.mrestrict
{M : Type u_1}
[add_monoid M]
{N : Type u_2}
[add_monoid N]
(f : M →+ N)
(S : add_submonoid M) :
Restriction of an add_monoid hom to an add_submonoid of the domain.
@[simp]
theorem
add_monoid_hom.mrestrict_apply
{M : Type u_1}
[add_monoid M]
(S : add_submonoid M)
{N : Type u_2}
[add_monoid N]
(f : M →+ N)
(x : ↥S) :
def
monoid_hom.cod_mrestrict
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N]
(f : M →* N)
(S : submonoid N) :
Restriction of a monoid hom to a submonoid of the codomain.
def
add_monoid_hom.cod_mrestrict
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(S : add_submonoid N) :
Restriction of an add_monoid hom to an add_submonoid of the codomain.
def
add_monoid_hom.mrange_restrict
{M : Type u_1}
[add_monoid M]
{N : Type u_2}
[add_monoid N]
(f : M →+ N) :
Restriction of an add_monoid hom to its range interpreted as a submonoid.
Restriction of a monoid hom to its range interpreted as a submonoid.
Equations
- f.mrange_restrict = f.cod_mrestrict f.mrange _
@[simp]
theorem
monoid_hom.coe_mrange_restrict
{M : Type u_1}
[monoid M]
{N : Type u_2}
[monoid N]
(f : M →* N)
(x : M) :
↑(⇑(f.mrange_restrict) x) = ⇑f x
@[simp]
theorem
add_monoid_hom.coe_mrange_restrict
{M : Type u_1}
[add_monoid M]
{N : Type u_2}
[add_monoid N]
(f : M →+ N)
(x : M) :
↑(⇑(f.mrange_restrict) x) = ⇑f x
theorem
add_submonoid.mrange_inl'
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(add_monoid_hom.inl M N).mrange = add_submonoid.comap (add_monoid_hom.snd M N) ⊥
theorem
submonoid.mrange_inl'
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N] :
(monoid_hom.inl M N).mrange = submonoid.comap (monoid_hom.snd M N) ⊥
theorem
submonoid.mrange_inr'
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N] :
(monoid_hom.inr M N).mrange = submonoid.comap (monoid_hom.fst M N) ⊥
theorem
add_submonoid.mrange_inr'
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(add_monoid_hom.inr M N).mrange = add_submonoid.comap (add_monoid_hom.fst M N) ⊥
@[simp]
theorem
submonoid.mrange_fst
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N] :
(monoid_hom.fst M N).mrange = ⊤
@[simp]
theorem
add_submonoid.mrange_fst
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(add_monoid_hom.fst M N).mrange = ⊤
@[simp]
theorem
add_submonoid.mrange_snd
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(add_monoid_hom.snd M N).mrange = ⊤
@[simp]
theorem
submonoid.mrange_snd
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N] :
(monoid_hom.snd M N).mrange = ⊤
@[simp]
theorem
add_submonoid.mrange_inl_sup_mrange_inr
{M : Type u_1}
{N : Type u_2}
[add_monoid M]
[add_monoid N] :
(add_monoid_hom.inl M N).mrange ⊔ (add_monoid_hom.inr M N).mrange = ⊤
@[simp]
theorem
submonoid.mrange_inl_sup_mrange_inr
{M : Type u_1}
{N : Type u_2}
[monoid M]
[monoid N] :
(monoid_hom.inl M N).mrange ⊔ (monoid_hom.inr M N).mrange = ⊤
The add_monoid hom associated to an inclusion of submonoids.
The monoid hom associated to an inclusion of submonoids.
Equations
- submonoid.inclusion h = S.subtype.cod_mrestrict T _
@[simp]
Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.
Equations
- mul_equiv.submonoid_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.