Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes HΓΆlzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
Amelia Livingston, Yury Kudryashov, Yakov Pechersky, Jireh Loreaux

! This file was ported from Lean 3 source module group_theory.subsemigroup.operations
! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Subsemigroup.Basic
import Mathlib.Algebra.Group.Prod
import Mathlib.Algebra.Group.TypeTags

/-!
# Operations on `Subsemigroup`s

In this file we define various operations on `Subsemigroup`s and `MulHom`s.

## Main definitions

### Conversion between multiplicative and additive definitions

convert between multiplicative and additive subsemigroups of `M`,
`Multiplicative M`, and `Additive M`. These are stated as `OrderIso`s.

### (Commutative) semigroup structure on a subsemigroup

* `Subsemigroup.toSemigroup`, `Subsemigroup.toCommSemigroup`: a subsemigroup inherits a
(commutative) semigroup structure.

### Operations on subsemigroups

* `Subsemigroup.comap`: preimage of a subsemigroup under a semigroup homomorphism as a subsemigroup
of the domain;
* `Subsemigroup.map`: image of a subsemigroup under a semigroup homomorphism as a subsemigroup of
the codomain;
* `Subsemigroup.prod`: product of two subsemigroups `s : Subsemigroup M` and `t : Subsemigroup N`
as a subsemigroup of `M Γ N`;

### Semigroup homomorphisms between subsemigroups

* `Subsemigroup.subtype`: embedding of a subsemigroup into the ambient semigroup.
* `Subsemigroup.inclusion`: given two subsemigroups `S`, `T` such that `S β€ T`, `S.inclusion T` is
the inclusion of `S` into `T` as a semigroup homomorphism;
* `MulEquiv.subsemigroupCongr`: converts a proof of `S = T` into a semigroup isomorphism between
`S` and `T`.
* `Subsemigroup.prodEquiv`: semigroup isomorphism between `s.prod t` and `s Γ t`;

### Operations on `MulHom`s

* `MulHom.srange`: range of a semigroup homomorphism as a subsemigroup of the codomain;
* `MulHom.restrict`: restrict a semigroup homomorphism to a subsemigroup;
* `MulHom.codRestrict`: restrict the codomain of a semigroup homomorphism to a subsemigroup;
* `MulHom.srangeRestrict`: restrict a semigroup homomorphism to its range;

### Implementation notes

This file follows closely `GroupTheory/Submonoid/Operations.lean`, omitting only that which is
necessary.

## Tags

subsemigroup, range, product, map, comap
-/

variable {M: Type ?u.14M N: Type ?u.5N P: Type ?u.33445P Ο: Type ?u.33448Ο : Type _: Type (?u.11+1)Type _}

/-!
-/

section

variable [Mul: Type ?u.26 β Type ?u.26Mul M: Type ?u.14M]

