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.
/-
Copyright (c) 2022 Yakov Pechersky. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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

* `Subsemigroup.toAddSubsemigroup`, `Subsemigroup.toAddSubsemigroup'`,
  `AddSubsemigroup.toSubsemigroup`, `AddSubsemigroup.toSubsemigroup'`:
  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.14
M
N: Type ?u.5
N
P: Type ?u.33445
P
Οƒ: Type ?u.33448
Οƒ
:
Type _: Type (?u.11+1)
Type _
} /-! ### Conversion to/from `Additive`/`Multiplicative` -/ section variable [
Mul: Type ?u.26 β†’ Type ?u.26
Mul
M: Type ?u.14
M
] /-- Subsemigroups of semigroup `M` are isomorphic to additive subsemigroups of `Additive M`. -/ @[
simps: βˆ€ {M : Type u_1} [inst : Mul M] (S : AddSubsemigroup (Additive M)), ↑(↑(RelIso.symm toAddSubsemigroup) S) = ↑Additive.ofMul ⁻¹' ↑S
simps
] 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.46
Subsemigroup
M: Type ?u.29
M
≃o
AddSubsemigroup: (M : Type ?u.54) β†’ [inst : Add M] β†’ Type ?u.54
AddSubsemigroup
(
Additive: Type ?u.55 β†’ Type ?u.55
Additive
M: Type ?u.29
M
) where toFun
S: ?m.166
S
:= { carrier :=
Additive.toMul: {Ξ± : Type ?u.179} β†’ Additive Ξ± ≃ Ξ±
Additive.toMul
⁻¹'
S: ?m.166
S
add_mem' :=
S: ?m.166
S
.
mul_mem': βˆ€ {M : Type ?u.349} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a ∈ self.carrier β†’ b ∈ self.carrier β†’ a * b ∈ self.carrier
mul_mem'
} invFun
S: ?m.393
S
:= { carrier :=
Additive.ofMul: {Ξ± : Type ?u.403} β†’ Ξ± ≃ Additive Ξ±
Additive.ofMul
⁻¹'
S: ?m.393
S
mul_mem' :=
S: ?m.393
S
.
add_mem': βˆ€ {M : Type ?u.548} [inst : Add M] (self : AddSubsemigroup M) {a b : M}, a ∈ self.carrier β†’ b ∈ self.carrier β†’ a + b ∈ self.carrier
add_mem'
} left_inv
_: ?m.578
_
:=
rfl: βˆ€ {Ξ± : Sort ?u.580} {a : Ξ±}, a = a
rfl
right_inv
_: ?m.598
_
:=
rfl: βˆ€ {Ξ± : Sort ?u.600} {a : Ξ±}, a = a
rfl
map_rel_iff':=
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align subsemigroup.to_add_subsemigroup
Subsemigroup.toAddSubsemigroup: {M : Type u_1} β†’ [inst : Mul M] β†’ Subsemigroup M ≃o AddSubsemigroup (Additive M)
Subsemigroup.toAddSubsemigroup
#align subsemigroup.to_add_subsemigroup_symm_apply_coe
Subsemigroup.toAddSubsemigroup_symm_apply_coe: βˆ€ {M : Type u_1} [inst : Mul M] (S : AddSubsemigroup (Additive M)), ↑(↑(RelIso.symm Subsemigroup.toAddSubsemigroup) S) = ↑Additive.ofMul ⁻¹' ↑S
Subsemigroup.toAddSubsemigroup_symm_apply_coe
#align subsemigroup.to_add_subsemigroup_apply_coe
Subsemigroup.toAddSubsemigroup_apply_coe: βˆ€ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), ↑(↑Subsemigroup.toAddSubsemigroup S) = ↑Additive.toMul ⁻¹' ↑S
Subsemigroup.toAddSubsemigroup_apply_coe
/-- Additive subsemigroups of an additive semigroup `Additive M` are isomorphic to subsemigroups of `M`. -/ abbrev
AddSubsemigroup.toSubsemigroup': {M : Type u_1} β†’ [inst : Mul M] β†’ AddSubsemigroup (Additive M) ≃o Subsemigroup M
AddSubsemigroup.toSubsemigroup'
:
AddSubsemigroup: (M : Type ?u.882) β†’ [inst : Add M] β†’ Type ?u.882
AddSubsemigroup
(
Additive: Type ?u.883 β†’ Type ?u.883
Additive
M: Type ?u.865
M
) ≃o
Subsemigroup: (M : Type ?u.900) β†’ [inst : Mul M] β†’ Type ?u.900
Subsemigroup
M: Type ?u.865
M
:=
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
#align add_subsemigroup.to_subsemigroup'
AddSubsemigroup.toSubsemigroup': {M : Type u_1} β†’ [inst : Mul M] β†’ AddSubsemigroup (Additive M) ≃o Subsemigroup M
AddSubsemigroup.toSubsemigroup'
theorem
Subsemigroup.toAddSubsemigroup_closure: βˆ€ (S : Set M), ↑toAddSubsemigroup (closure S) = AddSubsemigroup.closure (↑Additive.toMul ⁻¹' S)
Subsemigroup.toAddSubsemigroup_closure
(
S: Set M
S
:
Set: Type ?u.1175 β†’ Type ?u.1175
Set
M: Type ?u.1160
M
) :
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 M
Subsemigroup.closure
S: Set M
S
) =
AddSubsemigroup.closure: {M : Type ?u.1299} β†’ [inst : Add M] β†’ Set M β†’ AddSubsemigroup M
AddSubsemigroup.closure
(
Additive.toMul: {Ξ± : Type ?u.1308} β†’ Additive Ξ± ≃ Ξ±
Additive.toMul
⁻¹'
S: Set M
S
) :=
le_antisymm: βˆ€ {Ξ± : Type ?u.1409} [inst : PartialOrder Ξ±] {a b : Ξ±}, a ≀ b β†’ b ≀ a β†’ a = b
le_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 ≀ y
le_symm_apply
.
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1
<|
Subsemigroup.closure_le: βˆ€ {M : Type ?u.1621} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s ≀ S ↔ s βŠ† ↑S
Subsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
(
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.1662
Additive
M: Type ?u.1160
M
))) (
AddSubsemigroup.closure_le: βˆ€ {M : Type ?u.1722} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s ≀ S ↔ s βŠ† ↑S
AddSubsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
(
Subsemigroup.subset_closure: βˆ€ {M : Type ?u.1758} [inst : Mul M] {s : Set M}, s βŠ† ↑(closure s)
Subsemigroup.subset_closure
(M :=
M: Type ?u.1160
M
))) #align subsemigroup.to_add_subsemigroup_closure
Subsemigroup.toAddSubsemigroup_closure: βˆ€ {M : Type u_1} [inst : Mul M] (S : Set M), ↑Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (↑Additive.toMul ⁻¹' S)
Subsemigroup.toAddSubsemigroup_closure
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.1813
Set
(
Additive: Type ?u.1814 β†’ Type ?u.1814
Additive
M: Type ?u.1798
M
)) :
AddSubsemigroup.toSubsemigroup': {M : Type ?u.1818} β†’ [inst : Mul M] β†’ AddSubsemigroup (Additive M) ≃o Subsemigroup M
AddSubsemigroup.toSubsemigroup'
(
AddSubsemigroup.closure: {M : Type ?u.1901} β†’ [inst : Add M] β†’ Set M β†’ AddSubsemigroup M
AddSubsemigroup.closure
S: Set (Additive M)
S
) =
Subsemigroup.closure: {M : Type ?u.1950} β†’ [inst : Mul M] β†’ Set M β†’ Subsemigroup M
Subsemigroup.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 = b
le_antisymm
(
AddSubsemigroup.toSubsemigroup': {M : Type ?u.2076} β†’ [inst : Mul M] β†’ AddSubsemigroup (Additive M) ≃o Subsemigroup M
AddSubsemigroup.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 ≀ y
le_symm_apply
.
1: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
1
<|
AddSubsemigroup.closure_le: βˆ€ {M : Type ?u.2258} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, closure s ≀ S ↔ s βŠ† ↑S
AddSubsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
(
Subsemigroup.subset_closure: βˆ€ {M : Type ?u.2296} [inst : Mul M] {s : Set M}, s βŠ† ↑(Subsemigroup.closure s)
Subsemigroup.subset_closure
(M :=
M: Type ?u.1798
M
))) (
Subsemigroup.closure_le: βˆ€ {M : Type ?u.2349} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s ≀ S ↔ s βŠ† ↑S
Subsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
$
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.2389
Additive
M: Type ?u.1798
M
)) #align add_subsemigroup.to_subsemigroup'_closure
AddSubsemigroup.toSubsemigroup'_closure: βˆ€ {M : Type u_1} [inst : Mul M] (S : Set (Additive M)), ↑AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (↑Multiplicative.ofAdd ⁻¹' S)
AddSubsemigroup.toSubsemigroup'_closure
end section variable {
A: Type ?u.2448
A
:
Type _: Type (?u.2448+1)
Type _
} [
Add: Type ?u.3537 β†’ Type ?u.3537
Add
A: Type ?u.2448
A
] /-- Additive subsemigroups of an additive semigroup `A` are isomorphic to multiplicative subsemigroups of `Multiplicative A`. -/ @[
simps: βˆ€ {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)), ↑(↑(RelIso.symm toSubsemigroup) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
simps
] 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.2474
AddSubsemigroup
A: Type ?u.2466
A
≃o
Subsemigroup: (M : Type ?u.2481) β†’ [inst : Mul M] β†’ Type ?u.2481
Subsemigroup
(
Multiplicative: Type ?u.2482 β†’ Type ?u.2482
Multiplicative
A: Type ?u.2466
A
) where toFun
S: ?m.2593
S
:= { carrier :=
Multiplicative.toAdd: {Ξ± : Type ?u.2606} β†’ Multiplicative Ξ± ≃ Ξ±
Multiplicative.toAdd
⁻¹'
S: ?m.2593
S
mul_mem' :=
S: ?m.2593
S
.
add_mem': βˆ€ {M : Type ?u.2776} [inst : Add M] (self : AddSubsemigroup M) {a b : M}, a ∈ self.carrier β†’ b ∈ self.carrier β†’ a + b ∈ self.carrier
add_mem'
} invFun
S: ?m.2820
S
:= { carrier :=
Multiplicative.ofAdd: {Ξ± : Type ?u.2830} β†’ Ξ± ≃ Multiplicative Ξ±
Multiplicative.ofAdd
⁻¹'
S: ?m.2820
S
add_mem' :=
S: ?m.2820
S
.
mul_mem': βˆ€ {M : Type ?u.2975} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a ∈ self.carrier β†’ b ∈ self.carrier β†’ a * b ∈ self.carrier
mul_mem'
} left_inv
_: ?m.3005
_
:=
rfl: βˆ€ {Ξ± : Sort ?u.3007} {a : Ξ±}, a = a
rfl
right_inv
_: ?m.3025
_
:=
rfl: βˆ€ {Ξ± : Sort ?u.3027} {a : Ξ±}, a = a
rfl
map_rel_iff' :=
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align add_subsemigroup.to_subsemigroup
AddSubsemigroup.toSubsemigroup: {A : Type u_1} β†’ [inst : Add A] β†’ AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)
AddSubsemigroup.toSubsemigroup
#align add_subsemigroup.to_subsemigroup_apply_coe
AddSubsemigroup.toSubsemigroup_apply_coe: βˆ€ {A : Type u_1} [inst : Add A] (S : AddSubsemigroup A), ↑(↑AddSubsemigroup.toSubsemigroup S) = ↑Multiplicative.toAdd ⁻¹' ↑S
AddSubsemigroup.toSubsemigroup_apply_coe
#align add_subsemigroup.to_subsemigroup_symm_apply_coe
AddSubsemigroup.toSubsemigroup_symm_apply_coe: βˆ€ {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)), ↑(↑(RelIso.symm AddSubsemigroup.toSubsemigroup) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
AddSubsemigroup.toSubsemigroup_symm_apply_coe
/-- 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 A
Subsemigroup.toAddSubsemigroup'
:
Subsemigroup: (M : Type ?u.3276) β†’ [inst : Mul M] β†’ Type ?u.3276
Subsemigroup
(
Multiplicative: Type ?u.3277 β†’ Type ?u.3277
Multiplicative
A: Type ?u.3268
A
) ≃o
AddSubsemigroup: (M : Type ?u.3294) β†’ [inst : Add M] β†’ Type ?u.3294
AddSubsemigroup
A: Type ?u.3268
A
:=
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
#align subsemigroup.to_add_subsemigroup'
Subsemigroup.toAddSubsemigroup': {A : Type u_1} β†’ [inst : Add A] β†’ Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A
Subsemigroup.toAddSubsemigroup'
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 A
S
:
Set: Type ?u.3540 β†’ Type ?u.3540
Set
A: Type ?u.3534
A
) :
AddSubsemigroup.toSubsemigroup: {A : Type ?u.3544} β†’ [inst : Add A] β†’ AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)
AddSubsemigroup.toSubsemigroup
(
AddSubsemigroup.closure: {M : Type ?u.3624} β†’ [inst : Add M] β†’ Set M β†’ AddSubsemigroup M
AddSubsemigroup.closure
S: Set A
S
) =
Subsemigroup.closure: {M : Type ?u.3657} β†’ [inst : Mul M] β†’ Set M β†’ Subsemigroup M
Subsemigroup.closure
(
Multiplicative.toAdd: {Ξ± : Type ?u.3666} β†’ Multiplicative Ξ± ≃ Ξ±
Multiplicative.toAdd
⁻¹'
S: Set A
S
) :=
le_antisymm: βˆ€ {Ξ± : Type ?u.3767} [inst : PartialOrder Ξ±] {a b : Ξ±}, a ≀ b β†’ b ≀ a β†’ a = b
le_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 ≀ b
l_le
<|
AddSubsemigroup.closure_le: βˆ€ {M : Type ?u.3996} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, closure s ≀ S ↔ s βŠ† ↑S
AddSubsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
$
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.4036
Multiplicative
A: Type ?u.3534
A
)) (
Subsemigroup.closure_le: βˆ€ {M : Type ?u.4096} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, Subsemigroup.closure s ≀ S ↔ s βŠ† ↑S
Subsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
$
AddSubsemigroup.subset_closure: βˆ€ {M : Type ?u.4135} [inst : Add M] {s : Set M}, s βŠ† ↑(closure s)
AddSubsemigroup.subset_closure
(M :=
A: Type ?u.3534
A
)) #align add_subsemigroup.to_subsemigroup_closure
AddSubsemigroup.toSubsemigroup_closure: βˆ€ {A : Type u_1} [inst : Add A] (S : Set A), ↑AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (↑Multiplicative.toAdd ⁻¹' S)
AddSubsemigroup.toSubsemigroup_closure
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: Type ?u.4192 β†’ Type ?u.4192
Set
(
Multiplicative: Type ?u.4193 β†’ Type ?u.4193
Multiplicative
A: Type ?u.4186
A
)) :
Subsemigroup.toAddSubsemigroup': {A : Type ?u.4197} β†’ [inst : Add A] β†’ Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A
Subsemigroup.toAddSubsemigroup'
(
Subsemigroup.closure: {M : Type ?u.4277} β†’ [inst : Mul M] β†’ Set M β†’ Subsemigroup M
Subsemigroup.closure
S) =
AddSubsemigroup.closure: {M : Type ?u.4328} β†’ [inst : Add M] β†’ Set M β†’ AddSubsemigroup M
AddSubsemigroup.closure
(
Additive.ofMul: {Ξ± : Type ?u.4337} β†’ Ξ± ≃ Additive Ξ±
Additive.ofMul
⁻¹' S) :=
le_antisymm: βˆ€ {Ξ± : Type ?u.4425} [inst : PartialOrder Ξ±] {a b : Ξ±}, a ≀ b β†’ b ≀ a β†’ a = b
le_antisymm
(
Subsemigroup.toAddSubsemigroup': {A : Type ?u.4454} β†’ [inst : Add A] β†’ Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A
Subsemigroup.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 ≀ b
l_le
<|
Subsemigroup.closure_le: βˆ€ {M : Type ?u.4653} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s ≀ S ↔ s βŠ† ↑S
Subsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
$
AddSubsemigroup.subset_closure: βˆ€ {M : Type ?u.4696} [inst : Add M] {s : Set M}, s βŠ† ↑(AddSubsemigroup.closure s)
AddSubsemigroup.subset_closure
(M :=
A: Type ?u.4186
A
)) (
AddSubsemigroup.closure_le: βˆ€ {M : Type ?u.4748} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s ≀ S ↔ s βŠ† ↑S
AddSubsemigroup.closure_le
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
$
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.4785
Multiplicative
A: Type ?u.4186
A
)) #align subsemigroup.to_add_subsemigroup'_closure
Subsemigroup.toAddSubsemigroup'_closure: βˆ€ {A : Type u_1} [inst : Add A] (S : Set (Multiplicative A)), ↑Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (↑Additive.ofMul ⁻¹' S)
Subsemigroup.toAddSubsemigroup'_closure
end namespace Subsemigroup open Set /-! ### `comap` and `map` -/ variable [
Mul: Type ?u.15418 β†’ Type ?u.15418
Mul
M: Type ?u.18022
M
] [
Mul: Type ?u.13393 β†’ Type ?u.13393
Mul
N: Type ?u.4835
N
] [
Mul: Type ?u.13396 β†’ Type ?u.13396
Mul
P: Type ?u.7231
P
] (S :
Subsemigroup: (M : Type ?u.16858) β†’ [inst : Mul M] β†’ Type ?u.16858
Subsemigroup
M: Type ?u.4832
M
) /-- The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/ @[
to_additive: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ AddHom M N β†’ AddSubsemigroup N β†’ AddSubsemigroup M
to_additive
"The preimage of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is an `AddSubsemigroup`."] def
comap: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
(f :
M: Type ?u.4863
M
β†’β‚™*
N: Type ?u.4866
N
) (S :
Subsemigroup: (M : Type ?u.4912) β†’ [inst : Mul M] β†’ Type ?u.4912
Subsemigroup
N: Type ?u.4866
N
) :
Subsemigroup: (M : Type ?u.4916) β†’ [inst : Mul M] β†’ Type ?u.4916
Subsemigroup
M: Type ?u.4863
M
where carrier := f ⁻¹' S mul_mem'
ha: ?m.5248
ha
hb: ?m.5251
hb
:= show f (
_: ?m.5475
_
*
_: ?m.5478
_
) ∈ S by
M: Type ?u.4863

