MulHom.map_mclosure
theorem MulHom.map_mclosure :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (s : Set M),
Subsemigroup.map f (Subsemigroup.closure s) = Subsemigroup.closure (⇑f '' s)
The theorem `MulHom.map_mclosure` states that for any two types `M` and `N` that have multiplication (`Mul`) structure, a semigroup homomorphism `f` from `M` to `N`, and a set `s` of elements from `M`, the subsemigroup generated by the image of the set `s` under the homomorphism `f` (i.e., `Subsemigroup.closure (⇑f '' s)`) is equal to the image (under the same homomorphism `f`) of the subsemigroup generated by the set `s` (i.e., `Subsemigroup.map f (Subsemigroup.closure s)`). In other words, the action of a semigroup homomorphism can be interchanged with the operation of taking the subsemigroup generated by a set.
More concisely: For any semigroup homomorphism between types with multiplication structures, the image of the subsemigroup generated by a set under the homomorphism is equal to the subsemigroup generated by the image of the set under the homomorphism.
|
Subsemigroup.gc_map_comap
theorem Subsemigroup.gc_map_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N),
GaloisConnection (Subsemigroup.map f) (Subsemigroup.comap f)
The theorem `Subsemigroup.gc_map_comap` states that for all semigroups `M` and `N` (with respective multiplication operations), and for any semigroup homomorphism `f` from `M` to `N`, there exists a Galois connection between the function that maps subsemigroups of `M` to subsemigroups of `N` via `f`, and the function that returns the preimage of a subsemigroup in `N` along `f` as a subsemigroup of `M`. In other words, a subsemigroup in `M` is mapped to a subsemigroup in `N` under `f` if and only if the preimage of a subsemigroup in `N` under `f` is a subsemigroup in `M`.
More concisely: For every semigroup homomorphism f between semigroups M and N, the functions mapping subsemigroups of M to subsemigroups of N via f and mapping subsemigroups of N back to their preimages in M form a Galois connection.
|
AddSubsemigroup.gc_map_comap
theorem AddSubsemigroup.gc_map_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N),
GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
The theorem `AddSubsemigroup.gc_map_comap` states that for any types `M` and `N` equipped with an additive structure (i.e., instances of `Add M` and `Add N`), and for any additive semigroup homomorphism `f` from `M` to `N`, there exists a Galois connection between the map operation and the co-map operation on additive subsemigroups. In more detail, the map operation `AddSubsemigroup.map f` and the co-map operation `AddSubsemigroup.comap f` form a Galois connection. This means that for any additive subsemigroup `S` of `M` and `T` of `N`, the image of `S` under `f` is a subset of `T` if and only if `S` is a subset of the preimage of `T` under `f`.
More concisely: For any additive semigroup homomorphism `f` between additive types `M` and `N`, the map and co-map operations on additive subsemigroups form a Galois connection.
|
AddHom.srange_top_of_surjective
theorem AddHom.srange_top_of_surjective :
∀ {M : Type u_1} [inst : Add M] {N : Type u_5} [inst_1 : Add N] (f : AddHom M N),
Function.Surjective ⇑f → f.srange = ⊤
The theorem `AddHom.srange_top_of_surjective` states that for any two types `M` and `N` that have addition defined on them, if a function `f` from `M` to `N` is a surjective Additive Semigroup homomorphism (an `AddHom`), then the range (set of all possible output values) of `f` is equal to the entire codomain `N`. In other words, every element in `N` can be expressed as the sum of elements in `M` using the function `f`.
More concisely: If `f` is a surjective Additive Semigroup homomorphism from type `M` to type `N`, then the range of `f` equals `N`.
|
MulHom.srange_top_of_surjective
theorem MulHom.srange_top_of_surjective :
∀ {M : Type u_1} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] (f : M →ₙ* N),
Function.Surjective ⇑f → f.srange = ⊤
This theorem states that for any given surjective semigroup homomorphism `f` from a semigroup `M` to a semigroup `N`, the range of `f` covers the entire codomain. In other words, if `f` is a function from `M` to `N` that respects the multiplication operation (i.e., a semigroup homomorphism) and if every element in `N` comes from applying `f` to some element in `M` (i.e., `f` is surjective), then the set of all possible outputs of `f` (the range of `f`) is exactly the whole set `N` (denoted as `⊤`).
More concisely: If `f` is a surjective semigroup homomorphism from semigroup `M` to semigroup `N`, then the range of `f` equals the entire codomain `N`.
|
Mathlib.GroupTheory.Subsemigroup.Operations._auxLemma.2
theorem Mathlib.GroupTheory.Subsemigroup.Operations._auxLemma.2 :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M},
(x ∈ AddSubsemigroup.comap f S) = (f x ∈ S)
The theorem `Mathlib.GroupTheory.Subsemigroup.Operations._auxLemma.2` states that for any types `M` and `N` with addition (`Add M` and `Add N`), a given `AddSubsemigroup` `S` of `N`, and an additive homomorphism `f` from `M` to `N`, an element `x` of `M` is in the preimage of `S` under `f` (i.e., `x` belongs to `AddSubsemigroup.comap f S`) if and only if `f(x)` is in `S`. In other words, it connects the membership of an element in the preimage of a subsemigroup with the mapping of that element into the subsemigroup by the homomorphism.
More concisely: For any additive homomorphism from an additive semigroup to another, an element is in the preimage of a subsemigroup if and only if its image under the homomorphism is in the subsemigroup.
|
Mathlib.GroupTheory.Subsemigroup.Operations._auxLemma.1
theorem Mathlib.GroupTheory.Subsemigroup.Operations._auxLemma.1 :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M →ₙ* N} {x : M},
(x ∈ Subsemigroup.comap f S) = (f x ∈ S)
This theorem states that for all types `M` and `N` with multiplication operations (`Mul M` and `Mul N` respectively), a subsemigroup `S` of `N`, and a semigroup homomorphism `f` from `M` to `N`, an element `x` from `M` is in the preimage of `S` under `f` (i.e., `x` is in `Subsemigroup.comap f S`) if and only if the image of `x` under `f` (i.e., `f x`) is in `S`. In other words, membership in the preimage subsemigroup defined by `f` and `S` corresponds exactly to membership in `S` under the mapping `f`.
More concisely: For any semigroup homomorphism $f$ from type `M` to type `N` and any subsemigroup `S` of `N`, an element `x` from `M` is in the preimage of `S` under `f` if and only if $f(x) \in S$.
|
AddHom.map_mclosure
theorem AddHom.map_mclosure :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) (s : Set M),
AddSubsemigroup.map f (AddSubsemigroup.closure s) = AddSubsemigroup.closure (⇑f '' s)
The theorem `AddHom.map_mclosure` states that for any set `s` of elements in an additive semigroup `M` and a homomorphism `f` from `M` to another additive semigroup `N`, the additive subsemigroup generated by applying `f` to the subsemigroup generated by `s` (i.e., the image of the additive subsemigroup generated by `s` under the homomorphism `f`) is equal to the additive subsemigroup generated by the image of the set `s` under the homomorphism `f`. In other words, mapping an additive subsemigroup to another additive semigroup through a homomorphism preserves the structure of subsemigroup generated by a set.
More concisely: For any set `s` in an additive semigroup `M` and a homomorphism `f` from `M` to an additive semigroup `N`, the image of the additive subsemigroup generated by `s` under `f` equals the additive subsemigroup generated by the image of `s` under `f`.
|