/-- Subsemigroups of semigroup `M` are isomorphic to additive subsemigroups of `Additive M`. -/
@[simps: β {M : Type u_1} [inst : Mul M] (S : AddSubsemigroup (Additive M)),
def Subsemigroup.toAddSubsemigroup: {M : Type u_1} β [inst : Mul M] β Subsemigroup M βo AddSubsemigroup (Additive M)Subsemigroup.toAddSubsemigroup : Subsemigroup: (M : Type ?u.46) β [inst : Mul M] β Type ?u.46Subsemigroup M: Type ?u.29M βo AddSubsemigroup: (M : Type ?u.54) β [inst : Add M] β Type ?u.54AddSubsemigroup (Additive: Type ?u.55 β Type ?u.55Additive M: Type ?u.29M) where
toFun S: ?m.166S :=
add_mem' := S: ?m.166S.mul_mem': β {M : Type ?u.349} [inst : Mul M] (self : Subsemigroup M) {a b : M},
a β self.carrier β b β self.carrier β a * b β self.carriermul_mem' }
invFun S: ?m.393S :=
mul_mem' := S: ?m.393S.add_mem': β {M : Type ?u.548} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
a β self.carrier β b β self.carrier β a + b β self.carrieradd_mem' }
left_inv _: ?m.578_ := rfl: β {Ξ± : Sort ?u.580} {a : Ξ±}, a = arfl
right_inv _: ?m.598_ := rfl: β {Ξ± : Sort ?u.600} {a : Ξ±}, a = arfl
map_rel_iff':= Iff.rfl: β {a : Prop}, a β aIff.rfl

of `M`. -/
abbrev AddSubsemigroup.toSubsemigroup': {M : Type u_1} β [inst : Mul M] β AddSubsemigroup (Additive M) βo Subsemigroup MAddSubsemigroup.toSubsemigroup' : AddSubsemigroup: (M : Type ?u.882) β [inst : Add M] β Type ?u.882AddSubsemigroup (Additive: Type ?u.883 β Type ?u.883Additive M: Type ?u.865M) βo Subsemigroup: (M : Type ?u.900) β [inst : Mul M] β Type ?u.900Subsemigroup M: Type ?u.865M :=
Subsemigroup.toAddSubsemigroup: {M : Type ?u.973} β [inst : Mul M] β Subsemigroup M βo AddSubsemigroup (Additive M)Subsemigroup.toAddSubsemigroup.symm: {Ξ± : Type ?u.997} β {Ξ² : Type ?u.996} β [inst : LE Ξ±] β [inst_1 : LE Ξ²] β Ξ± βo Ξ² β Ξ² βo Ξ±symm

theorem Subsemigroup.toAddSubsemigroup_closure: β (S : Set M), βtoAddSubsemigroup (closure S) = AddSubsemigroup.closure (βAdditive.toMul β»ΒΉ' S)Subsemigroup.toAddSubsemigroup_closure (S: Set MS : Set: Type ?u.1175 β Type ?u.1175Set M: Type ?u.1160M) :
Subsemigroup.toAddSubsemigroup: {M : Type ?u.1179} β [inst : Mul M] β Subsemigroup M βo AddSubsemigroup (Additive M)Subsemigroup.toAddSubsemigroup (Subsemigroup.closure: {M : Type ?u.1262} β [inst : Mul M] β Set M β Subsemigroup MSubsemigroup.closure S: Set MS) =
le_antisymm: β {Ξ± : Type ?u.1409} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm
(Subsemigroup.toAddSubsemigroup: {M : Type ?u.1438} β [inst : Mul M] β Subsemigroup M βo AddSubsemigroup (Additive M)Subsemigroup.toAddSubsemigroup.le_symm_apply: β {Ξ± : Type ?u.1461} {Ξ² : Type ?u.1462} [inst : LE Ξ±] [inst_1 : LE Ξ²] (e : Ξ± βo Ξ²) {x : Ξ±} {y : Ξ²},
x β€ β(OrderIso.symm e) y β βe x β€ yle_symm_apply.1: β {a b : Prop}, (a β b) β a β b1 <|
Subsemigroup.closure_le: β {M : Type ?u.1621} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s β€ S β s β βSSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 (AddSubsemigroup.subset_closure: β {M : Type ?u.1661} [inst : Add M] {s : Set M}, s β β(AddSubsemigroup.closure s)AddSubsemigroup.subset_closure (M := Additive: Type ?u.1662 β Type ?u.1662Additive M: Type ?u.1160M)))
(AddSubsemigroup.closure_le: β {M : Type ?u.1722} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s β€ S β s β βSAddSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 (Subsemigroup.subset_closure: β {M : Type ?u.1758} [inst : Mul M] {s : Set M}, s β β(closure s)Subsemigroup.subset_closure (M := M: Type ?u.1160M)))
#align subsemigroup.to_add_subsemigroup_closure Subsemigroup.toAddSubsemigroup_closure: β {M : Type u_1} [inst : Mul M] (S : Set M),

theorem AddSubsemigroup.toSubsemigroup'_closure: β {M : Type u_1} [inst : Mul M] (S : Set (Additive M)),
βtoSubsemigroup' (closure S) = Subsemigroup.closure (βMultiplicative.ofAdd β»ΒΉ' S)AddSubsemigroup.toSubsemigroup'_closure (S: Set (Additive M)S : Set: Type ?u.1813 β Type ?u.1813Set (Additive: Type ?u.1814 β Type ?u.1814Additive M: Type ?u.1798M)) :
Subsemigroup.closure: {M : Type ?u.1950} β [inst : Mul M] β Set M β Subsemigroup MSubsemigroup.closure (Multiplicative.ofAdd: {Ξ± : Type ?u.1959} β Ξ± β Multiplicative Ξ±Multiplicative.ofAdd β»ΒΉ' S: Set (Additive M)S) :=
le_antisymm: β {Ξ± : Type ?u.2047} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm
(AddSubsemigroup.toSubsemigroup': {M : Type ?u.2076} β [inst : Mul M] β AddSubsemigroup (Additive M) βo Subsemigroup MAddSubsemigroup.toSubsemigroup'.le_symm_apply: β {Ξ± : Type ?u.2099} {Ξ² : Type ?u.2100} [inst : LE Ξ±] [inst_1 : LE Ξ²] (e : Ξ± βo Ξ²) {x : Ξ±} {y : Ξ²},
x β€ β(OrderIso.symm e) y β βe x β€ yle_symm_apply.1: β {a b : Prop}, (a β b) β a β b1 <|
AddSubsemigroup.closure_le: β {M : Type ?u.2258} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, closure s β€ S β s β βSAddSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 (Subsemigroup.subset_closure: β {M : Type ?u.2296} [inst : Mul M] {s : Set M}, s β β(Subsemigroup.closure s)Subsemigroup.subset_closure (M := M: Type ?u.1798M)))
(Subsemigroup.closure_le: β {M : Type ?u.2349} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s β€ S β s β βSSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 \$ AddSubsemigroup.subset_closure: β {M : Type ?u.2388} [inst : Add M] {s : Set M}, s β β(closure s)AddSubsemigroup.subset_closure (M := Additive: Type ?u.2389 β Type ?u.2389Additive M: Type ?u.1798M))
#align add_subsemigroup.to_subsemigroup'_closure AddSubsemigroup.toSubsemigroup'_closure: β {M : Type u_1} [inst : Mul M] (S : Set (Additive M)),

end

section

variable {A: Type ?u.2448A : Type _: Type (?u.2448+1)Type _} [Add: Type ?u.3537 β Type ?u.3537Add A: Type ?u.2448A]

multiplicative subsemigroups of `Multiplicative A`. -/
@[simps: β {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)),
β(β(RelIso.symm toSubsemigroup) S) = βMultiplicative.ofAdd β»ΒΉ' βSsimps]
def AddSubsemigroup.toSubsemigroup: {A : Type u_1} β [inst : Add A] β AddSubsemigroup A βo Subsemigroup (Multiplicative A)AddSubsemigroup.toSubsemigroup : AddSubsemigroup: (M : Type ?u.2474) β [inst : Add M] β Type ?u.2474AddSubsemigroup A: Type ?u.2466A βo Subsemigroup: (M : Type ?u.2481) β [inst : Mul M] β Type ?u.2481Subsemigroup (Multiplicative: Type ?u.2482 β Type ?u.2482Multiplicative A: Type ?u.2466A) where
toFun S: ?m.2593S :=
{ carrier := Multiplicative.toAdd: {Ξ± : Type ?u.2606} β Multiplicative Ξ± β Ξ±Multiplicative.toAdd β»ΒΉ' S: ?m.2593S
mul_mem' := S: ?m.2593S.add_mem': β {M : Type ?u.2776} [inst : Add M] (self : AddSubsemigroup M) {a b : M},
a β self.carrier β b β self.carrier β a + b β self.carrieradd_mem' }
invFun S: ?m.2820S :=
{ carrier := Multiplicative.ofAdd: {Ξ± : Type ?u.2830} β Ξ± β Multiplicative Ξ±Multiplicative.ofAdd β»ΒΉ' S: ?m.2820S
add_mem' := S: ?m.2820S.mul_mem': β {M : Type ?u.2975} [inst : Mul M] (self : Subsemigroup M) {a b : M},
a β self.carrier β b β self.carrier β a * b β self.carriermul_mem' }
left_inv _: ?m.3005_ := rfl: β {Ξ± : Sort ?u.3007} {a : Ξ±}, a = arfl
right_inv _: ?m.3025_ := rfl: β {Ξ± : Sort ?u.3027} {a : Ξ±}, a = arfl
map_rel_iff' := Iff.rfl: β {a : Prop}, a β aIff.rfl
#align add_subsemigroup.to_subsemigroup_symm_apply_coe AddSubsemigroup.toSubsemigroup_symm_apply_coe: β {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)),

/-- Subsemigroups of a semigroup `Multiplicative A` are isomorphic to additive subsemigroups
of `A`. -/
abbrev Subsemigroup.toAddSubsemigroup': {A : Type u_1} β [inst : Add A] β Subsemigroup (Multiplicative A) βo AddSubsemigroup ASubsemigroup.toAddSubsemigroup' : Subsemigroup: (M : Type ?u.3276) β [inst : Mul M] β Type ?u.3276Subsemigroup (Multiplicative: Type ?u.3277 β Type ?u.3277Multiplicative A: Type ?u.3268A) βo AddSubsemigroup: (M : Type ?u.3294) β [inst : Add M] β Type ?u.3294AddSubsemigroup A: Type ?u.3268A :=
AddSubsemigroup.toSubsemigroup: {A : Type ?u.3366} β [inst : Add A] β AddSubsemigroup A βo Subsemigroup (Multiplicative A)AddSubsemigroup.toSubsemigroup.symm: {Ξ± : Type ?u.3387} β {Ξ² : Type ?u.3386} β [inst : LE Ξ±] β [inst_1 : LE Ξ²] β Ξ± βo Ξ² β Ξ² βo Ξ±symm

theorem AddSubsemigroup.toSubsemigroup_closure: β {A : Type u_1} [inst : Add A] (S : Set A),
βtoSubsemigroup (closure S) = Subsemigroup.closure (βMultiplicative.toAdd β»ΒΉ' S)AddSubsemigroup.toSubsemigroup_closure (S: Set AS : Set: Type ?u.3540 β Type ?u.3540Set A: Type ?u.3534A) :
Subsemigroup.closure: {M : Type ?u.3657} β [inst : Mul M] β Set M β Subsemigroup MSubsemigroup.closure (Multiplicative.toAdd: {Ξ± : Type ?u.3666} β Multiplicative Ξ± β Ξ±Multiplicative.toAdd β»ΒΉ' S: Set AS) :=
le_antisymm: β {Ξ± : Type ?u.3767} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm
(AddSubsemigroup.toSubsemigroup: {A : Type ?u.3796} β [inst : Add A] β AddSubsemigroup A βo Subsemigroup (Multiplicative A)AddSubsemigroup.toSubsemigroup.to_galoisConnection: β {Ξ± : Type ?u.3817} {Ξ² : Type ?u.3816} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] (oi : Ξ± βo Ξ²),
GaloisConnection βoi β(OrderIso.symm oi)to_galoisConnection.l_le: β {Ξ± : Type ?u.3894} {Ξ² : Type ?u.3893} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β {a : Ξ±} {b : Ξ²}, a β€ u b β l a β€ bl_le <|
AddSubsemigroup.closure_le: β {M : Type ?u.3996} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, closure s β€ S β s β βSAddSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 \$ Subsemigroup.subset_closure: β {M : Type ?u.4035} [inst : Mul M] {s : Set M}, s β β(Subsemigroup.closure s)Subsemigroup.subset_closure (M := Multiplicative: Type ?u.4036 β Type ?u.4036Multiplicative A: Type ?u.3534A))
(Subsemigroup.closure_le: β {M : Type ?u.4096} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s β€ S β s β βSSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 \$ AddSubsemigroup.subset_closure: β {M : Type ?u.4135} [inst : Add M] {s : Set M}, s β β(closure s)AddSubsemigroup.subset_closure (M := A: Type ?u.3534A))

theorem Subsemigroup.toAddSubsemigroup'_closure: β {A : Type u_1} [inst : Add A] (S : Set (Multiplicative A)),
βtoAddSubsemigroup' (closure S) = AddSubsemigroup.closure (βAdditive.ofMul β»ΒΉ' S)Subsemigroup.toAddSubsemigroup'_closure (S: Set (Multiplicative A)S : Set: Type ?u.4192 β Type ?u.4192Set (Multiplicative: Type ?u.4193 β Type ?u.4193Multiplicative A: Type ?u.4186A)) :
Subsemigroup.toAddSubsemigroup': {A : Type ?u.4197} β [inst : Add A] β Subsemigroup (Multiplicative A) βo AddSubsemigroup ASubsemigroup.toAddSubsemigroup' (Subsemigroup.closure: {M : Type ?u.4277} β [inst : Mul M] β Set M β Subsemigroup MSubsemigroup.closure S: Set (Multiplicative A)S) =
le_antisymm: β {Ξ± : Type ?u.4425} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β b β€ a β a = ble_antisymm
(Subsemigroup.toAddSubsemigroup': {A : Type ?u.4454} β [inst : Add A] β Subsemigroup (Multiplicative A) βo AddSubsemigroup ASubsemigroup.toAddSubsemigroup'.to_galoisConnection: β {Ξ± : Type ?u.4475} {Ξ² : Type ?u.4474} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] (oi : Ξ± βo Ξ²),
GaloisConnection βoi β(OrderIso.symm oi)to_galoisConnection.l_le: β {Ξ± : Type ?u.4552} {Ξ² : Type ?u.4551} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β {a : Ξ±} {b : Ξ²}, a β€ u b β l a β€ bl_le <|
Subsemigroup.closure_le: β {M : Type ?u.4653} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s β€ S β s β βSSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 \$ AddSubsemigroup.subset_closure: β {M : Type ?u.4696} [inst : Add M] {s : Set M}, s β β(AddSubsemigroup.closure s)AddSubsemigroup.subset_closure (M := A: Type ?u.4186A))
(AddSubsemigroup.closure_le: β {M : Type ?u.4748} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s β€ S β s β βSAddSubsemigroup.closure_le.2: β {a b : Prop}, (a β b) β b β a2 \$ Subsemigroup.subset_closure: β {M : Type ?u.4784} [inst : Mul M] {s : Set M}, s β β(closure s)Subsemigroup.subset_closure (M := Multiplicative: Type ?u.4785 β Type ?u.4785Multiplicative A: Type ?u.4186A))
#align subsemigroup.to_add_subsemigroup'_closure Subsemigroup.toAddSubsemigroup'_closure: β {A : Type u_1} [inst : Add A] (S : Set (Multiplicative A)),

end

namespace Subsemigroup

open Set

/-!
### `comap` and `map`
-/

variable [Mul: Type ?u.15418 β Type ?u.15418Mul M: Type ?u.18022M] [Mul: Type ?u.13393 β Type ?u.13393Mul N: Type ?u.4835N] [Mul: Type ?u.13396 β Type ?u.13396Mul P: Type ?u.7231P] (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.16858) β [inst : Mul M] β Type ?u.16858Subsemigroup M: Type ?u.4832M)

/-- The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/
def comap: {M : Type u_1} β {N : Type u_2} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap (f: M ββ* Nf : M: Type ?u.4863M ββ* N: Type ?u.4866N) (S: Subsemigroup NS : Subsemigroup: (M : Type ?u.4912) β [inst : Mul M] β Type ?u.4912Subsemigroup N: Type ?u.4866N) :
Subsemigroup: (M : Type ?u.4916) β [inst : Mul M] β Type ?u.4916Subsemigroup M: Type ?u.4863M where
carrier := f: M ββ* Nf β»ΒΉ' S: Subsemigroup NS
mul_mem' ha: ?m.5248ha hb: ?m.5251hb := show f: M ββ* Nf (_: ?m.5475_ * _: ?m.5478_) β S: Subsemigroup NS by rw [M: Type ?u.4863N: Type ?u.4866P: Type ?u.4869Ο: Type ?u.4872instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Naβ, bβ: Mha: aβ β βf β»ΒΉ' βShb: bβ β βf β»ΒΉ' βSβf (aβ * bβ) β Smap_mul: β {M : Type ?u.5584} {N : Type ?u.5585} {F : Type ?u.5583} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
(f : F) (x y : M), βf (x * y) = βf x * βf ymap_mulM: Type ?u.4863N: Type ?u.4866P: Type ?u.4869Ο: Type ?u.4872instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Naβ, bβ: Mha: aβ β βf β»ΒΉ' βShb: bβ β βf β»ΒΉ' βSβf aβ * βf bβ β S]M: Type ?u.4863N: Type ?u.4866P: Type ?u.4869Ο: Type ?u.4872instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Naβ, bβ: Mha: aβ β βf β»ΒΉ' βShb: bβ β βf β»ΒΉ' βSβf aβ * βf bβ β S;M: Type ?u.4863N: Type ?u.4866P: Type ?u.4869Ο: Type ?u.4872instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Naβ, bβ: Mha: aβ β βf β»ΒΉ' βShb: bβ β βf β»ΒΉ' βSβf aβ * βf bβ β S M: Type ?u.4863N: Type ?u.4866P: Type ?u.4869Ο: Type ?u.4872instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Naβ, bβ: Mha: aβ β βf β»ΒΉ' βShb: bβ β βf β»ΒΉ' βSβf (aβ * bβ) β Sexact mul_mem: β {S : Type ?u.5803} {M : Type ?u.5802} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S}
{a b : M}, a β s β b β s β a * b β smul_mem ha: aβ β βf β»ΒΉ' βSha hb: bβ β βf β»ΒΉ' βShbGoals accomplished! π
#align subsemigroup.comap Subsemigroup.comap: {M : Type u_1} β {N : Type u_2} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup MSubsemigroup.comap