N: Type ?u.4866

P: Type ?u.4869

Οƒ: Type ?u.4872

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S


↑f (a✝ * b✝) ∈ S
M: Type ?u.4863

N: Type ?u.4866

P: Type ?u.4869

Οƒ: Type ?u.4872

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S


↑f a✝ * ↑f b✝ ∈ S
M: Type ?u.4863

N: Type ?u.4866

P: Type ?u.4869

Οƒ: Type ?u.4872

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S


↑f a✝ * ↑f b✝ ∈ S
M: Type ?u.4863

N: Type ?u.4866

P: Type ?u.4869

Οƒ: Type ?u.4872

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S


↑f a✝ * ↑f b✝ ∈ S
M: Type ?u.4863

N: Type ?u.4866

P: Type ?u.4869

Οƒ: Type ?u.4872

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup N

a✝, b✝: M

ha: a✝ ∈ ↑f ⁻¹' ↑S

hb: b✝ ∈ ↑f ⁻¹' ↑S


↑f (a✝ * b✝) ∈ S

Goals 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 M
Subsemigroup.comap
#align add_subsemigroup.comap
AddSubsemigroup.comap: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ AddHom M N β†’ AddSubsemigroup N β†’ AddSubsemigroup M
AddSubsemigroup.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), ↑(AddSubsemigroup.comap f S) = ↑f ⁻¹' ↑S
to_additive
(attr := simp)] theorem
coe_comap: βˆ€ (S : Subsemigroup N) (f : M β†’β‚™* N), ↑(comap f S) = ↑f ⁻¹' ↑S
coe_comap
(S :
Subsemigroup: (M : Type ?u.6112) β†’ [inst : Mul M] β†’ Type ?u.6112
Subsemigroup
N: Type ?u.6084
N
) (f :
M: Type ?u.6081
M
β†’β‚™*
N: Type ?u.6084
N
) : (S.
comap: {M : Type ?u.6138} β†’ {N : Type ?u.6137} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f :
Set: Type ?u.6136 β†’ Type ?u.6136
Set
M: Type ?u.6081
M
) = f ⁻¹' S :=
rfl: βˆ€ {Ξ± : Sort ?u.6616} {a : Ξ±}, a = a
rfl
#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 ⁻¹' ↑S
Subsemigroup.coe_comap
#align add_subsemigroup.coe_comap
AddSubsemigroup.coe_comap: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup N) (f : AddHom M N), ↑(AddSubsemigroup.comap f S) = ↑f ⁻¹' ↑S
AddSubsemigroup.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 ∈ S
to_additive
(attr := simp)] theorem
mem_comap: βˆ€ {S : Subsemigroup N} {f : M β†’β‚™* N} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
mem_comap
{S :
Subsemigroup: (M : Type ?u.6736) β†’ [inst : Mul M] β†’ Type ?u.6736
Subsemigroup
N: Type ?u.6708
N
} {f :
M: Type ?u.6705
M
β†’β‚™*
N: Type ?u.6708
N
} {
x: M
x
:
M: Type ?u.6705
M
} :
x: M
x
∈ S.
comap: {M : Type ?u.6766} β†’ {N : Type ?u.6765} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f ↔ f
x: M
x
∈ S :=
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.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 ∈ S
Subsemigroup.mem_comap
#align add_subsemigroup.mem_comap
AddSubsemigroup.mem_comap: βˆ€ {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 ∈ S
AddSubsemigroup.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) (g : AddHom N P) (f : AddHom M N), AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (AddHom.comp g f) S
to_additive
] 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) S
comap_comap
(S :
Subsemigroup: (M : Type ?u.7256) β†’ [inst : Mul M] β†’ Type ?u.7256
Subsemigroup
P: Type ?u.7231
P
) (g :
N: Type ?u.7228
N
β†’β‚™*
P: Type ?u.7231
P
) (f :
M: Type ?u.7225
M
β†’β‚™*
N: Type ?u.7228
N
) : (S.
comap: {M : Type ?u.7292} β†’ {N : Type ?u.7291} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
g).
comap: {M : Type ?u.7314} β†’ {N : Type ?u.7313} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S.
comap: {M : Type ?u.7336} β†’ {N : Type ?u.7335} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
(g.
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 β†’β‚™* P
comp
f) :=
rfl: βˆ€ {Ξ± : Sort ?u.7404} {a : Ξ±}, a = a
rfl
#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) S
Subsemigroup.comap_comap
#align add_subsemigroup.comap_comap
AddSubsemigroup.comap_comap: βˆ€ {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) (g : AddHom N P) (f : AddHom M N), AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (AddHom.comp g f) S
AddSubsemigroup.comap_comap
@[
to_additive: βˆ€ {P : Type u_1} [inst : Add P] (S : AddSubsemigroup P), AddSubsemigroup.comap (AddHom.id P) S = S
to_additive
(attr := simp)] theorem
comap_id: βˆ€ {P : Type u_1} [inst : Mul P] (S : Subsemigroup P), comap (MulHom.id P) S = S
comap_id
(S :
Subsemigroup: (M : Type ?u.7545) β†’ [inst : Mul M] β†’ Type ?u.7545
Subsemigroup
P: Type ?u.7520
P
) : S.
comap: {M : Type ?u.7557} β†’ {N : Type ?u.7556} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
(
MulHom.id: (M : Type ?u.7568) β†’ [inst : Mul M] β†’ M β†’β‚™* M
MulHom.id
_: Type ?u.7568
_
) = S :=
ext: βˆ€ {M : Type ?u.7624} [inst : Mul M] {S T : Subsemigroup M}, (βˆ€ (x : M), x ∈ S ↔ x ∈ T) β†’ S = T
ext
(

Goals accomplished! πŸ™
M: Type ?u.7514

N: Type ?u.7517

P: Type u_1

Οƒ: Type ?u.7523

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

S: Subsemigroup P


βˆ€ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S

Goals accomplished! πŸ™
) #align subsemigroup.comap_id
Subsemigroup.comap_id: βˆ€ {P : Type u_1} [inst : Mul P] (S : Subsemigroup P), comap (MulHom.id P) S = S
Subsemigroup.comap_id
#align add_subsemigroup.comap_id
AddSubsemigroup.comap_id: βˆ€ {P : Type u_1} [inst : Add P] (S : AddSubsemigroup P), AddSubsemigroup.comap (AddHom.id P) S = S
AddSubsemigroup.comap_id
/-- The image of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/ @[
to_additive: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ AddHom M N β†’ AddSubsemigroup M β†’ AddSubsemigroup N
to_additive
"The image of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is an `AddSubsemigroup`."] def
map: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
(f :
M: Type ?u.8706
M
β†’β‚™*
N: Type ?u.8709
N
) (S :
Subsemigroup: (M : Type ?u.8755) β†’ [inst : Mul M] β†’ Type ?u.8755
Subsemigroup
M: Type ?u.8706
M
) :
Subsemigroup: (M : Type ?u.8759) β†’ [inst : Mul M] β†’ Type ?u.8759
Subsemigroup
N: Type ?u.8709
N
where carrier := f '' S mul_mem' :=