theorem coe_comap: β (S : Subsemigroup N) (f : M ββ* N), β(comap f S) = βf β»ΒΉ' βScoe_comap (S: Subsemigroup NS : Subsemigroup: (M : Type ?u.6112) β [inst : Mul M] β Type ?u.6112Subsemigroup N: Type ?u.6084N) (f: M ββ* Nf : M: Type ?u.6081M ββ* N: Type ?u.6084N) : (S: Subsemigroup NS.comap: {M : Type ?u.6138} β
{N : Type ?u.6137} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf : Set: Type ?u.6136 β Type ?u.6136Set M: Type ?u.6081M) = f: M ββ* Nf β»ΒΉ' S: Subsemigroup NS :=
rfl: β {Ξ± : Sort ?u.6616} {a : Ξ±}, a = arfl
#align subsemigroup.coe_comap Subsemigroup.coe_comap: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup N) (f : M ββ* N),
β(comap f S) = βf β»ΒΉ' βSSubsemigroup.coe_comap

@[to_additive: β {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M},
x β AddSubsemigroup.comap f S β βf x β Sto_additive (attr := simp)]
theorem mem_comap: β {S : Subsemigroup N} {f : M ββ* N} {x : M}, x β comap f S β βf x β Smem_comap {S: Subsemigroup NS : Subsemigroup: (M : Type ?u.6736) β [inst : Mul M] β Type ?u.6736Subsemigroup N: Type ?u.6708N} {f: M ββ* Nf : M: Type ?u.6705M ββ* N: Type ?u.6708N} {x: Mx : M: Type ?u.6705M} : x: Mx β S: Subsemigroup NS.comap: {M : Type ?u.6766} β
{N : Type ?u.6765} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf β f: M ββ* Nf x: Mx β S: Subsemigroup NS :=
Iff.rfl: β {a : Prop}, a β aIff.rfl
#align subsemigroup.mem_comap Subsemigroup.mem_comap: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M ββ* N} {x : M},
x β comap f S β βf x β SSubsemigroup.mem_comap

@[to_additive: β {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (S : AddSubsemigroup P)
theorem comap_comap: β {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup P)
(g : N ββ* P) (f : M ββ* N), comap f (comap g S) = comap (MulHom.comp g f) Scomap_comap (S: Subsemigroup PS : Subsemigroup: (M : Type ?u.7256) β [inst : Mul M] β Type ?u.7256Subsemigroup P: Type ?u.7231P) (g: N ββ* Pg : N: Type ?u.7228N ββ* P: Type ?u.7231P) (f: M ββ* Nf : M: Type ?u.7225M ββ* N: Type ?u.7228N) :
(S: Subsemigroup PS.comap: {M : Type ?u.7292} β
{N : Type ?u.7291} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap g: N ββ* Pg).comap: {M : Type ?u.7314} β
{N : Type ?u.7313} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup PS.comap: {M : Type ?u.7336} β
{N : Type ?u.7335} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap (g: N ββ* Pg.comp: {M : Type ?u.7349} β
{N : Type ?u.7348} β
{P : Type ?u.7347} β [inst : Mul M] β [inst_1 : Mul N] β [inst_2 : Mul P] β (N ββ* P) β (M ββ* N) β M ββ* Pcomp f: M ββ* Nf) :=
rfl: β {Ξ± : Sort ?u.7404} {a : Ξ±}, a = arfl
#align subsemigroup.comap_comap Subsemigroup.comap_comap: β {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup P)
(g : N ββ* P) (f : M ββ* N), comap f (comap g S) = comap (MulHom.comp g f) SSubsemigroup.comap_comap

theorem comap_id: β {P : Type u_1} [inst : Mul P] (S : Subsemigroup P), comap (MulHom.id P) S = Scomap_id (S: Subsemigroup PS : Subsemigroup: (M : Type ?u.7545) β [inst : Mul M] β Type ?u.7545Subsemigroup P: Type ?u.7520P) : S: Subsemigroup PS.comap: {M : Type ?u.7557} β
{N : Type ?u.7556} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap (MulHom.id: (M : Type ?u.7568) β [inst : Mul M] β M ββ* MMulHom.id _: Type ?u.7568_) = S: Subsemigroup PS :=
ext: β {M : Type ?u.7624} [inst : Mul M] {S T : Subsemigroup M}, (β (x : M), x β S β x β T) β S = Text (byGoals accomplished! π M: Type ?u.7514N: Type ?u.7517P: Type u_1Ο: Type ?u.7523instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup MS: Subsemigroup Pβ (x : P), x β comap (MulHom.id P) S β x β SsimpGoals accomplished! π)
#align subsemigroup.comap_id Subsemigroup.comap_id: β {P : Type u_1} [inst : Mul P] (S : Subsemigroup P), comap (MulHom.id P) S = SSubsemigroup.comap_id

/-- The image of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/
def map: {M : Type u_1} β {N : Type u_2} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap (f: M ββ* Nf : M: Type ?u.8706M ββ* N: Type ?u.8709N) (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.8755) β [inst : Mul M] β Type ?u.8755Subsemigroup M: Type ?u.8706M) : Subsemigroup: (M : Type ?u.8759) β [inst : Mul M] β Type ?u.8759Subsemigroup N: Type ?u.8709N where
carrier := f: M ββ* Nf '' S: Subsemigroup MS
mul_mem' := byGoals accomplished! π
M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mβ {a b : N}, a β βf '' βS β b β βf '' βS β a * b β βf '' βSrintro _: N_ _: N_ β¨x, hx, rflβ©: aβΒΉ β βf '' βSβ¨x: Mxβ¨x, hx, rflβ©: aβΒΉ β βf '' βS, hx: x β βShxβ¨x, hx, rflβ©: aβΒΉ β βf '' βS, rfl: βf x = aβrflβ¨x, hx, rflβ©: aβΒΉ β βf '' βSβ© β¨y, hy, rflβ©: y β βS β§ βf y = bββ¨y: Myβ¨y, hy, rflβ©: y β βS β§ βf y = bβ, hy: y β βShyβ¨y, hy, rflβ©: y β βS β§ βf y = bβ, rfl: βf y = bβrflβ¨y, hy, rflβ©: y β βS β§ βf y = bββ©M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mx: Mhx: x β βSy: Mhy: y β βSintro.intro.intro.introβf x * βf y β βf '' βS
M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mβ {a b : N}, a β βf '' βS β b β βf '' βS β a * b β βf '' βSexact β¨x: Mx * y: My, @mul_mem: β {S : Type ?u.9263} {M : Type ?u.9262} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S}
{a b : M}, a β s β b β s β a * b β smul_mem (Subsemigroup: (M : Type ?u.9264) β [inst : Mul M] β Type ?u.9264Subsemigroup M: Type ?u.8706M) M: Type ?u.8706M _ _ _ _: Subsemigroup M_ _: M_ _: M_ hx: x β βShx hy: y β βShy, M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mx: Mhx: x β βSy: Mhy: y β βSintro.intro.intro.introβf x * βf y β βf '' βSbyGoals accomplished! π M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mx: Mhx: x β βSy: Mhy: y β βSβf (x * y) = βf x * βf yrw [M: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mx: Mhx: x β βSy: Mhy: y β βSβf (x * y) = βf x * βf ymap_mul: β {M : Type ?u.9314} {N : Type ?u.9315} {F : Type ?u.9313} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
(f : F) (x y : M), βf (x * y) = βf x * βf ymap_mulM: Type ?u.8706N: Type ?u.8709P: Type ?u.8712Ο: Type ?u.8715instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup Mf: M ββ* NS: Subsemigroup Mx: Mhx: x β βSy: Mhy: y β βSβf x * βf y = βf x * βf y]Goals accomplished! πβ©Goals accomplished! π
#align subsemigroup.map Subsemigroup.map: {M : Type u_1} β {N : Type u_2} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup NSubsemigroup.map

theorem coe_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) (S : Subsemigroup M),
β(map f S) = βf '' βScoe_map (f: M ββ* Nf : M: Type ?u.9768M ββ* N: Type ?u.9771N) (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.9817) β [inst : Mul M] β Type ?u.9817Subsemigroup M: Type ?u.9768M) : (S: Subsemigroup MS.map: {M : Type ?u.9825} β
{N : Type ?u.9824} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf : Set: Type ?u.9823 β Type ?u.9823Set N: Type ?u.9771N) = f: M ββ* Nf '' S: Subsemigroup MS :=
rfl: β {Ξ± : Sort ?u.10303} {a : Ξ±}, a = arfl
#align subsemigroup.coe_map Subsemigroup.coe_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) (S : Subsemigroup M),
β(map f S) = βf '' βSSubsemigroup.coe_map

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {y : N},
y β AddSubsemigroup.map f S β β x, x β S β§ βf x = yto_additive (attr := simp)]
theorem mem_map: β {f : M ββ* N} {S : Subsemigroup M} {y : N}, y β map f S β β x, x β S β§ βf x = ymem_map {f: M ββ* Nf : M: Type ?u.10392M ββ* N: Type ?u.10395N} {S: Subsemigroup MS : Subsemigroup: (M : Type ?u.10441) β [inst : Mul M] β Type ?u.10441Subsemigroup M: Type ?u.10392M} {y: Ny : N: Type ?u.10395N} : y: Ny β S: Subsemigroup MS.map: {M : Type ?u.10453} β
{N : Type ?u.10452} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β β x: ?m.10540x β S: Subsemigroup MS, f: M ββ* Nf x: ?m.10540x = y: Ny :=
mem_image: β {Ξ± : Type ?u.10800} {Ξ² : Type ?u.10801} (f : Ξ± β Ξ²) (s : Set Ξ±) (y : Ξ²), y β f '' s β β x, x β s β§ f x = ymem_image _: ?m.10802 β ?m.10803_ _: Set ?m.10802_ _: ?m.10803_
#align subsemigroup.mem_map Subsemigroup.mem_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N} {S : Subsemigroup M} {y : N},
y β map f S β β x, x β S β§ βf x = ySubsemigroup.mem_map
y β AddSubsemigroup.map f S β β x, x β S β§ βf x = yAddSubsemigroup.mem_map

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) {S : AddSubsemigroup M} {x : M},
theorem mem_map_of_mem: β (f : M ββ* N) {S : Subsemigroup M} {x : M}, x β S β βf x β map f Smem_map_of_mem (f: M ββ* Nf : M: Type ?u.10966M ββ* N: Type ?u.10969N) {S: Subsemigroup MS : Subsemigroup: (M : Type ?u.11015) β [inst : Mul M] β Type ?u.11015Subsemigroup M: Type ?u.10966M} {x: Mx : M: Type ?u.10966M} (hx: x β Shx : x: Mx β S: Subsemigroup MS) : f: M ββ* Nf x: Mx β S: Subsemigroup MS.map: {M : Type ?u.11306} β
{N : Type ?u.11305} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf :=
mem_image_of_mem: β {Ξ± : Type ?u.11392} {Ξ² : Type ?u.11393} (f : Ξ± β Ξ²) {x : Ξ±} {a : Set Ξ±}, x β a β f x β f '' amem_image_of_mem f: M ββ* Nf hx: x β Shx
#align subsemigroup.mem_map_of_mem Subsemigroup.mem_map_of_mem: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) {S : Subsemigroup M} {x : M},
x β S β βf x β map f SSubsemigroup.mem_map_of_mem

(x : { x // x β S }), βf βx β AddSubsemigroup.map f Sto_additive]
theorem apply_coe_mem_map: β (f : M ββ* N) (S : Subsemigroup M) (x : { x // x β S }), βf βx β map f Sapply_coe_mem_map (f: M ββ* Nf : M: Type ?u.11705M ββ* N: Type ?u.11708N) (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.11754) β [inst : Mul M] β Type ?u.11754Subsemigroup M: Type ?u.11705M) (x: { x // x β S }x : S: Subsemigroup MS) : f: M ββ* Nf x: { x // x β S }x β S: Subsemigroup MS.map: {M : Type ?u.12142} β
{N : Type ?u.12141} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf :=
mem_map_of_mem: β {M : Type ?u.12228} {N : Type ?u.12229} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) {S : Subsemigroup M} {x : M},
x β S β βf x β map f Smem_map_of_mem f: M ββ* Nf x: { x // x β S }x.prop: β {Ξ± : Sort ?u.12277} {p : Ξ± β Prop} (x : Subtype p), p βxprop
#align subsemigroup.apply_coe_mem_map Subsemigroup.apply_coe_mem_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) (S : Subsemigroup M) (x : { x // x β S }),
βf βx β map f SSubsemigroup.apply_coe_mem_map
(x : { x // x β S }), βf βx β AddSubsemigroup.map f SAddSubsemigroup.apply_coe_mem_map

@[to_additive: β {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (S : AddSubsemigroup M)
theorem map_map: β {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup M)
(g : N ββ* P) (f : M ββ* N), map g (map f S) = map (MulHom.comp g f) Smap_map (g: N ββ* Pg : N: Type ?u.12339N ββ* P: Type ?u.12342P) (f: M ββ* Nf : M: Type ?u.12336M ββ* N: Type ?u.12339N) : (S: Subsemigroup MS.map: {M : Type ?u.12399} β
{N : Type ?u.12398} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).map: {M : Type ?u.12421} β
{N : Type ?u.12420} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap g: N ββ* Pg = S: Subsemigroup MS.map: {M : Type ?u.12443} β
{N : Type ?u.12442} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap (g: N ββ* Pg.comp: {M : Type ?u.12456} β
{N : Type ?u.12455} β
{P : Type ?u.12454} β [inst : Mul M] β [inst_1 : Mul N] β [inst_2 : Mul P] β (N ββ* P) β (M ββ* N) β M ββ* Pcomp f: M ββ* Nf) :=
SetLike.coe_injective: β {A : Type ?u.12510} {B : Type ?u.12511} [i : SetLike A B], Function.Injective SetLike.coeSetLike.coe_injective <| image_image: β {Ξ± : Type ?u.12528} {Ξ² : Type ?u.12530} {Ξ³ : Type ?u.12529} (g : Ξ² β Ξ³) (f : Ξ± β Ξ²) (s : Set Ξ±),
g '' (f '' s) = (fun x => g (f x)) '' simage_image _: ?m.12532 β ?m.12533_ _: ?m.12531 β ?m.12532_ _: Set ?m.12531_
#align subsemigroup.map_map Subsemigroup.map_map: β {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup M)
(g : N ββ* P) (f : M ββ* N), map g (map f S) = map (MulHom.comp g f) SSubsemigroup.map_map

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
Function.Injective βf β β {S : AddSubsemigroup M} {x : M}, βf x β AddSubsemigroup.map f S β x β Sto_additive]
theorem mem_map_iff_mem: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β {S : Subsemigroup M} {x : M}, βf x β map f S β x β Smem_map_iff_mem {f: M ββ* Nf : M: Type ?u.12671M ββ* N: Type ?u.12674N} (hf: Function.Injective βfhf : Function.Injective: {Ξ± : Sort ?u.12721} β {Ξ² : Sort ?u.12720} β (Ξ± β Ξ²) β PropFunction.Injective f: M ββ* Nf) {S: Subsemigroup MS : Subsemigroup: (M : Type ?u.12953) β [inst : Mul M] β Type ?u.12953Subsemigroup M: Type ?u.12671M} {x: Mx : M: Type ?u.12671M} :
f: M ββ* Nf x: Mx β S: Subsemigroup MS.map: {M : Type ?u.13166} β
{N : Type ?u.13165} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β x: Mx β S: Subsemigroup MS :=
hf: Function.Injective βfhf.mem_set_image: β {Ξ± : Type ?u.13275} {Ξ² : Type ?u.13276} {f : Ξ± β Ξ²},
Function.Injective f β β {s : Set Ξ±} {a : Ξ±}, f a β f '' s β a β smem_set_image
#align subsemigroup.mem_map_iff_mem Subsemigroup.mem_map_iff_mem: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β {S : Subsemigroup M} {x : M}, βf x β map f S β x β SSubsemigroup.mem_map_iff_mem
Function.Injective βf β β {S : AddSubsemigroup M} {x : M}, βf x β AddSubsemigroup.map f S β x β SAddSubsemigroup.mem_map_iff_mem

theorem map_le_iff_le_comap: β {f : M ββ* N} {S : Subsemigroup M} {T : Subsemigroup N}, map f S β€ T β S β€ comap f Tmap_le_iff_le_comap {f: M ββ* Nf : M: Type ?u.13378M ββ* N: Type ?u.13381N} {S: Subsemigroup MS : Subsemigroup: (M : Type ?u.13427) β [inst : Mul M] β Type ?u.13427Subsemigroup M: Type ?u.13378M} {T: Subsemigroup NT : Subsemigroup: (M : Type ?u.13431) β [inst : Mul M] β Type ?u.13431Subsemigroup N: Type ?u.13381N} :
S: Subsemigroup MS.map: {M : Type ?u.13437} β
{N : Type ?u.13436} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β€ T: Subsemigroup NT β S: Subsemigroup MS β€ T: Subsemigroup NT.comap: {M : Type ?u.13502} β
{N : Type ?u.13501} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
image_subset_iff: β {Ξ± : Type ?u.13561} {Ξ² : Type ?u.13562} {s : Set Ξ±} {t : Set Ξ²} {f : Ξ± β Ξ²}, f '' s β t β s β f β»ΒΉ' timage_subset_iff
#align subsemigroup.map_le_iff_le_comap Subsemigroup.map_le_iff_le_comap: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N} {S : Subsemigroup M} {T : Subsemigroup N},
map f S β€ T β S β€ comap f TSubsemigroup.map_le_iff_le_comap

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N),
theorem gc_map_comap: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N), GaloisConnection (map f) (comap f)gc_map_comap (f: M ββ* Nf : M: Type ?u.13669M ββ* N: Type ?u.13672N) : GaloisConnection: {Ξ± : Type ?u.13719} β {Ξ² : Type ?u.13718} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β (Ξ² β Ξ±) β PropGaloisConnection (map: {M : Type ?u.13755} β
{N : Type ?u.13754} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) (comap: {M : Type ?u.13818} β
{N : Type ?u.13817} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf) := fun _: ?m.13938_ _: ?m.13941_ =>
map_le_iff_le_comap: β {M : Type ?u.13943} {N : Type ?u.13944} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N} {S : Subsemigroup M}
{T : Subsemigroup N}, map f S β€ T β S β€ comap f Tmap_le_iff_le_comap
#align subsemigroup.gc_map_comap Subsemigroup.gc_map_comap: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N), GaloisConnection (map f) (comap f)Subsemigroup.gc_map_comap

theorem map_le_of_le_comap: β {T : Subsemigroup N} {f : M ββ* N}, S β€ comap f T β map f S β€ Tmap_le_of_le_comap {T: Subsemigroup NT : Subsemigroup: (M : Type ?u.14097) β [inst : Mul M] β Type ?u.14097Subsemigroup N: Type ?u.14069N} {f: M ββ* Nf : M: Type ?u.14066M ββ* N: Type ?u.14069N} : S: Subsemigroup MS β€ T: Subsemigroup NT.comap: {M : Type ?u.14122} β
{N : Type ?u.14121} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf β S: Subsemigroup MS.map: {M : Type ?u.14188} β
{N : Type ?u.14187} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β€ T: Subsemigroup NT :=
(gc_map_comap: β {M : Type ?u.14249} {N : Type ?u.14250} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_le: β {Ξ± : Type ?u.14278} {Ξ² : Type ?u.14277} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β {a : Ξ±} {b : Ξ²}, a β€ u b β l a β€ bl_le
#align subsemigroup.map_le_of_le_comap Subsemigroup.map_le_of_le_comap: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M ββ* N},
S β€ comap f T β map f S β€ TSubsemigroup.map_le_of_le_comap

theorem le_comap_of_map_le: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M ββ* N},
map f S β€ T β S β€ comap f Tle_comap_of_map_le {T: Subsemigroup NT : Subsemigroup: (M : Type ?u.14463) β [inst : Mul M] β Type ?u.14463Subsemigroup N: Type ?u.14435N} {f: M ββ* Nf : M: Type ?u.14432M ββ* N: Type ?u.14435N} : S: Subsemigroup MS.map: {M : Type ?u.14488} β
{N : Type ?u.14487} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β€ T: Subsemigroup NT β S: Subsemigroup MS β€ T: Subsemigroup NT.comap: {M : Type ?u.14554} β
{N : Type ?u.14553} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.14615} {N : Type ?u.14616} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).le_u: β {Ξ± : Type ?u.14644} {Ξ² : Type ?u.14643} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β {a : Ξ±} {b : Ξ²}, l a β€ b β a β€ u ble_u
#align subsemigroup.le_comap_of_map_le Subsemigroup.le_comap_of_map_le: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M ββ* N},
map f S β€ T β S β€ comap f TSubsemigroup.le_comap_of_map_le

theorem le_comap_map: β {f : M ββ* N}, S β€ comap f (map f S)le_comap_map {f: M ββ* Nf : M: Type ?u.14798M ββ* N: Type ?u.14801N} : S: Subsemigroup MS β€ (S: Subsemigroup MS.map: {M : Type ?u.14849} β
{N : Type ?u.14848} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.14871} β
{N : Type ?u.14870} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.14931} {N : Type ?u.14932} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).le_u_l: β {Ξ± : Type ?u.14960} {Ξ² : Type ?u.14959} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β (a : Ξ±), a β€ u (l a)le_u_l _: ?m.14969_
#align subsemigroup.le_comap_map Subsemigroup.le_comap_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {f : M ββ* N},
S β€ comap f (map f S)Subsemigroup.le_comap_map