Goals accomplished! πŸ™
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M


βˆ€ {a b : N}, a ∈ ↑f '' ↑S β†’ b ∈ ↑f '' ↑S β†’ a * b ∈ ↑f '' ↑S
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


intro.intro.intro.intro
↑f x * ↑f y ∈ ↑f '' ↑S
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M


βˆ€ {a b : N}, a ∈ ↑f '' ↑S β†’ b ∈ ↑f '' ↑S β†’ a * b ∈ ↑f '' ↑S
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


intro.intro.intro.intro
↑f x * ↑f y ∈ ↑f '' ↑S

Goals accomplished! πŸ™
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


↑f (x * y) = ↑f x * ↑f y
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


↑f (x * y) = ↑f x * ↑f y
M: Type ?u.8706

N: Type ?u.8709

P: Type ?u.8712

Οƒ: Type ?u.8715

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

f: M β†’β‚™* N

S: Subsemigroup M

x: M

hx: x ∈ ↑S

y: M

hy: 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 N
Subsemigroup.map
#align add_subsemigroup.map
AddSubsemigroup.map: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ AddHom M N β†’ AddSubsemigroup M β†’ AddSubsemigroup N
AddSubsemigroup.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), ↑(AddSubsemigroup.map f S) = ↑f '' ↑S
to_additive
(attr := simp)] 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 '' ↑S
coe_map
(f :
M: Type ?u.9768
M
β†’β‚™*
N: Type ?u.9771
N
) (S :
Subsemigroup: (M : Type ?u.9817) β†’ [inst : Mul M] β†’ Type ?u.9817
Subsemigroup
M: Type ?u.9768
M
) : (S.
map: {M : Type ?u.9825} β†’ {N : Type ?u.9824} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f :
Set: Type ?u.9823 β†’ Type ?u.9823
Set
N: Type ?u.9771
N
) = f '' S :=
rfl: βˆ€ {Ξ± : Sort ?u.10303} {a : Ξ±}, a = a
rfl
#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 '' ↑S
Subsemigroup.coe_map
#align add_subsemigroup.coe_map
AddSubsemigroup.coe_map: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) (S : AddSubsemigroup M), ↑(AddSubsemigroup.map f S) = ↑f '' ↑S
AddSubsemigroup.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 = y
to_additive
(attr := simp)] theorem
mem_map: βˆ€ {f : M β†’β‚™* N} {S : Subsemigroup M} {y : N}, y ∈ map f S ↔ βˆƒ x, x ∈ S ∧ ↑f x = y
mem_map
{f :
M: Type ?u.10392
M
β†’β‚™*
N: Type ?u.10395
N
} {S :
Subsemigroup: (M : Type ?u.10441) β†’ [inst : Mul M] β†’ Type ?u.10441
Subsemigroup
M: Type ?u.10392
M
} {
y: N
y
:
N: Type ?u.10395
N
} :
y: N
y
∈ S.
map: {M : Type ?u.10453} β†’ {N : Type ?u.10452} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ↔ βˆƒ
x: ?m.10540
x
∈ S, f
x: ?m.10540
x
=
y: N
y
:=
mem_image: βˆ€ {Ξ± : Type ?u.10800} {Ξ² : Type ?u.10801} (f : Ξ± β†’ Ξ²) (s : Set Ξ±) (y : Ξ²), y ∈ f '' s ↔ βˆƒ x, x ∈ s ∧ f x = y
mem_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 = y
Subsemigroup.mem_map
#align add_subsemigroup.mem_map
AddSubsemigroup.mem_map: βˆ€ {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 = y
AddSubsemigroup.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}, x ∈ S β†’ ↑f x ∈ AddSubsemigroup.map f S
to_additive
] theorem
mem_map_of_mem: βˆ€ (f : M β†’β‚™* N) {S : Subsemigroup M} {x : M}, x ∈ S β†’ ↑f x ∈ map f S
mem_map_of_mem
(f :
M: Type ?u.10966
M
β†’β‚™*
N: Type ?u.10969
N
) {S :
Subsemigroup: (M : Type ?u.11015) β†’ [inst : Mul M] β†’ Type ?u.11015
Subsemigroup
M: Type ?u.10966
M
} {
x: M
x
:
M: Type ?u.10966
M
} (
hx: x ∈ S
hx
:
x: M
x
∈ S) : f
x: M
x
∈ S.
map: {M : Type ?u.11306} β†’ {N : Type ?u.11305} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f :=
mem_image_of_mem: βˆ€ {Ξ± : Type ?u.11392} {Ξ² : Type ?u.11393} (f : Ξ± β†’ Ξ²) {x : Ξ±} {a : Set Ξ±}, x ∈ a β†’ f x ∈ f '' a
mem_image_of_mem
f
hx: x ∈ S
hx
#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 S
Subsemigroup.mem_map_of_mem
#align add_subsemigroup.mem_map_of_mem
AddSubsemigroup.mem_map_of_mem: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) {S : AddSubsemigroup M} {x : M}, x ∈ S β†’ ↑f x ∈ AddSubsemigroup.map f S
AddSubsemigroup.mem_map_of_mem
@[
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 : { x // x ∈ S }), ↑f ↑x ∈ AddSubsemigroup.map f S
to_additive
] theorem
apply_coe_mem_map: βˆ€ (f : M β†’β‚™* N) (S : Subsemigroup M) (x : { x // x ∈ S }), ↑f ↑x ∈ map f S
apply_coe_mem_map
(f :
M: Type ?u.11705
M
β†’β‚™*
N: Type ?u.11708
N
) (S :
Subsemigroup: (M : Type ?u.11754) β†’ [inst : Mul M] β†’ Type ?u.11754
Subsemigroup
M: Type ?u.11705
M
) (
x: { x // x ∈ S }
x
: S) : f
x: { x // x ∈ S }
x
∈ S.
map: {M : Type ?u.12142} β†’ {N : Type ?u.12141} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f :=
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 S
mem_map_of_mem
f
x: { x // x ∈ S }
x
.
prop: βˆ€ {Ξ± : Sort ?u.12277} {p : Ξ± β†’ Prop} (x : Subtype p), p ↑x
prop
#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 S
Subsemigroup.apply_coe_mem_map
#align add_subsemigroup.apply_coe_mem_map
AddSubsemigroup.apply_coe_mem_map: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N) (S : AddSubsemigroup M) (x : { x // x ∈ S }), ↑f ↑x ∈ AddSubsemigroup.map f S
AddSubsemigroup.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) (g : AddHom N P) (f : AddHom M N), AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (AddHom.comp g f) S
to_additive
] 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) S
map_map
(g :
N: Type ?u.12339
N
β†’β‚™*
P: Type ?u.12342
P
) (f :
M: Type ?u.12336
M
β†’β‚™*
N: Type ?u.12339
N
) : (S.
map: {M : Type ?u.12399} β†’ {N : Type ?u.12398} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
map: {M : Type ?u.12421} β†’ {N : Type ?u.12420} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
g = S.
map: {M : Type ?u.12443} β†’ {N : Type ?u.12442} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
(g.
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 β†’β‚™* P
comp
f) :=
SetLike.coe_injective: βˆ€ {A : Type ?u.12510} {B : Type ?u.12511} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.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)) '' s
image_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) S
Subsemigroup.map_map
#align add_subsemigroup.map_map
AddSubsemigroup.map_map: βˆ€ {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) (g : AddHom N P) (f : AddHom M N), AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (AddHom.comp g f) S
AddSubsemigroup.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 ∈ S
to_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 ∈ S
mem_map_iff_mem
{f :
M: Type ?u.12671
M
β†’β‚™*
N: Type ?u.12674
N
} (
hf: Function.Injective ↑f
hf
:
Function.Injective: {Ξ± : Sort ?u.12721} β†’ {Ξ² : Sort ?u.12720} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective
f) {S :
Subsemigroup: (M : Type ?u.12953) β†’ [inst : Mul M] β†’ Type ?u.12953
Subsemigroup
M: Type ?u.12671
M
} {
x: M
x
:
M: Type ?u.12671
M
} : f
x: M
x
∈ S.
map: {M : Type ?u.13166} β†’ {N : Type ?u.13165} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ↔
x: M
x
∈ S :=
hf: Function.Injective ↑f
hf
.
mem_set_image: βˆ€ {Ξ± : Type ?u.13275} {Ξ² : Type ?u.13276} {f : Ξ± β†’ Ξ²}, Function.Injective f β†’ βˆ€ {s : Set Ξ±} {a : Ξ±}, f a ∈ f '' s ↔ a ∈ s
mem_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 ∈ S
Subsemigroup.mem_map_iff_mem
#align add_subsemigroup.mem_map_iff_mem
AddSubsemigroup.mem_map_iff_mem: βˆ€ {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 ∈ S
AddSubsemigroup.mem_map_iff_mem
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {T : AddSubsemigroup N}, AddSubsemigroup.map f S ≀ T ↔ S ≀ AddSubsemigroup.comap f T
to_additive
] theorem
map_le_iff_le_comap: βˆ€ {f : M β†’β‚™* N} {S : Subsemigroup M} {T : Subsemigroup N}, map f S ≀ T ↔ S ≀ comap f T
map_le_iff_le_comap
{f :
M: Type ?u.13378
M
β†’β‚™*
N: Type ?u.13381
N
} {S :
Subsemigroup: (M : Type ?u.13427) β†’ [inst : Mul M] β†’ Type ?u.13427
Subsemigroup
M: Type ?u.13378
M
} {T :
Subsemigroup: (M : Type ?u.13431) β†’ [inst : Mul M] β†’ Type ?u.13431
Subsemigroup
N: Type ?u.13381
N
} : S.
map: {M : Type ?u.13437} β†’ {N : Type ?u.13436} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ≀ T ↔ S ≀ T.
comap: {M : Type ?u.13502} β†’ {N : Type ?u.13501} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f :=
image_subset_iff: βˆ€ {Ξ± : Type ?u.13561} {Ξ² : Type ?u.13562} {s : Set Ξ±} {t : Set Ξ²} {f : Ξ± β†’ Ξ²}, f '' s βŠ† t ↔ s βŠ† f ⁻¹' t
image_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 T
Subsemigroup.map_le_iff_le_comap
#align add_subsemigroup.map_le_iff_le_comap
AddSubsemigroup.map_le_iff_le_comap: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {T : AddSubsemigroup N}, AddSubsemigroup.map f S ≀ T ↔ S ≀ AddSubsemigroup.comap f T
AddSubsemigroup.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), GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
to_additive
] 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: Type ?u.13669
M
β†’β‚™*
N: Type ?u.13672
N
) :
GaloisConnection: {Ξ± : Type ?u.13719} β†’ {Ξ² : Type ?u.13718} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ (Ξ² β†’ Ξ±) β†’ Prop
GaloisConnection
(
map: {M : Type ?u.13755} β†’ {N : Type ?u.13754} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f) (
comap: {M : Type ?u.13818} β†’ {N : Type ?u.13817} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f) := 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 T
map_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
#align add_subsemigroup.gc_map_comap
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)
AddSubsemigroup.gc_map_comap
@[
to_additive: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N}, S ≀ AddSubsemigroup.comap f T β†’ AddSubsemigroup.map f S ≀ T
to_additive
] theorem
map_le_of_le_comap: βˆ€ {T : Subsemigroup N} {f : M β†’β‚™* N}, S ≀ comap f T β†’ map f S ≀ T
map_le_of_le_comap
{T :
Subsemigroup: (M : Type ?u.14097) β†’ [inst : Mul M] β†’ Type ?u.14097
Subsemigroup
N: Type ?u.14069
N
} {f :
M: Type ?u.14066
M
β†’β‚™*
N: Type ?u.14069
N
} : S ≀ T.
comap: {M : Type ?u.14122} β†’ {N : Type ?u.14121} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f β†’ S.
map: {M : Type ?u.14188} β†’ {N : Type ?u.14187} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ≀ T := (
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).
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 ≀ b
l_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 ≀ T
Subsemigroup.map_le_of_le_comap
#align add_subsemigroup.map_le_of_le_comap
AddSubsemigroup.map_le_of_le_comap: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N}, S ≀ AddSubsemigroup.comap f T β†’ AddSubsemigroup.map f S ≀ T
AddSubsemigroup.map_le_of_le_comap
@[
to_additive: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.map f S ≀ T β†’ S ≀ AddSubsemigroup.comap f T
to_additive
] 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 T
le_comap_of_map_le
{T :
Subsemigroup: (M : Type ?u.14463) β†’ [inst : Mul M] β†’ Type ?u.14463
Subsemigroup
N: Type ?u.14435
N
} {f :
M: Type ?u.14432
M
β†’β‚™*
N: Type ?u.14435
N
} : S.
map: {M : Type ?u.14488} β†’ {N : Type ?u.14487} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ≀ T β†’ S ≀ T.
comap: {M : Type ?u.14554} β†’ {N : Type ?u.14553} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f := (
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).
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 b
le_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 T
Subsemigroup.le_comap_of_map_le
#align add_subsemigroup.le_comap_of_map_le
AddSubsemigroup.le_comap_of_map_le: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.map f S ≀ T β†’ S ≀ AddSubsemigroup.comap f T
AddSubsemigroup.le_comap_of_map_le
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : AddHom M N}, S ≀ AddSubsemigroup.comap f (AddSubsemigroup.map f S)
to_additive
] theorem
le_comap_map: βˆ€ {f : M β†’β‚™* N}, S ≀ comap f (map f S)
le_comap_map
{f :
M: Type ?u.14798
M
β†’β‚™*
N: Type ?u.14801
N
} : S ≀ (S.
map: {M : Type ?u.14849} β†’ {N : Type ?u.14848} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.14871} β†’ {N : Type ?u.14870} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f := (
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).
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
#align add_subsemigroup.le_comap_map
AddSubsemigroup.le_comap_map: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : AddHom M N}, S ≀ AddSubsemigroup.comap f (AddSubsemigroup.map f S)
AddSubsemigroup.le_comap_map
@[
to_additive: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≀ S
to_additive
] 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) ≀ S
map_comap_le
{S :
Subsemigroup: (M : Type ?u.15128) β†’ [inst : Mul M] β†’ Type ?u.15128
Subsemigroup
N: Type ?u.15100
N
} {f :
M: Type ?u.15097
M
β†’β‚™*
N: Type ?u.15100
N
} : (S.
comap: {M : Type ?u.15152} β†’ {N : Type ?u.15151} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f).
map: {M : Type ?u.15174} β†’ {N : Type ?u.15173} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ≀ S := (
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).
l_u_le: βˆ€ {Ξ± : Type ?u.15265} {Ξ² : Type ?u.15264} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±}, GaloisConnection l u β†’ βˆ€ (a : Ξ²), l (u a) ≀ a
l_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) ≀ S
Subsemigroup.map_comap_le
#align add_subsemigroup.map_comap_le
AddSubsemigroup.map_comap_le: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≀ S
AddSubsemigroup.map_comap_le
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Monotone (AddSubsemigroup.map f)
to_additive
] theorem
monotone_map: βˆ€ {f : M β†’β‚™* N}, Monotone (map f)
monotone_map
{f :
M: Type ?u.15406
M
β†’β‚™*
N: Type ?u.15409
N
} :
Monotone: {Ξ± : Type ?u.15456} β†’ {Ξ² : Type ?u.15455} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone
(
map: {M : Type ?u.15492} β†’ {N : Type ?u.15491} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f) := (
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).
monotone_l: βˆ€ {Ξ± : Type ?u.15652} {Ξ² : Type ?u.15651} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±}, GaloisConnection l u β†’ Monotone l
monotone_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
#align add_subsemigroup.monotone_map
AddSubsemigroup.monotone_map: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Monotone (AddSubsemigroup.map f)
AddSubsemigroup.monotone_map
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Monotone (AddSubsemigroup.comap f)
to_additive
] 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: Type ?u.15784
M
β†’β‚™*
N: Type ?u.15787
N
} :
Monotone: {Ξ± : Type ?u.15834} β†’ {Ξ² : Type ?u.15833} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone
(
comap: {M : Type ?u.15870} β†’ {N : Type ?u.15869} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f) := (
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).
monotone_u: βˆ€ {Ξ± : Type ?u.16030} {Ξ² : Type ?u.16029} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±}, GaloisConnection l u β†’ Monotone u
monotone_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
#align add_subsemigroup.monotone_comap
AddSubsemigroup.monotone_comap: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Monotone (AddSubsemigroup.comap f)
AddSubsemigroup.monotone_comap
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : AddHom M N}, AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S
to_additive
(attr := simp)] theorem
map_comap_map: βˆ€ {f : M β†’β‚™* N}, map f (comap f (map f S)) = map f S
map_comap_map
{f :
M: Type ?u.16162
M
β†’β‚™*
N: Type ?u.16165
N
} : ((S.
map: {M : Type ?u.16213} β†’ {N : Type ?u.16212} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.16235} β†’ {N : Type ?u.16234} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f).
map: {M : Type ?u.16253} β†’ {N : Type ?u.16252} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f = S.
map: {M : Type ?u.16269} β†’ {N : Type ?u.16268} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f := (
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).
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 a
l_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 S
Subsemigroup.map_comap_map
#align add_subsemigroup.map_comap_map
AddSubsemigroup.map_comap_map: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S : AddSubsemigroup M) {f : AddHom M N}, AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S
AddSubsemigroup.map_comap_map
@[
to_additive: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap f S
to_additive
(attr := simp)] theorem
comap_map_comap: βˆ€ {S : Subsemigroup N} {f : M β†’β‚™* N}, comap f (map f (comap f S)) = comap f S
comap_map_comap
{S :
Subsemigroup: (M : Type ?u.16529) β†’ [inst : Mul M] β†’ Type ?u.16529
Subsemigroup
N: Type ?u.16501
N
} {f :
M: Type ?u.16498
M
β†’β‚™*
N: Type ?u.16501
N
} : ((S.
comap: {M : Type ?u.16553} β†’ {N : Type ?u.16552} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f).
map: {M : Type ?u.16575} β†’ {N : Type ?u.16574} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.16593} β†’ {N : Type ?u.16592} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S.
comap: {M : Type ?u.16609} β†’ {N : Type ?u.16608} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f := (
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).
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 b
u_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 S
Subsemigroup.comap_map_comap
#align add_subsemigroup.comap_map_comap
AddSubsemigroup.comap_map_comap: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : AddHom M N}, AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap f S
AddSubsemigroup.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), AddSubsemigroup.map f (S βŠ” T) = AddSubsemigroup.map f S βŠ” AddSubsemigroup.map f T
to_additive
] 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 T
map_sup
(S T :
Subsemigroup: (M : Type ?u.16868) β†’ [inst : Mul M] β†’ Type ?u.16868
Subsemigroup
M: Type ?u.16837
M
) (f :
M: Type ?u.16837
M
β†’β‚™*
N: Type ?u.16840
N
) : (S βŠ” T).
map: {M : Type ?u.16932} β†’ {N : Type ?u.16931} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f = S.
map: {M : Type ?u.16955} β†’ {N : Type ?u.16954} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f βŠ” T.
map: {M : Type ?u.17013} β†’ {N : Type ?u.17012} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f := (
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).
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 T
Subsemigroup.map_sup
#align add_subsemigroup.map_sup
AddSubsemigroup.map_sup: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup M) (f : AddHom M N), AddSubsemigroup.map f (S βŠ” T) = AddSubsemigroup.map f S βŠ” AddSubsemigroup.map f T
AddSubsemigroup.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) (s : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.map f (iSup s) = ⨆ i, AddSubsemigroup.map f (s i)
to_additive
] 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.17291
Sort
Sort _: Type ?u.17291
_
} (f :
M: Type ?u.17260
M
β†’β‚™*
N: Type ?u.17263
N
) (
s: ΞΉ β†’ Subsemigroup M
s
:
ΞΉ: Sort ?u.17291
ΞΉ
β†’
Subsemigroup: (M : Type ?u.17314) β†’ [inst : Mul M] β†’ Type ?u.17314
Subsemigroup
M: Type ?u.17260
M
) : (
iSup: {Ξ± : Type ?u.17320} β†’ [inst : SupSet Ξ±] β†’ {ΞΉ : Sort ?u.17319} β†’ (ΞΉ β†’ Ξ±) β†’ Ξ±
iSup
s: ΞΉ β†’ Subsemigroup M
s
).
map: {M : Type ?u.17351} β†’ {N : Type ?u.17350} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f = ⨆
i: ?m.17376
i
, (
s: ΞΉ β†’ Subsemigroup M
s
i: ?m.17376
i
).
map: {M : Type ?u.17379} β†’ {N : Type ?u.17378} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f := (
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).
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) (s : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.map f (iSup s) = ⨆ i, AddSubsemigroup.map f (s i)
AddSubsemigroup.map_iSup
@[
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), AddSubsemigroup.comap f (S βŠ“ T) = AddSubsemigroup.comap f S βŠ“ AddSubsemigroup.comap f T
to_additive
] 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 T
comap_inf
(S T :
Subsemigroup: (M : Type ?u.17674) β†’ [inst : Mul M] β†’ Type ?u.17674
Subsemigroup
N: Type ?u.17636
N
) (f :
M: Type ?u.17633
M
β†’β‚™*
N: Type ?u.17636
N
) : (S βŠ“ T).
comap: {M : Type ?u.17708} β†’ {N : Type ?u.17707} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S.
comap: {M : Type ?u.17731} β†’ {N : Type ?u.17730} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f βŠ“ T.
comap: {M : Type ?u.17789} β†’ {N : Type ?u.17788} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f := (
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).
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 T
Subsemigroup.comap_inf
#align add_subsemigroup.comap_inf
AddSubsemigroup.comap_inf: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup N) (f : AddHom M N), AddSubsemigroup.comap f (S βŠ“ T) = AddSubsemigroup.comap f S βŠ“ AddSubsemigroup.comap f T
AddSubsemigroup.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) (s : ΞΉ β†’ AddSubsemigroup N), AddSubsemigroup.comap f (iInf s) = β¨… i, AddSubsemigroup.comap f (s i)
to_additive
] 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.18053
Sort
Sort _: Type ?u.18053
_
} (f :
M: Type ?u.18022
M
β†’β‚™*
N: Type ?u.18025
N
) (
s: ΞΉ β†’ Subsemigroup N
s
:
ΞΉ: Sort ?u.18053
ΞΉ
β†’
Subsemigroup: (M : Type ?u.18076) β†’ [inst : Mul M] β†’ Type ?u.18076
Subsemigroup
N: Type ?u.18025
N
) : (
iInf: {Ξ± : Type ?u.18082} β†’ [inst : InfSet Ξ±] β†’ {ΞΉ : Sort ?u.18081} β†’ (ΞΉ β†’ Ξ±) β†’ Ξ±
iInf
s: ΞΉ β†’ Subsemigroup N
s
).
comap: {M : Type ?u.18104} β†’ {N : Type ?u.18103} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = β¨…
i: ?m.18129
i
, (
s: ΞΉ β†’ Subsemigroup N
s
i: ?m.18129
i
).
comap: {M : Type ?u.18132} β†’ {N : Type ?u.18131} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f := (
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).
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) (s : ΞΉ β†’ AddSubsemigroup N), AddSubsemigroup.comap f (iInf s) = β¨… i, AddSubsemigroup.comap f (s i)
AddSubsemigroup.comap_iInf
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N), AddSubsemigroup.map f βŠ₯ = βŠ₯
to_additive
(attr := simp)] theorem
map_bot: βˆ€ (f : M β†’β‚™* N), map f βŠ₯ = βŠ₯
map_bot
(f :
M: Type ?u.18387
M
β†’β‚™*
N: Type ?u.18390
N
) : (
βŠ₯: ?m.18441
βŠ₯
:
Subsemigroup: (M : Type ?u.18438) β†’ [inst : Mul M] β†’ Type ?u.18438
Subsemigroup
M: Type ?u.18387
M
).
map: {M : Type ?u.18481} β†’ {N : Type ?u.18480} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f =
βŠ₯: ?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).
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
#align add_subsemigroup.map_bot
AddSubsemigroup.map_bot: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N), AddSubsemigroup.map f βŠ₯ = βŠ₯
AddSubsemigroup.map_bot
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N), AddSubsemigroup.comap f ⊀ = ⊀
to_additive
(attr := simp)] 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: Type ?u.18832
M
β†’β‚™*
N: Type ?u.18835
N
) : (
⊀: ?m.18886
⊀
:
Subsemigroup: (M : Type ?u.18883) β†’ [inst : Mul M] β†’ Type ?u.18883
Subsemigroup
N: Type ?u.18835
N
).
comap: {M : Type ?u.18921} β†’ {N : Type ?u.18920} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f =
⊀: ?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).
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
#align add_subsemigroup.comap_top
AddSubsemigroup.comap_top: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : AddHom M N), AddSubsemigroup.comap f ⊀ = ⊀
AddSubsemigroup.comap_top
@[
to_additive: βˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.map (AddHom.id M) S = S
to_additive
(attr := simp)] theorem
map_id: βˆ€ (S : Subsemigroup M), map (MulHom.id M) S = S
map_id
(S :
Subsemigroup: (M : Type ?u.19292) β†’ [inst : Mul M] β†’ Type ?u.19292
Subsemigroup
M: Type ?u.19261
M
) : S.
map: {M : Type ?u.19304} β†’ {N : Type ?u.19303} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
(
MulHom.id: (M : Type ?u.19315) β†’ [inst : Mul M] β†’ M β†’β‚™* M
MulHom.id
M: Type ?u.19261
M
) = S :=
ext: βˆ€ {M : Type ?u.19330} [inst : Mul M] {S T : Subsemigroup M}, (βˆ€ (x : M), x ∈ S ↔ x ∈ T) β†’ S = T
ext
fun
_: ?m.19362
_
=> ⟨fun ⟨
_: ?m.19362
_
,
h: x✝¹ ∈ ↑S
h
,
rfl: βˆ€ {Ξ± : Sort ?u.19376} {a : Ξ±}, a = a
rfl
⟩ =>
h: x✝¹ ∈ ↑S
h
, fun
h: ?m.19677
h
=> ⟨
_: ?m.19684
_
,
h: ?m.19677
h
,
rfl: βˆ€ {Ξ± : Sort ?u.19709} {a : Ξ±}, a = a
rfl
⟩⟩ #align subsemigroup.map_id
Subsemigroup.map_id: βˆ€ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), map (MulHom.id M) S = S
Subsemigroup.map_id
#align add_subsemigroup.map_id
AddSubsemigroup.map_id: βˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.map (AddHom.id M) S = S
AddSubsemigroup.map_id
section GaloisCoinsertion variable {
ΞΉ: Type ?u.22089
ΞΉ
:
Type _: Type (?u.23689+1)
Type _
} {f :
M: Type ?u.20133
M
β†’β‚™*
N: Type ?u.19857
N
} (
hf: Function.Injective ↑f
hf
:
Function.Injective: {Ξ± : Sort ?u.23705} β†’ {Ξ² : Sort ?u.23704} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective
f) --include hf /-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is 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 β†’ 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 N
map
f) (
comap: {M : Type ?u.20524} β†’ {N : Type ?u.20523} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f) := (
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).
toGaloisCoinsertion: {Ξ± : Type ?u.20654} β†’ {Ξ² : Type ?u.20653} β†’ [inst : Preorder Ξ±] β†’ [inst_1 : Preorder Ξ²] β†’ {l : Ξ± β†’ Ξ²} β†’ {u : Ξ² β†’ Ξ±} β†’ GaloisConnection l u β†’ (βˆ€ (a : Ξ±), u (l a) ≀ a) β†’ GaloisCoinsertion l u
toGaloisCoinsertion
fun
S: ?m.20689
S
x: ?m.20692
x
=>

Goals accomplished! πŸ™
M: Type ?u.20133

N: Type ?u.20136

P: Type ?u.20139

Οƒ: Type ?u.20142

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

ΞΉ: Type ?u.20164

f: M β†’β‚™* N

hf: Function.Injective ↑f

S: Subsemigroup M

x: M


x ∈ comap f (map f S) β†’ x ∈ S

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
#align add_subsemigroup.gci_map_comap
AddSubsemigroup.gciMapComap: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ {f : AddHom M N} β†’ Function.Injective ↑f β†’ GaloisCoinsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
AddSubsemigroup.gciMapComap
@[
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), AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S
to_additive
] theorem
comap_map_eq_of_injective: βˆ€ (S : Subsemigroup M), comap f (map f S) = S
comap_map_eq_of_injective
(S :
Subsemigroup: (M : Type ?u.22337) β†’ [inst : Mul M] β†’ Type ?u.22337
Subsemigroup
M: Type ?u.22058
M
) : (S.
map: {M : Type ?u.22349} β†’ {N : Type ?u.22348} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.22377} β†’ {N : Type ?u.22376} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S := (
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 ↑f
hf
).
u_l_eq: βˆ€ {Ξ± : Type ?u.22442} {Ξ² : Type ?u.22441} {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²], GaloisCoinsertion l u β†’ βˆ€ (a : Ξ±), u (l a) = a
u_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) = S
Subsemigroup.comap_map_eq_of_injective
#align add_subsemigroup.comap_map_eq_of_injective
AddSubsemigroup.comap_map_eq_of_injective: βˆ€ {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), AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S
AddSubsemigroup.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}, Function.Injective ↑f β†’ Function.Surjective (AddSubsemigroup.comap f)
to_additive
] 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} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Surjective
(
comap: {M : Type ?u.22872} β†’ {N : Type ?u.22871} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f) := (
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 ↑f
hf
).
u_surjective: βˆ€ {Ξ± : Type ?u.22993} {Ξ² : Type ?u.22992} {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²], GaloisCoinsertion l u β†’ Function.Surjective u
u_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
#align add_subsemigroup.comap_surjective_of_injective
AddSubsemigroup.comap_surjective_of_injective: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ Function.Surjective (AddSubsemigroup.comap f)
AddSubsemigroup.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}, Function.Injective ↑f β†’ Function.Injective (AddSubsemigroup.map f)
to_additive
] theorem
map_injective_of_injective: Function.Injective (map f)
map_injective_of_injective
:
Function.Injective: {Ξ± : Sort ?u.23404} β†’ {Ξ² : Sort ?u.23403} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Injective
(
map: {M : Type ?u.23408} β†’ {N : Type ?u.23407} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f) := (
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 ↑f
hf
).
l_injective: βˆ€ {Ξ± : Type ?u.23528} {Ξ² : Type ?u.23527} {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±} [inst : PartialOrder Ξ±] [inst_1 : Preorder Ξ²], GaloisCoinsertion l u β†’ Function.Injective l
l_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
#align add_subsemigroup.map_injective_of_injective
AddSubsemigroup.map_injective_of_injective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ Function.Injective (AddSubsemigroup.map f)
AddSubsemigroup.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 β†’ βˆ€ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S βŠ“ AddSubsemigroup.map f T) = S βŠ“ T
to_additive
] 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 βŠ“ T
comap_inf_map_of_injective
(S T :
Subsemigroup: (M : Type ?u.23947) β†’ [inst : Mul M] β†’ Type ?u.23947
Subsemigroup
M: Type ?u.23658
M
) : (S.
map: {M : Type ?u.23956} β†’ {N : Type ?u.23955} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f βŠ“ T.
map: {M : Type ?u.24026} β†’ {N : Type ?u.24025} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.24093} β†’ {N : Type ?u.24092} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S βŠ“ T := (
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 ↑f
hf
).
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 βŠ“ b
u_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 βŠ“ T
Subsemigroup.comap_inf_map_of_injective
#align add_subsemigroup.comap_inf_map_of_injective
AddSubsemigroup.comap_inf_map_of_injective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ βˆ€ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S βŠ“ AddSubsemigroup.map f T) = S βŠ“ T
AddSubsemigroup.comap_inf_map_of_injective
@[
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 β†’ βˆ€ (S : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.comap f (β¨… i, AddSubsemigroup.map f (S i)) = iInf S
to_additive
] theorem
comap_iInf_map_of_injective: βˆ€ (S : ΞΉ β†’ Subsemigroup M), comap f (β¨… i, map f (S i)) = iInf S
comap_iInf_map_of_injective
(
S: ΞΉ β†’ Subsemigroup M
S
:
ΞΉ: Type ?u.24355
ΞΉ
β†’
Subsemigroup: (M : Type ?u.24605) β†’ [inst : Mul M] β†’ Type ?u.24605
Subsemigroup
M: Type ?u.24324
M
) : (β¨…
i: ?m.24622
i
, (
S: ΞΉ β†’ Subsemigroup M
S
i: ?m.24622
i
).
map: {M : Type ?u.24625} β†’ {N : Type ?u.24624} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.24711} β†’ {N : Type ?u.24710} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f =
iInf: {Ξ± : Type ?u.24727} β†’ [inst : InfSet Ξ±] β†’ {ΞΉ : Sort ?u.24726} β†’ (ΞΉ β†’ Ξ±) β†’ Ξ±
iInf
S: ΞΉ β†’ Subsemigroup M
S
:= (
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 ↑f
hf
).
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 i
u_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 S
Subsemigroup.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 β†’ βˆ€ (S : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.comap f (β¨… i, AddSubsemigroup.map f (S i)) = iInf S
AddSubsemigroup.comap_iInf_map_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 β†’ βˆ€ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S βŠ” AddSubsemigroup.map f T) = S βŠ” T
to_additive
] theorem
comap_sup_map_of_injective: βˆ€ (S T : Subsemigroup M), comap f (map f S βŠ” map f T) = S βŠ” T
comap_sup_map_of_injective
(S T :
Subsemigroup: (M : Type ?u.25255) β†’ [inst : Mul M] β†’ Type ?u.25255
Subsemigroup
M: Type ?u.24966
M
) : (S.
map: {M : Type ?u.25264} β†’ {N : Type ?u.25263} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f βŠ” T.
map: {M : Type ?u.25334} β†’ {N : Type ?u.25333} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.25421} β†’ {N : Type ?u.25420} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f = S βŠ” T := (
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 ↑f
hf
).
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 βŠ” b
u_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 βŠ” T
Subsemigroup.comap_sup_map_of_injective
#align add_subsemigroup.comap_sup_map_of_injective
AddSubsemigroup.comap_sup_map_of_injective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ βˆ€ (S T : AddSubsemigroup M), AddSubsemigroup.comap f (AddSubsemigroup.map f S βŠ” AddSubsemigroup.map f T) = S βŠ” T
AddSubsemigroup.comap_sup_map_of_injective
@[
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 β†’ βˆ€ (S : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.comap f (⨆ i, AddSubsemigroup.map f (S i)) = iSup S
to_additive
] 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 S
comap_iSup_map_of_injective
(
S: ΞΉ β†’ Subsemigroup M
S
:
ΞΉ: Type ?u.25697
ΞΉ
β†’
Subsemigroup: (M : Type ?u.25947) β†’ [inst : Mul M] β†’ Type ?u.25947
Subsemigroup
M: Type ?u.25666
M
) : (⨆
i: ?m.25964
i
, (
S: ΞΉ β†’ Subsemigroup M
S
i: ?m.25964
i
).
map: {M : Type ?u.25967} β†’ {N : Type ?u.25966} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f).
comap: {M : Type ?u.26062} β†’ {N : Type ?u.26061} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f =
iSup: {Ξ± : Type ?u.26078} β†’ [inst : SupSet Ξ±] β†’ {ΞΉ : Sort ?u.26077} β†’ (ΞΉ β†’ Ξ±) β†’ Ξ±
iSup
S: ΞΉ β†’ Subsemigroup M
S
:= (
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 ↑f
hf
).
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 i
u_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 S
Subsemigroup.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 β†’ βˆ€ (S : ΞΉ β†’ AddSubsemigroup M), AddSubsemigroup.comap f (⨆ i, AddSubsemigroup.map f (S i)) = iSup S
AddSubsemigroup.comap_iSup_map_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 β†’ βˆ€ {S T : AddSubsemigroup M}, AddSubsemigroup.map f S ≀ AddSubsemigroup.map f T ↔ S ≀ T
to_additive
] theorem
map_le_map_iff_of_injective: βˆ€ {S T : Subsemigroup M}, map f S ≀ map f T ↔ S ≀ T
map_le_map_iff_of_injective
{S T :
Subsemigroup: (M : Type ?u.26605) β†’ [inst : Mul M] β†’ Type ?u.26605
Subsemigroup
M: Type ?u.26316
M
} : S.
map: {M : Type ?u.26611} β†’ {N : Type ?u.26610} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ≀ T.
map: {M : Type ?u.26639} β†’ {N : Type ?u.26638} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f ↔ S ≀ T := (
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 ↑f
hf
).
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 ≀ b
l_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 ≀ T
Subsemigroup.map_le_map_iff_of_injective
#align add_subsemigroup.map_le_map_iff_of_injective
AddSubsemigroup.map_le_map_iff_of_injective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ βˆ€ {S T : AddSubsemigroup M}, AddSubsemigroup.map f S ≀ AddSubsemigroup.map f T ↔ S ≀ T
AddSubsemigroup.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}, Function.Injective ↑f β†’ StrictMono (AddSubsemigroup.map f)
to_additive
] 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 Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono
(
map: {M : Type ?u.27257} β†’ {N : Type ?u.27256} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f) := (
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 ↑f
hf
).
strictMono_l: βˆ€ {Ξ± : Type ?u.27443} {Ξ² : Type ?u.27442} {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²], GaloisCoinsertion l u β†’ StrictMono l
strictMono_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
#align add_subsemigroup.map_strict_mono_of_injective
AddSubsemigroup.map_strictMono_of_injective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Injective ↑f β†’ StrictMono (AddSubsemigroup.map f)
AddSubsemigroup.map_strictMono_of_injective
end GaloisCoinsertion section GaloisInsertion variable {
ΞΉ: Type ?u.29177
ΞΉ
:
Type _: Type (?u.30792+1)
Type _
} {f :
M: Type ?u.27865
M
β†’β‚™*
N: Type ?u.29149
N
} (hf :
Function.Surjective: {Ξ± : Sort ?u.27632} β†’ {Ξ² : Sort ?u.27631} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Surjective
f) /-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/ @[
to_additive: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ {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 N
map
f) (
comap: {M : Type ?u.28257} β†’ {N : Type ?u.28256} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f) := (
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).
toGaloisInsertion: {Ξ± : Type ?u.28387} β†’ {Ξ² : Type ?u.28386} β†’ [inst : Preorder Ξ±] β†’ [inst_1 : Preorder Ξ²] β†’ {l : Ξ± β†’ Ξ²} β†’ {u : Ξ² β†’ Ξ±} β†’ GaloisConnection l u β†’ (βˆ€ (b : Ξ²), b ≀ l (u b)) β†’ GaloisInsertion l u
toGaloisInsertion
fun
S: ?m.28422
S
x: ?m.28425
x
h: ?m.28428
h
=> let ⟨
y: M
y
,
hy: ↑f y = x
hy
⟩ := hf
x: ?m.28425
x
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 = y
mem_map
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
⟨
y: M
y
,

Goals accomplished! πŸ™
M: Type ?u.27865

N: Type ?u.27868

P: Type ?u.27871

Οƒ: Type ?u.27874

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

S✝: Subsemigroup M

ΞΉ: Type ?u.27896

f: M β†’β‚™* N

hf: Function.Surjective ↑f

S: Subsemigroup N

x: N

h: x ∈ S

y: M

hy: ↑f y = x


y ∈ comap f S ∧ ↑f y = x

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
#align add_subsemigroup.gi_map_comap
AddSubsemigroup.giMapComap: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Add M] β†’ [inst_1 : Add N] β†’ {f : AddHom M N} β†’ Function.Surjective ↑f β†’ GaloisInsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
AddSubsemigroup.giMapComap
@[
to_additive: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Surjective ↑f β†’ βˆ€ (S : AddSubsemigroup N), AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
to_additive
] theorem
map_comap_eq_of_surjective: βˆ€ (S : Subsemigroup N), map f (comap f S) = S
map_comap_eq_of_surjective
(S :
Subsemigroup: (M : Type ?u.29426) β†’ [inst : Mul M] β†’ Type ?u.29426
Subsemigroup
N: Type ?u.29149
N
) : (S.
comap: {M : Type ?u.29438} β†’ {N : Type ?u.29437} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup N β†’ Subsemigroup M
comap
f).
map: {M : Type ?u.29466} β†’ {N : Type ?u.29465} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f = S := (
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).
l_u_eq: βˆ€ {Ξ± : Type ?u.29532} {Ξ² : Type ?u.29531} {l : Ξ± β†’ Ξ²} {u : Ξ² β†’ Ξ±} [inst : Preorder Ξ±] [inst_1 : PartialOrder Ξ²], GaloisInsertion l u β†’ βˆ€ (b : Ξ²), l (u b) = b
l_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) = S
Subsemigroup.map_comap_eq_of_surjective
#align add_subsemigroup.map_comap_eq_of_surjective
AddSubsemigroup.map_comap_eq_of_surjective: βˆ€ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Surjective ↑f β†’ βˆ€ (S : AddSubsemigroup N), AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
AddSubsemigroup.map_comap_eq_of_surjective
@[
to_additive: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : AddHom M N}, Function.Surjective ↑f β†’ Function.Surjective (AddSubsemigroup.map f)
to_additive
] theorem
map_surjective_of_surjective: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M β†’β‚™* N}, Function.Surjective ↑f β†’ Function.Surjective (map f)
map_surjective_of_surjective
:
Function.Surjective: {Ξ± : Sort ?u.29962} β†’ {Ξ² : Sort ?u.29961} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Surjective
(
map: {M : Type ?u.29966} β†’ {N : Type ?u.29965} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ (M β†’β‚™* N) β†’ Subsemigroup M β†’ Subsemigroup N
map
f) := (
giMapComap: {M : Type ?u.30043} β†’ {N : Type ?u.30042} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ {f : M β†’β‚™* N} β†’ Function.Surjective ↑f β†’ GaloisInsertion (map f) (