theorem map_comap_le: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M ββ* N},
map f (comap f S) β€ Smap_comap_le {S: Subsemigroup NS : Subsemigroup: (M : Type ?u.15128) β [inst : Mul M] β Type ?u.15128Subsemigroup N: Type ?u.15100N} {f: M ββ* Nf : M: Type ?u.15097M ββ* N: Type ?u.15100N} : (S: Subsemigroup NS.comap: {M : Type ?u.15152} β
{N : Type ?u.15151} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf).map: {M : Type ?u.15174} β
{N : Type ?u.15173} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β€ S: Subsemigroup NS :=
(gc_map_comap: β {M : Type ?u.15236} {N : Type ?u.15237} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_u_le: β {Ξ± : Type ?u.15265} {Ξ² : Type ?u.15264} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β (a : Ξ²), l (u a) β€ al_u_le _: ?m.15275_
#align subsemigroup.map_comap_le Subsemigroup.map_comap_le: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M ββ* N},
map f (comap f S) β€ SSubsemigroup.map_comap_le

theorem monotone_map: β {f : M ββ* N}, Monotone (map f)monotone_map {f: M ββ* Nf : M: Type ?u.15406M ββ* N: Type ?u.15409N} : Monotone: {Ξ± : Type ?u.15456} β {Ξ² : Type ?u.15455} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone (map: {M : Type ?u.15492} β
{N : Type ?u.15491} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) :=
(gc_map_comap: β {M : Type ?u.15623} {N : Type ?u.15624} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).monotone_l: β {Ξ± : Type ?u.15652} {Ξ² : Type ?u.15651} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β Monotone lmonotone_l
#align subsemigroup.monotone_map Subsemigroup.monotone_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N}, Monotone (map f)Subsemigroup.monotone_map

theorem monotone_comap: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N}, Monotone (comap f)monotone_comap {f: M ββ* Nf : M: Type ?u.15784M ββ* N: Type ?u.15787N} : Monotone: {Ξ± : Type ?u.15834} β {Ξ² : Type ?u.15833} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone (comap: {M : Type ?u.15870} β
{N : Type ?u.15869} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf) :=
(gc_map_comap: β {M : Type ?u.16001} {N : Type ?u.16002} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).monotone_u: β {Ξ± : Type ?u.16030} {Ξ² : Type ?u.16029} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β Monotone umonotone_u
#align subsemigroup.monotone_comap Subsemigroup.monotone_comap: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N}, Monotone (comap f)Subsemigroup.monotone_comap

theorem map_comap_map: β {f : M ββ* N}, map f (comap f (map f S)) = map f Smap_comap_map {f: M ββ* Nf : M: Type ?u.16162M ββ* N: Type ?u.16165N} : ((S: Subsemigroup MS.map: {M : Type ?u.16213} β
{N : Type ?u.16212} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.16235} β
{N : Type ?u.16234} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf).map: {M : Type ?u.16253} β
{N : Type ?u.16252} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf = S: Subsemigroup MS.map: {M : Type ?u.16269} β
{N : Type ?u.16268} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.16287} {N : Type ?u.16288} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_u_l_eq_l: β {Ξ± : Type ?u.16316} {Ξ² : Type ?u.16315} [inst : Preorder Ξ±] [inst_1 : PartialOrder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β (a : Ξ±), l (u (l a)) = l al_u_l_eq_l _: ?m.16325_
#align subsemigroup.map_comap_map Subsemigroup.map_comap_map: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {f : M ββ* N},
map f (comap f (map f S)) = map f SSubsemigroup.map_comap_map

theorem comap_map_comap: β {S : Subsemigroup N} {f : M ββ* N}, comap f (map f (comap f S)) = comap f Scomap_map_comap {S: Subsemigroup NS : Subsemigroup: (M : Type ?u.16529) β [inst : Mul M] β Type ?u.16529Subsemigroup N: Type ?u.16501N} {f: M ββ* Nf : M: Type ?u.16498M ββ* N: Type ?u.16501N} :
((S: Subsemigroup NS.comap: {M : Type ?u.16553} β
{N : Type ?u.16552} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf).map: {M : Type ?u.16575} β
{N : Type ?u.16574} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.16593} β
{N : Type ?u.16592} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup NS.comap: {M : Type ?u.16609} β
{N : Type ?u.16608} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.16628} {N : Type ?u.16629} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).u_l_u_eq_u: β {Ξ± : Type ?u.16657} {Ξ² : Type ?u.16656} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±},
GaloisConnection l u β β (b : Ξ²), u (l (u b)) = u bu_l_u_eq_u _: ?m.16667_
#align subsemigroup.comap_map_comap Subsemigroup.comap_map_comap: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M ββ* N},
comap f (map f (comap f S)) = comap f SSubsemigroup.comap_map_comap

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup M) (f : AddHom M N),
theorem map_sup: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup M) (f : M ββ* N),
map f (S β T) = map f S β map f Tmap_sup (S: Subsemigroup MS T: Subsemigroup MT : Subsemigroup: (M : Type ?u.16868) β [inst : Mul M] β Type ?u.16868Subsemigroup M: Type ?u.16837M) (f: M ββ* Nf : M: Type ?u.16837M ββ* N: Type ?u.16840N) : (S: Subsemigroup MS β T: Subsemigroup MT).map: {M : Type ?u.16932} β
{N : Type ?u.16931} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf = S: Subsemigroup MS.map: {M : Type ?u.16955} β
{N : Type ?u.16954} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β T: Subsemigroup MT.map: {M : Type ?u.17013} β
{N : Type ?u.17012} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.17104} {N : Type ?u.17105} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_sup: β {Ξ± : Type ?u.17133} {Ξ² : Type ?u.17132} {aβ aβ : Ξ±} [inst : SemilatticeSup Ξ±] [inst_1 : SemilatticeSup Ξ²] {l : Ξ± β Ξ²}
{u : Ξ² β Ξ±}, GaloisConnection l u β l (aβ β aβ) = l aβ β l aβl_sup
#align subsemigroup.map_sup Subsemigroup.map_sup: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup M) (f : M ββ* N),
map f (S β T) = map f S β map f TSubsemigroup.map_sup

@[to_additive: β {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {ΞΉ : Sort u_1} (f : AddHom M N)
theorem map_iSup: β {ΞΉ : Sort u_1} (f : M ββ* N) (s : ΞΉ β Subsemigroup M), map f (iSup s) = β¨ i, map f (s i)map_iSup {ΞΉ: Sort ?u.17291ΞΉ : Sort _: Type ?u.17291SortSort _: Type ?u.17291 _} (f: M ββ* Nf : M: Type ?u.17260M ββ* N: Type ?u.17263N) (s: ΞΉ β Subsemigroup Ms : ΞΉ: Sort ?u.17291ΞΉ β Subsemigroup: (M : Type ?u.17314) β [inst : Mul M] β Type ?u.17314Subsemigroup M: Type ?u.17260M) :
(iSup: {Ξ± : Type ?u.17320} β [inst : SupSet Ξ±] β {ΞΉ : Sort ?u.17319} β (ΞΉ β Ξ±) β Ξ±iSup s: ΞΉ β Subsemigroup Ms).map: {M : Type ?u.17351} β
{N : Type ?u.17350} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf = β¨ i: ?m.17376i, (s: ΞΉ β Subsemigroup Ms i: ?m.17376i).map: {M : Type ?u.17379} β
{N : Type ?u.17378} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.17466} {N : Type ?u.17467} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_iSup: β {Ξ± : Type ?u.17496} {Ξ² : Type ?u.17495} {ΞΉ : Sort ?u.17494} [inst : CompleteLattice Ξ±] [inst_1 : CompleteLattice Ξ²]
{l : Ξ± β Ξ²} {u : Ξ² β Ξ±}, GaloisConnection l u β β {f : ΞΉ β Ξ±}, l (iSup f) = β¨ i, l (f i)l_iSup
#align subsemigroup.map_supr Subsemigroup.map_iSup: β {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {ΞΉ : Sort u_1} (f : M ββ* N) (s : ΞΉ β Subsemigroup M),
map f (iSup s) = β¨ i, map f (s i)Subsemigroup.map_iSup
#align add_subsemigroup.map_supr AddSubsemigroup.map_iSup: β {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {ΞΉ : Sort u_1} (f : AddHom M N)

@[to_additive: β {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup N) (f : AddHom M N),
theorem comap_inf: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup N) (f : M ββ* N),
comap f (S β T) = comap f S β comap f Tcomap_inf (S: Subsemigroup NS T: Subsemigroup NT : Subsemigroup: (M : Type ?u.17674) β [inst : Mul M] β Type ?u.17674Subsemigroup N: Type ?u.17636N) (f: M ββ* Nf : M: Type ?u.17633M ββ* N: Type ?u.17636N) : (S: Subsemigroup NS β T: Subsemigroup NT).comap: {M : Type ?u.17708} β
{N : Type ?u.17707} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup NS.comap: {M : Type ?u.17731} β
{N : Type ?u.17730} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf β T: Subsemigroup NT.comap: {M : Type ?u.17789} β
{N : Type ?u.17788} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.17860} {N : Type ?u.17861} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).u_inf: β {Ξ± : Type ?u.17889} {Ξ² : Type ?u.17888} {bβ bβ : Ξ²} [inst : SemilatticeInf Ξ±] [inst_1 : SemilatticeInf Ξ²] {l : Ξ± β Ξ²}
{u : Ξ² β Ξ±}, GaloisConnection l u β u (bβ β bβ) = u bβ β u bβu_inf
#align subsemigroup.comap_inf Subsemigroup.comap_inf: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup N) (f : M ββ* N),
comap f (S β T) = comap f S β comap f TSubsemigroup.comap_inf

@[to_additive: β {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {ΞΉ : Sort u_1} (f : AddHom M N)
theorem comap_iInf: β {ΞΉ : Sort u_1} (f : M ββ* N) (s : ΞΉ β Subsemigroup N), comap f (iInf s) = β¨ i, comap f (s i)comap_iInf {ΞΉ: Sort u_1ΞΉ : Sort _: Type ?u.18053SortSort _: Type ?u.18053 _} (f: M ββ* Nf : M: Type ?u.18022M ββ* N: Type ?u.18025N) (s: ΞΉ β Subsemigroup Ns : ΞΉ: Sort ?u.18053ΞΉ β Subsemigroup: (M : Type ?u.18076) β [inst : Mul M] β Type ?u.18076Subsemigroup N: Type ?u.18025N) :
(iInf: {Ξ± : Type ?u.18082} β [inst : InfSet Ξ±] β {ΞΉ : Sort ?u.18081} β (ΞΉ β Ξ±) β Ξ±iInf s: ΞΉ β Subsemigroup Ns).comap: {M : Type ?u.18104} β
{N : Type ?u.18103} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = β¨ i: ?m.18129i, (s: ΞΉ β Subsemigroup Ns i: ?m.18129i).comap: {M : Type ?u.18132} β
{N : Type ?u.18131} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf :=
(gc_map_comap: β {M : Type ?u.18210} {N : Type ?u.18211} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).u_iInf: β {Ξ± : Type ?u.18240} {Ξ² : Type ?u.18239} {ΞΉ : Sort ?u.18238} [inst : CompleteLattice Ξ±] [inst_1 : CompleteLattice Ξ²]
{l : Ξ± β Ξ²} {u : Ξ² β Ξ±}, GaloisConnection l u β β {f : ΞΉ β Ξ²}, u (iInf f) = β¨ i, u (f i)u_iInf
#align subsemigroup.comap_infi Subsemigroup.comap_iInf: β {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {ΞΉ : Sort u_1} (f : M ββ* N) (s : ΞΉ β Subsemigroup N),
comap f (iInf s) = β¨ i, comap f (s i)Subsemigroup.comap_iInf
#align add_subsemigroup.comap_infi AddSubsemigroup.comap_iInf: β {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {ΞΉ : Sort u_1} (f : AddHom M N)

theorem map_bot: β (f : M ββ* N), map f β₯ = β₯map_bot (f: M ββ* Nf : M: Type ?u.18387M ββ* N: Type ?u.18390N) : (β₯: ?m.18441β₯ : Subsemigroup: (M : Type ?u.18438) β [inst : Mul M] β Type ?u.18438Subsemigroup M: Type ?u.18387M).map: {M : Type ?u.18481} β
{N : Type ?u.18480} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf = β₯: ?m.18501β₯ :=
(gc_map_comap: β {M : Type ?u.18560} {N : Type ?u.18561} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).l_bot: β {Ξ± : Type ?u.18589} {Ξ² : Type ?u.18588} [inst : Preorder Ξ±] [inst_1 : PartialOrder Ξ²] [inst_2 : OrderBot Ξ²]
[inst_3 : OrderBot Ξ±] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±}, GaloisConnection l u β l β₯ = β₯l_bot
#align subsemigroup.map_bot Subsemigroup.map_bot: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N), map f β₯ = β₯Subsemigroup.map_bot

theorem comap_top: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N), comap f β€ = β€comap_top (f: M ββ* Nf : M: Type ?u.18832M ββ* N: Type ?u.18835N) : (β€: ?m.18886β€ : Subsemigroup: (M : Type ?u.18883) β [inst : Mul M] β Type ?u.18883Subsemigroup N: Type ?u.18835N).comap: {M : Type ?u.18921} β
{N : Type ?u.18920} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = β€: ?m.18941β€ :=
(gc_map_comap: β {M : Type ?u.18991} {N : Type ?u.18992} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).u_top: β {Ξ± : Type ?u.19020} {Ξ² : Type ?u.19019} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²] [inst_2 : OrderTop Ξ±]
[inst_3 : OrderTop Ξ²] {l : Ξ± β Ξ²} {u : Ξ² β Ξ±}, GaloisConnection l u β u β€ = β€u_top
#align subsemigroup.comap_top Subsemigroup.comap_top: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N), comap f β€ = β€Subsemigroup.comap_top

theorem map_id: β (S : Subsemigroup M), map (MulHom.id M) S = Smap_id (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.19292) β [inst : Mul M] β Type ?u.19292Subsemigroup M: Type ?u.19261M) : S: Subsemigroup MS.map: {M : Type ?u.19304} β
{N : Type ?u.19303} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap (MulHom.id: (M : Type ?u.19315) β [inst : Mul M] β M ββ* MMulHom.id M: Type ?u.19261M) = S: Subsemigroup MS :=
ext: β {M : Type ?u.19330} [inst : Mul M] {S T : Subsemigroup M}, (β (x : M), x β S β x β T) β S = Text fun _: ?m.19362_ => β¨fun β¨_: ?m.19362_, h: xβΒΉ β βSh, rfl: β {Ξ± : Sort ?u.19376} {a : Ξ±}, a = arflβ© => h: xβΒΉ β βSh, fun h: ?m.19677h => β¨_: ?m.19684_, h: ?m.19677h, rfl: β {Ξ± : Sort ?u.19709} {a : Ξ±}, a = arflβ©β©
#align subsemigroup.map_id Subsemigroup.map_id: β {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), map (MulHom.id M) S = SSubsemigroup.map_id

section GaloisCoinsertion

variable {ΞΉ: Type ?u.22089ΞΉ : Type _: Type (?u.23689+1)Type _} {f: M ββ* Nf : M: Type ?u.20133M ββ* N: Type ?u.19857N} (hf: Function.Injective βfhf : Function.Injective: {Ξ± : Sort ?u.23705} β {Ξ² : Sort ?u.23704} β (Ξ± β Ξ²) β PropFunction.Injective f: M ββ* Nf)

--include hf

/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/
@[to_additive: {M : Type u_1} β
{N : Type u_2} β
{f : AddHom M N} β Function.Injective βf β GaloisCoinsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)to_additive " `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. "]
def gciMapComap: {M : Type u_1} β
{N : Type u_2} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap : GaloisCoinsertion: {Ξ± : Type ?u.20413} β
{Ξ² : Type ?u.20412} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β (Ξ² β Ξ±) β Type (max?u.20413?u.20412)GaloisCoinsertion (map: {M : Type ?u.20449} β
{N : Type ?u.20448} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) (comap: {M : Type ?u.20524} β
{N : Type ?u.20523} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf) :=
(gc_map_comap: β {M : Type ?u.20641} {N : Type ?u.20642} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).toGaloisCoinsertion: {Ξ± : Type ?u.20654} β
{Ξ² : Type ?u.20653} β
[inst : Preorder Ξ±] β
[inst_1 : Preorder Ξ²] β
{l : Ξ± β Ξ²} β {u : Ξ² β Ξ±} β GaloisConnection l u β (β (a : Ξ±), u (l a) β€ a) β GaloisCoinsertion l utoGaloisCoinsertion fun S: ?m.20689S x: ?m.20692x => byGoals accomplished! π M: Type ?u.20133N: Type ?u.20136P: Type ?u.20139Ο: Type ?u.20142instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup MΞΉ: Type ?u.20164f: M ββ* Nhf: Function.Injective βfS: Subsemigroup Mx: Mx β comap f (map f S) β x β Ssimp [mem_comap: β {M : Type ?u.20700} {N : Type ?u.20699} [inst : Mul M] [inst_1 : Mul N] {S : Subsemigroup N} {f : M ββ* N} {x : M},
x β comap f S β βf x β Smem_comap, mem_map: β {M : Type ?u.20740} {N : Type ?u.20741} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N} {S : Subsemigroup M} {y : N},
y β map f S β β x, x β S β§ βf x = ymem_map, hf: Function.Injective βfhf.eq_iff: β {Ξ± : Sort ?u.20773} {Ξ² : Sort ?u.20774} {f : Ξ± β Ξ²}, Function.Injective f β β {a b : Ξ±}, f a = f b β a = beq_iff]Goals accomplished! π
#align subsemigroup.gci_map_comap Subsemigroup.gciMapComap: {M : Type u_1} β
{N : Type u_2} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)Subsemigroup.gciMapComap
{N : Type u_2} β

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem comap_map_eq_of_injective: β (S : Subsemigroup M), comap f (map f S) = Scomap_map_eq_of_injective (S: Subsemigroup MS : Subsemigroup: (M : Type ?u.22337) β [inst : Mul M] β Type ?u.22337Subsemigroup M: Type ?u.22058M) : (S: Subsemigroup MS.map: {M : Type ?u.22349} β
{N : Type ?u.22348} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.22377} β
{N : Type ?u.22376} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup MS :=
(gciMapComap: {M : Type ?u.22398} β
{N : Type ?u.22397} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_l_eq: β {Ξ± : Type ?u.22442} {Ξ² : Type ?u.22441} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²],
GaloisCoinsertion l u β β (a : Ξ±), u (l a) = au_l_eq _: ?m.22451_
#align subsemigroup.comap_map_eq_of_injective Subsemigroup.comap_map_eq_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β (S : Subsemigroup M), comap f (map f S) = SSubsemigroup.comap_map_eq_of_injective

@[to_additive: β {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem comap_surjective_of_injective: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β Function.Surjective (comap f)comap_surjective_of_injective : Function.Surjective: {Ξ± : Sort ?u.22868} β {Ξ² : Sort ?u.22867} β (Ξ± β Ξ²) β PropFunction.Surjective (comap: {M : Type ?u.22872} β
{N : Type ?u.22871} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf) :=
(gciMapComap: {M : Type ?u.22949} β
{N : Type ?u.22948} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_surjective: β {Ξ± : Type ?u.22993} {Ξ² : Type ?u.22992} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²],
GaloisCoinsertion l u β Function.Surjective uu_surjective
#align subsemigroup.comap_surjective_of_injective Subsemigroup.comap_surjective_of_injective: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β Function.Surjective (comap f)Subsemigroup.comap_surjective_of_injective

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem map_injective_of_injective: Function.Injective (map f)map_injective_of_injective : Function.Injective: {Ξ± : Sort ?u.23404} β {Ξ² : Sort ?u.23403} β (Ξ± β Ξ²) β PropFunction.Injective (map: {M : Type ?u.23408} β
{N : Type ?u.23407} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) :=
(gciMapComap: {M : Type ?u.23484} β
{N : Type ?u.23483} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).l_injective: β {Ξ± : Type ?u.23528} {Ξ² : Type ?u.23527} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²],
GaloisCoinsertion l u β Function.Injective ll_injective
#align subsemigroup.map_injective_of_injective Subsemigroup.map_injective_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β Function.Injective (map f)Subsemigroup.map_injective_of_injective

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
Function.Injective βf β
theorem comap_inf_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β (S T : Subsemigroup M), comap f (map f S β map f T) = S β Tcomap_inf_map_of_injective (S: Subsemigroup MS T: Subsemigroup MT : Subsemigroup: (M : Type ?u.23947) β [inst : Mul M] β Type ?u.23947Subsemigroup M: Type ?u.23658M) : (S: Subsemigroup MS.map: {M : Type ?u.23956} β
{N : Type ?u.23955} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β T: Subsemigroup MT.map: {M : Type ?u.24026} β
{N : Type ?u.24025} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.24093} β
{N : Type ?u.24092} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup MS β T: Subsemigroup MT :=
(gciMapComap: {M : Type ?u.24127} β
{N : Type ?u.24126} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_inf_l: β {Ξ± : Type ?u.24171} {Ξ² : Type ?u.24170} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : SemilatticeInf Ξ±] [inst_1 : SemilatticeInf Ξ²],
GaloisCoinsertion l u β β (a b : Ξ±), u (l a β l b) = a β bu_inf_l _: ?m.24181_ _: ?m.24181_
#align subsemigroup.comap_inf_map_of_injective Subsemigroup.comap_inf_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β (S T : Subsemigroup M), comap f (map f S β map f T) = S β TSubsemigroup.comap_inf_map_of_injective
Function.Injective βf β

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ΞΉ : Type u_3} {f : AddHom M N},
Function.Injective βf β
theorem comap_iInf_map_of_injective: β (S : ΞΉ β Subsemigroup M), comap f (β¨ i, map f (S i)) = iInf Scomap_iInf_map_of_injective (S: ΞΉ β Subsemigroup MS : ΞΉ: Type ?u.24355ΞΉ β Subsemigroup: (M : Type ?u.24605) β [inst : Mul M] β Type ?u.24605Subsemigroup M: Type ?u.24324M) :
(β¨ i: ?m.24622i, (S: ΞΉ β Subsemigroup MS i: ?m.24622i).map: {M : Type ?u.24625} β
{N : Type ?u.24624} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.24711} β
{N : Type ?u.24710} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = iInf: {Ξ± : Type ?u.24727} β [inst : InfSet Ξ±] β {ΞΉ : Sort ?u.24726} β (ΞΉ β Ξ±) β Ξ±iInf S: ΞΉ β Subsemigroup MS :=
(gciMapComap: {M : Type ?u.24750} β
{N : Type ?u.24749} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_iInf_l: β {Ξ± : Type ?u.24795} {Ξ² : Type ?u.24794} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : CompleteLattice Ξ±]
[inst_1 : CompleteLattice Ξ²], GaloisCoinsertion l u β β {ΞΉ : Sort ?u.24793} (f : ΞΉ β Ξ±), u (β¨ i, l (f i)) = β¨ i, f iu_iInf_l _: ?m.24847 β ?m.24805_
#align subsemigroup.comap_infi_map_of_injective Subsemigroup.comap_iInf_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ΞΉ : Type u_3} {f : M ββ* N},
Function.Injective βf β β (S : ΞΉ β Subsemigroup M), comap f (β¨ i, map f (S i)) = iInf SSubsemigroup.comap_iInf_map_of_injective
#align add_subsemigroup.comap_infi_map_of_injective AddSubsemigroup.comap_iInf_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ΞΉ : Type u_3} {f : AddHom M N},
Function.Injective βf β

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
Function.Injective βf β
theorem comap_sup_map_of_injective: β (S T : Subsemigroup M), comap f (map f S β map f T) = S β Tcomap_sup_map_of_injective (S: Subsemigroup MS T: Subsemigroup MT : Subsemigroup: (M : Type ?u.25255) β [inst : Mul M] β Type ?u.25255Subsemigroup M: Type ?u.24966M) : (S: Subsemigroup MS.map: {M : Type ?u.25264} β
{N : Type ?u.25263} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β T: Subsemigroup MT.map: {M : Type ?u.25334} β
{N : Type ?u.25333} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.25421} β
{N : Type ?u.25420} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = S: Subsemigroup MS β T: Subsemigroup MT :=
(gciMapComap: {M : Type ?u.25475} β
{N : Type ?u.25474} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_sup_l: β {Ξ± : Type ?u.25519} {Ξ² : Type ?u.25518} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : SemilatticeSup Ξ±] [inst_1 : SemilatticeSup Ξ²],
GaloisCoinsertion l u β β (a b : Ξ±), u (l a β l b) = a β bu_sup_l _: ?m.25529_ _: ?m.25529_
#align subsemigroup.comap_sup_map_of_injective Subsemigroup.comap_sup_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β (S T : Subsemigroup M), comap f (map f S β map f T) = S β TSubsemigroup.comap_sup_map_of_injective
Function.Injective βf β

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ΞΉ : Type u_3} {f : AddHom M N},
Function.Injective βf β
theorem comap_iSup_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ΞΉ : Type u_3} {f : M ββ* N},
Function.Injective βf β β (S : ΞΉ β Subsemigroup M), comap f (β¨ i, map f (S i)) = iSup Scomap_iSup_map_of_injective (S: ΞΉ β Subsemigroup MS : ΞΉ: Type ?u.25697ΞΉ β Subsemigroup: (M : Type ?u.25947) β [inst : Mul M] β Type ?u.25947Subsemigroup M: Type ?u.25666M) :
(β¨ i: ?m.25964i, (S: ΞΉ β Subsemigroup MS i: ?m.25964i).map: {M : Type ?u.25967} β
{N : Type ?u.25966} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf).comap: {M : Type ?u.26062} β
{N : Type ?u.26061} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf = iSup: {Ξ± : Type ?u.26078} β [inst : SupSet Ξ±] β {ΞΉ : Sort ?u.26077} β (ΞΉ β Ξ±) β Ξ±iSup S: ΞΉ β Subsemigroup MS :=
(gciMapComap: {M : Type ?u.26110} β
{N : Type ?u.26109} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).u_iSup_l: β {Ξ± : Type ?u.26155} {Ξ² : Type ?u.26154} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : CompleteLattice Ξ±]
[inst_1 : CompleteLattice Ξ²], GaloisCoinsertion l u β β {ΞΉ : Sort ?u.26153} (f : ΞΉ β Ξ±), u (β¨ i, l (f i)) = β¨ i, f iu_iSup_l _: ?m.26207 β ?m.26165_
#align subsemigroup.comap_supr_map_of_injective Subsemigroup.comap_iSup_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ΞΉ : Type u_3} {f : M ββ* N},
Function.Injective βf β β (S : ΞΉ β Subsemigroup M), comap f (β¨ i, map f (S i)) = iSup SSubsemigroup.comap_iSup_map_of_injective
#align add_subsemigroup.comap_supr_map_of_injective AddSubsemigroup.comap_iSup_map_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ΞΉ : Type u_3} {f : AddHom M N},
Function.Injective βf β

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem map_le_map_iff_of_injective: β {S T : Subsemigroup M}, map f S β€ map f T β S β€ Tmap_le_map_iff_of_injective {S: Subsemigroup MS T: Subsemigroup MT : Subsemigroup: (M : Type ?u.26605) β [inst : Mul M] β Type ?u.26605Subsemigroup M: Type ?u.26316M} : S: Subsemigroup MS.map: {M : Type ?u.26611} β
{N : Type ?u.26610} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β€ T: Subsemigroup MT.map: {M : Type ?u.26639} β
{N : Type ?u.26638} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf β S: Subsemigroup MS β€ T: Subsemigroup MT :=
(gciMapComap: {M : Type ?u.26741} β
{N : Type ?u.26740} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).l_le_l_iff: β {Ξ± : Type ?u.26785} {Ξ² : Type ?u.26784} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²],
GaloisCoinsertion l u β β {a b : Ξ±}, l a β€ l b β a β€ bl_le_l_iff
#align subsemigroup.map_le_map_iff_of_injective Subsemigroup.map_le_map_iff_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β β {S T : Subsemigroup M}, map f S β€ map f T β S β€ TSubsemigroup.map_le_map_iff_of_injective

@[to_additive: β {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem map_strictMono_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β StrictMono (map f)map_strictMono_of_injective : StrictMono: {Ξ± : Type ?u.27221} β {Ξ² : Type ?u.27220} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropStrictMono (map: {M : Type ?u.27257} β
{N : Type ?u.27256} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) :=
(gciMapComap: {M : Type ?u.27399} β
{N : Type ?u.27398} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Injective βf β GaloisCoinsertion (map f) (comap f)gciMapComap hf: Function.Injective βfhf).strictMono_l: β {Ξ± : Type ?u.27443} {Ξ² : Type ?u.27442} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²],
GaloisCoinsertion l u β StrictMono lstrictMono_l
#align subsemigroup.map_strict_mono_of_injective Subsemigroup.map_strictMono_of_injective: β {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Injective βf β StrictMono (map f)Subsemigroup.map_strictMono_of_injective

end GaloisCoinsertion

section GaloisInsertion

variable {ΞΉ: Type ?u.29177ΞΉ : Type _: Type (?u.30792+1)Type _} {f: M ββ* Nf : M: Type ?u.27865M ββ* N: Type ?u.29149N} (hf: Function.Surjective βfhf : Function.Surjective: {Ξ± : Sort ?u.27632} β {Ξ² : Sort ?u.27631} β (Ξ± β Ξ²) β PropFunction.Surjective f: M ββ* Nf)

/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/
@[to_additive: {M : Type u_1} β
{N : Type u_2} β
{f : AddHom M N} β Function.Surjective βf β GaloisInsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)to_additive " `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. "]
def giMapComap: {M : Type u_1} β
{N : Type u_2} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Surjective βf β GaloisInsertion (map f) (comap f)giMapComap : GaloisInsertion: {Ξ± : Type ?u.28146} β
{Ξ² : Type ?u.28145} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β (Ξ² β Ξ±) β Type (max?u.28146?u.28145)GaloisInsertion (map: {M : Type ?u.28182} β
{N : Type ?u.28181} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf) (comap: {M : Type ?u.28257} β
{N : Type ?u.28256} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf) :=
(gc_map_comap: β {M : Type ?u.28374} {N : Type ?u.28375} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N),
GaloisConnection (map f) (comap f)gc_map_comap f: M ββ* Nf).toGaloisInsertion: {Ξ± : Type ?u.28387} β
{Ξ² : Type ?u.28386} β
[inst : Preorder Ξ±] β
[inst_1 : Preorder Ξ²] β
{l : Ξ± β Ξ²} β {u : Ξ² β Ξ±} β GaloisConnection l u β (β (b : Ξ²), b β€ l (u b)) β GaloisInsertion l utoGaloisInsertion fun S: ?m.28422S x: ?m.28425x h: ?m.28428h =>
let β¨y: My, hy: βf y = xhyβ© := hf: Function.Surjective βfhf x: ?m.28425x
mem_map: β {M : Type ?u.28489} {N : Type ?u.28490} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N} {S : Subsemigroup M} {y : N},
y β map f S β β x, x β S β§ βf x = ymem_map.2: β {a b : Prop}, (a β b) β b β a2 β¨y: My, byGoals accomplished! π M: Type ?u.27865N: Type ?u.27868P: Type ?u.27871Ο: Type ?u.27874instβΒ²: Mul MinstβΒΉ: Mul Ninstβ: Mul PSβ: Subsemigroup MΞΉ: Type ?u.27896f: M ββ* Nhf: Function.Surjective βfS: Subsemigroup Nx: Nh: x β Sy: Mhy: βf y = xy β comap f S β§ βf y = xsimp [hy: βf y = xhy, h: x β Sh]Goals accomplished! πβ©
#align subsemigroup.gi_map_comap Subsemigroup.giMapComap: {M : Type u_1} β
{N : Type u_2} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Surjective βf β GaloisInsertion (map f) (comap f)Subsemigroup.giMapComap
{N : Type u_2} β

@[to_additive: β {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {f : AddHom M N},
theorem map_comap_eq_of_surjective: β (S : Subsemigroup N), map f (comap f S) = Smap_comap_eq_of_surjective (S: Subsemigroup NS : Subsemigroup: (M : Type ?u.29426) β [inst : Mul M] β Type ?u.29426Subsemigroup N: Type ?u.29149N) : (S: Subsemigroup NS.comap: {M : Type ?u.29438} β
{N : Type ?u.29437} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup N β Subsemigroup Mcomap f: M ββ* Nf).map: {M : Type ?u.29466} β
{N : Type ?u.29465} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β Subsemigroup M β Subsemigroup Nmap f: M ββ* Nf = S: Subsemigroup NS :=
(giMapComap: {M : Type ?u.29487} β
{N : Type ?u.29486} β
[inst : Mul M] β [inst_1 : Mul N] β {f : M ββ* N} β Function.Surjective βf β GaloisInsertion (map f) (comap f)giMapComap hf: Function.Surjective βfhf).l_u_eq: β {Ξ± : Type ?u.29532} {Ξ² : Type ?u.29531} {l : Ξ± β Ξ²} {u : Ξ² β Ξ±} [inst : Preorder Ξ±] [inst_1 : PartialOrder Ξ²],
GaloisInsertion l u β β (b : Ξ²), l (u b) = bl_u_eq _: ?m.29542_
#align subsemigroup.map_comap_eq_of_surjective Subsemigroup.map_comap_eq_of_surjective: β {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] {f : M ββ* N},
Function.Surjective βf β β (S : Subsemigroup N), map f (comap f S) = SSubsemigroup.map_comap_eq_of_surjective