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) 2018 Johannes Hölzl. 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

! This file was ported from Lean 3 source module group_theory.submonoid.operations
! leanprover-community/mathlib commit cf8e77c636317b059a8ce20807a29cf3772a0640
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Monoid.Cancel.Basic
import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.GroupTheory.Submonoid.Basic
import Mathlib.GroupTheory.Subsemigroup.Operations

/-!
# Operations on `Submonoid`s

In this file we define various operations on `Submonoid`s and `MonoidHom`s.

## Main definitions

### Conversion between multiplicative and additive definitions

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

### (Commutative) monoid structure on a submonoid

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

### Group actions by submonoids

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

### Operations on submonoids

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

### Monoid homomorphisms between submonoid

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

### Operations on `MonoidHom`s

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

## Tags

submonoid, range, product, map, comap
-/


variable {
M: Type ?u.86057
M
N: Type ?u.33229
N
P: Type ?u.48758
P
:
Type _: Type (?u.48755+1)
Type _
} [
MulOneClass: Type ?u.34652 → Type ?u.34652
MulOneClass
M: Type ?u.29
M
] [
MulOneClass: Type ?u.123590 → Type ?u.123590
MulOneClass
N: Type ?u.5
N
] [
MulOneClass: Type ?u.15878 → Type ?u.15878
MulOneClass
P: Type ?u.35
P
] (S :
Submonoid: (M : Type ?u.181499) → [inst : MulOneClass M] → Type ?u.181499
Submonoid
M: Type ?u.2
M
) /-! ### Conversion to/from `Additive`/`Multiplicative` -/ section /-- Submonoids of monoid `M` are isomorphic to additive submonoids of `Additive M`. -/ @[
simps: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑(↑toAddSubmonoid S) = ↑Additive.toMul ⁻¹' ↑S
simps
] def
Submonoid.toAddSubmonoid: {M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
:
Submonoid: (M : Type ?u.58) → [inst : MulOneClass M] → Type ?u.58
Submonoid
M: Type ?u.29
M
≃o
AddSubmonoid: (M : Type ?u.65) → [inst : AddZeroClass M] → Type ?u.65
AddSubmonoid
(
Additive: Type ?u.66 → Type ?u.66
Additive
M: Type ?u.29
M
) where toFun
S: ?m.183
S
:= { carrier :=
Additive.toMul: {α : Type ?u.281} → Additive α ≃ α
Additive.toMul
⁻¹'
S: ?m.183
S
zero_mem' :=
S: ?m.183
S
.
one_mem': ∀ {M : Type ?u.552} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
one_mem'
add_mem' := fun
ha: ?m.452
ha
hb: ?m.455
hb
=>
S: ?m.183
S
.
mul_mem': ∀ {M : Type ?u.462} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
mul_mem'
ha: ?m.452
ha
hb: ?m.455
hb
} invFun
S: ?m.560
S
:= { carrier :=
Additive.ofMul: {α : Type ?u.573} → α ≃ Additive α
Additive.ofMul
⁻¹'
S: ?m.560
S
one_mem' :=
S: ?m.560
S
.
zero_mem': ∀ {M : Type ?u.756} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
zero_mem'
mul_mem' := fun
ha: ?m.719
ha
hb: ?m.722
hb
=>
S: ?m.560
S
.
add_mem': ∀ {M : Type ?u.727} [inst : Add M] (self : AddSubsemigroup M) {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
add_mem'
ha: ?m.719
ha
hb: ?m.722
hb
} left_inv
x: ?m.764
x
:=

Goals accomplished! 🐙
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S, x: Submonoid M


(fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) x) = x
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toSubsemigroup✝: Subsemigroup M

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier


mk
(fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) = { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toSubsemigroup✝: Subsemigroup M

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier


mk
(fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) = { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S, x: Submonoid M


(fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) x) = x

Goals accomplished! 🐙
right_inv
x: ?m.770
x
:=

Goals accomplished! 🐙
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

x: AddSubmonoid (Additive M)


(fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) x) = x
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toAddSubsemigroup✝: AddSubsemigroup (Additive M)

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier


mk
(fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) = { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

toAddSubsemigroup✝: AddSubsemigroup (Additive M)

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier


mk
(fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) = { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
M: Type ?u.29

N: Type ?u.32

P: Type ?u.35

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S: Submonoid M

x: AddSubmonoid (Additive M)


(fun S => { toAddSubsemigroup := { carrier := ↑Additive.toMul ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : Additive M}, a ∈ ↑Additive.toMul ⁻¹' ↑S → b ∈ ↑Additive.toMul ⁻¹' ↑S → ↑Additive.toMul a * ↑Additive.toMul b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Additive.ofMul ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑Additive.ofMul ⁻¹' ↑S → b ∈ ↑Additive.ofMul ⁻¹' ↑S → a + b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) x) = x

Goals accomplished! 🐙
map_rel_iff' :=
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.to_add_submonoid
Submonoid.toAddSubmonoid: {M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
#align submonoid.to_add_submonoid_symm_apply_coe
Submonoid.toAddSubmonoid_symm_apply_coe: ∀ {M : Type u_1} [inst : MulOneClass M] (S : AddSubmonoid (Additive M)), ↑(↑(RelIso.symm Submonoid.toAddSubmonoid) S) = ↑Additive.ofMul ⁻¹' ↑S
Submonoid.toAddSubmonoid_symm_apply_coe
#align submonoid.to_add_submonoid_apply_coe
Submonoid.toAddSubmonoid_apply_coe: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑(↑Submonoid.toAddSubmonoid S) = ↑Additive.toMul ⁻¹' ↑S
Submonoid.toAddSubmonoid_apply_coe
/-- Additive submonoids of an additive monoid `Additive M` are isomorphic to submonoids of `M`. -/ abbrev
AddSubmonoid.toSubmonoid': {M : Type u_1} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'
:
AddSubmonoid: (M : Type ?u.1222) → [inst : AddZeroClass M] → Type ?u.1222
AddSubmonoid
(
Additive: Type ?u.1223 → Type ?u.1223
Additive
M: Type ?u.1193
M
) ≃o
Submonoid: (M : Type ?u.1238) → [inst : MulOneClass M] → Type ?u.1238
Submonoid
M: Type ?u.1193
M
:=
Submonoid.toAddSubmonoid: {M : Type ?u.1318} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
.
symm: {α : Type ?u.1334} → {β : Type ?u.1333} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
symm
#align add_submonoid.to_submonoid'
AddSubmonoid.toSubmonoid': {M : Type u_1} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'
theorem
Submonoid.toAddSubmonoid_closure: ∀ (S : Set M), ↑toAddSubmonoid (closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)
Submonoid.toAddSubmonoid_closure
(
S: Set M
S
:
Set: Type ?u.1532 → Type ?u.1532
Set
M: Type ?u.1505
M
) :
Submonoid.toAddSubmonoid: {M : Type ?u.1536} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
(
Submonoid.closure: {M : Type ?u.1611} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure
S: Set M
S
) =
AddSubmonoid.closure: {M : Type ?u.1639} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure
(
Additive.toMul: {α : Type ?u.1648} → Additive α ≃ α
Additive.toMul
⁻¹'
S: Set M
S
) :=
le_antisymm: ∀ {α : Type ?u.1747} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
(
Submonoid.toAddSubmonoid: {M : Type ?u.1780} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)
Submonoid.toAddSubmonoid
.
le_symm_apply: ∀ {α : Type ?u.1795} {β : Type ?u.1796} [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
<|
Submonoid.closure_le: ∀ {M : Type ?u.1967} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
(
AddSubmonoid.subset_closure: ∀ {M : Type ?u.1999} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
AddSubmonoid.subset_closure
(M :=
Additive: Type ?u.2000 → Type ?u.2000
Additive
M: Type ?u.1505
M
))) (
AddSubmonoid.closure_le: ∀ {M : Type ?u.2058} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
Submonoid.subset_closure: ∀ {M : Type ?u.2090} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(closure s)
Submonoid.subset_closure
(M :=
M: Type ?u.1505
M
)) #align submonoid.to_add_submonoid_closure
Submonoid.toAddSubmonoid_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set M), ↑Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)
Submonoid.toAddSubmonoid_closure
theorem
AddSubmonoid.toSubmonoid'_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)), ↑toSubmonoid' (closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)
AddSubmonoid.toSubmonoid'_closure
(
S: Set (Additive M)
S
:
Set: Type ?u.2156 → Type ?u.2156
Set
(
Additive: Type ?u.2157 → Type ?u.2157
Additive
M: Type ?u.2129
M
)) :
AddSubmonoid.toSubmonoid': {M : Type ?u.2161} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'
(
AddSubmonoid.closure: {M : Type ?u.2236} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure
S: Set (Additive M)
S
) =
Submonoid.closure: {M : Type ?u.2278} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure
(
Multiplicative.ofAdd: {α : Type ?u.2287} → α ≃ Multiplicative α
Multiplicative.ofAdd
⁻¹'
S: Set (Additive M)
S
) :=
le_antisymm: ∀ {α : Type ?u.2375} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
(
AddSubmonoid.toSubmonoid': {M : Type ?u.2408} → [inst : MulOneClass M] → AddSubmonoid (Additive M) ≃o Submonoid M
AddSubmonoid.toSubmonoid'
.
le_symm_apply: ∀ {α : Type ?u.2423} {β : Type ?u.2424} [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
<|
AddSubmonoid.closure_le: ∀ {M : Type ?u.2594} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
(
Submonoid.subset_closure: ∀ {M : Type ?u.2628} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s)
Submonoid.subset_closure
(M :=
M: Type ?u.2129
M
))) (
Submonoid.closure_le: ∀ {M : Type ?u.2680} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
AddSubmonoid.subset_closure: ∀ {M : Type ?u.2711} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(closure s)
AddSubmonoid.subset_closure
(M :=
Additive: Type ?u.2712 → Type ?u.2712
Additive
M: Type ?u.2129
M
)) #align add_submonoid.to_submonoid'_closure
AddSubmonoid.toSubmonoid'_closure: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)), ↑AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)
AddSubmonoid.toSubmonoid'_closure
end section variable {
A: Type ?u.2784
A
:
Type _: Type (?u.2784+1)
Type _
} [
AddZeroClass: Type ?u.4122 → Type ?u.4122
AddZeroClass
A: Type ?u.2784
A
] /-- Additive submonoids of an additive monoid `A` are isomorphic to multiplicative submonoids of `Multiplicative A`. -/ @[
simps: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)), ↑(↑(RelIso.symm toSubmonoid) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
simps
] def
AddSubmonoid.toSubmonoid: {A : Type u_1} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
:
AddSubmonoid: (M : Type ?u.2825) → [inst : AddZeroClass M] → Type ?u.2825
AddSubmonoid
A: Type ?u.2817
A
≃o
Submonoid: (M : Type ?u.2831) → [inst : MulOneClass M] → Type ?u.2831
Submonoid
(
Multiplicative: Type ?u.2832 → Type ?u.2832
Multiplicative
A: Type ?u.2817
A
) where toFun
S: ?m.2949
S
:= { carrier :=
Multiplicative.toAdd: {α : Type ?u.2989} → Multiplicative α ≃ α
Multiplicative.toAdd
⁻¹'
S: ?m.2949
S
one_mem' :=
S: ?m.2949
S
.
zero_mem': ∀ {M : Type ?u.3217} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
zero_mem'
mul_mem' := fun
ha: ?m.3160
ha
hb: ?m.3163
hb
=>
S: ?m.2949
S
.
add_mem': ∀ {M : Type ?u.3170} [inst : Add M] (self : AddSubsemigroup M) {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
add_mem'
ha: ?m.3160
ha
hb: ?m.3163
hb
} invFun
S: ?m.3225
S
:= { carrier :=
Multiplicative.ofAdd: {α : Type ?u.3238} → α ≃ Multiplicative α
Multiplicative.ofAdd
⁻¹'
S: ?m.3225
S
zero_mem' :=
S: ?m.3225
S
.
one_mem': ∀ {M : Type ?u.3421} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
one_mem'
add_mem' := fun
ha: ?m.3384
ha
hb: ?m.3387
hb
=>
S: ?m.3225
S
.
mul_mem': ∀ {M : Type ?u.3392} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
mul_mem'
ha: ?m.3384
ha
hb: ?m.3387
hb
} left_inv
x: ?m.3429
x
:=

Goals accomplished! 🐙
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: AddSubmonoid A


(fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) x) = x
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toAddSubsemigroup✝: AddSubsemigroup A

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier


mk
(fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) = { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toAddSubsemigroup✝: AddSubsemigroup A

zero_mem'✝: 0 ∈ toAddSubsemigroup✝.carrier


mk
(fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) = { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: AddSubmonoid A


(fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) ((fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) x) = x

Goals accomplished! 🐙
right_inv
x: ?m.3435
x
:=

Goals accomplished! 🐙
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: Submonoid (Multiplicative A)


(fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) x) = x
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toSubsemigroup✝: Subsemigroup (Multiplicative A)

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier


mk
(fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) = { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

toSubsemigroup✝: Subsemigroup (Multiplicative A)

one_mem'✝: 1 ∈ toSubsemigroup✝.carrier


mk
(fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) = { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
M: Type ?u.2790

N: Type ?u.2793

P: Type ?u.2796

inst✝³: MulOneClass M

inst✝²: MulOneClass N

inst✝¹: MulOneClass P

S: Submonoid M

A: Type ?u.2817

inst✝: AddZeroClass A

x: Submonoid (Multiplicative A)


(fun S => { toSubsemigroup := { carrier := ↑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : Multiplicative A}, a ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.toAdd ⁻¹' ↑S → ↑Multiplicative.toAdd a + ↑Multiplicative.toAdd b ∈ S.carrier) }, one_mem' := (_ : 0 ∈ S.carrier) }) ((fun S => { toAddSubsemigroup := { carrier := ↑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : A}, a ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → b ∈ ↑Multiplicative.ofAdd ⁻¹' ↑S → a * b ∈ S.carrier) }, zero_mem' := (_ : 1 ∈ S.carrier) }) x) = x

Goals accomplished! 🐙
map_rel_iff' :=
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align add_submonoid.to_submonoid
AddSubmonoid.toSubmonoid: {A : Type u_1} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
#align add_submonoid.to_submonoid_symm_apply_coe
AddSubmonoid.toSubmonoid_symm_apply_coe: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)), ↑(↑(RelIso.symm AddSubmonoid.toSubmonoid) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S
AddSubmonoid.toSubmonoid_symm_apply_coe
#align add_submonoid.to_submonoid_apply_coe
AddSubmonoid.toSubmonoid_apply_coe: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : AddSubmonoid A), ↑(↑AddSubmonoid.toSubmonoid S) = ↑Multiplicative.toAdd ⁻¹' ↑S
AddSubmonoid.toSubmonoid_apply_coe
/-- Submonoids of a monoid `Multiplicative A` are isomorphic to additive submonoids of `A`. -/ abbrev
Submonoid.toAddSubmonoid': Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'
:
Submonoid: (M : Type ?u.3839) → [inst : MulOneClass M] → Type ?u.3839
Submonoid
(
Multiplicative: Type ?u.3840 → Type ?u.3840
Multiplicative
A: Type ?u.3831
A
) ≃o
AddSubmonoid: (M : Type ?u.3855) → [inst : AddZeroClass M] → Type ?u.3855
AddSubmonoid
A: Type ?u.3831
A
:=
AddSubmonoid.toSubmonoid: {A : Type ?u.3934} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
.
symm: {α : Type ?u.3949} → {β : Type ?u.3948} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → β ≃o α
symm
#align submonoid.to_add_submonoid'
Submonoid.toAddSubmonoid': {A : Type u_1} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'
theorem
AddSubmonoid.toSubmonoid_closure: ∀ (S : Set A), ↑toSubmonoid (closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
AddSubmonoid.toSubmonoid_closure
(
S: Set A
S
:
Set: Type ?u.4125 → Type ?u.4125
Set
A: Type ?u.4119
A
) : (
AddSubmonoid.toSubmonoid: {A : Type ?u.4129} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
) (
AddSubmonoid.closure: {M : Type ?u.4213} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure
S: Set A
S
) =
Submonoid.closure: {M : Type ?u.4239} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure
(
Multiplicative.toAdd: {α : Type ?u.4248} → Multiplicative α ≃ α
Multiplicative.toAdd
⁻¹'
S: Set A
S
) :=
le_antisymm: ∀ {α : Type ?u.4347} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
(
AddSubmonoid.toSubmonoid: {A : Type ?u.4380} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
AddSubmonoid.toSubmonoid
.
to_galoisConnection: ∀ {α : Type ?u.4395} {β : Type ?u.4394} [inst : Preorder α] [inst_1 : Preorder β] (oi : α ≃o β), GaloisConnection ↑oi ↑(OrderIso.symm oi)
to_galoisConnection
.
l_le: ∀ {α : Type ?u.4480} {β : Type ?u.4479} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le
<|
AddSubmonoid.closure_le: ∀ {M : Type ?u.4586} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
Submonoid.subset_closure: ∀ {M : Type ?u.4619} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s)
Submonoid.subset_closure
(M :=
Multiplicative: Type ?u.4620 → Type ?u.4620
Multiplicative
A: Type ?u.4119
A
)) (
Submonoid.closure_le: ∀ {M : Type ?u.4678} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
AddSubmonoid.subset_closure: ∀ {M : Type ?u.4709} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(closure s)
AddSubmonoid.subset_closure
(M :=
A: Type ?u.4119
A
)) #align add_submonoid.to_submonoid_closure
AddSubmonoid.toSubmonoid_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set A), ↑AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
AddSubmonoid.toSubmonoid_closure
theorem
Submonoid.toAddSubmonoid'_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set (Multiplicative A)), ↑toAddSubmonoid' (closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)
Submonoid.toAddSubmonoid'_closure
(S :
Set: Type ?u.4780 → Type ?u.4780
Set
(
Multiplicative: Type ?u.4781 → Type ?u.4781
Multiplicative
A: Type ?u.4774
A
)) :
Submonoid.toAddSubmonoid': {A : Type ?u.4785} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'
(
Submonoid.closure: {M : Type ?u.4859} → [inst : MulOneClass M] → Set M → Submonoid M
Submonoid.closure
S) =
AddSubmonoid.closure: {M : Type ?u.4899} → [inst : AddZeroClass M] → Set M → AddSubmonoid M
AddSubmonoid.closure
(
Additive.ofMul: {α : Type ?u.4908} → α ≃ Additive α
Additive.ofMul
⁻¹' S) :=
le_antisymm: ∀ {α : Type ?u.4996} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
(
Submonoid.toAddSubmonoid': {A : Type ?u.5029} → [inst : AddZeroClass A] → Submonoid (Multiplicative A) ≃o AddSubmonoid A
Submonoid.toAddSubmonoid'
.
to_galoisConnection: ∀ {α : Type ?u.5044} {β : Type ?u.5043} [inst : Preorder α] [inst_1 : Preorder β] (oi : α ≃o β), GaloisConnection ↑oi ↑(OrderIso.symm oi)
to_galoisConnection
.
l_le: ∀ {α : Type ?u.5129} {β : Type ?u.5128} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le
<|
Submonoid.closure_le: ∀ {M : Type ?u.5234} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, closure s ≤ S ↔ s ⊆ ↑S
Submonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
AddSubmonoid.subset_closure: ∀ {M : Type ?u.5269} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
AddSubmonoid.subset_closure
(M :=
A: Type ?u.4774
A
)) (
AddSubmonoid.closure_le: ∀ {M : Type ?u.5320} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S
AddSubmonoid.closure_le
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
Submonoid.subset_closure: ∀ {M : Type ?u.5350} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(closure s)
Submonoid.subset_closure
(M :=
Multiplicative: Type ?u.5351 → Type ?u.5351
Multiplicative
A: Type ?u.4774
A
)) #align submonoid.to_add_submonoid'_closure
Submonoid.toAddSubmonoid'_closure: ∀ {A : Type u_1} [inst : AddZeroClass A] (S : Set (Multiplicative A)), ↑Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)
Submonoid.toAddSubmonoid'_closure
end namespace Submonoid variable {
F: Type ?u.5465
F
:
Type _: Type (?u.23621+1)
Type _
} [
mc: MonoidHomClass F M N
mc
:
MonoidHomClass: Type ?u.20871 → (M : outParam (Type ?u.20870)) → (N : outParam (Type ?u.20869)) → [inst : MulOneClass M] → [inst : MulOneClass N] → Type (max(max?u.20871?u.20870)?u.20869)
MonoidHomClass
F: Type ?u.22839
F
M: Type ?u.21960
M
N: Type ?u.5399
N
] open Set /-! ### `comap` and `map` -/ /-- The preimage of a submonoid along a monoid homomorphism is a submonoid. -/ @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N → AddSubmonoid M
to_additive
"The preimage of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."] def
comap: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
(
f: F
f
:
F: Type ?u.5465
F
) (S :
Submonoid: (M : Type ?u.5482) → [inst : MulOneClass M] → Type ?u.5482
Submonoid
N: Type ?u.5441
N
) :
Submonoid: (M : Type ?u.5491) → [inst : MulOneClass M] → Type ?u.5491
Submonoid
M: Type ?u.5438
M
where carrier :=
f: F
f
⁻¹' S one_mem' := show
f: F
f
1: ?m.6442
1
∈ S by
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N


↑f 1 ∈ S
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N


1 ∈ S
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N


1 ∈ S
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N


1 ∈ S
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N


↑f 1 ∈ S

Goals accomplished! 🐙
mul_mem'
ha: ?m.5861
ha
hb: ?m.5864
hb
:= show
f: F
f
(
_: ?m.6057
_
*
_: ?m.6060
_
) ∈ S by
M: Type ?u.5438

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

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

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


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

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

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

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


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

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

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

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


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

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

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

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


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

N: Type ?u.5441

P: Type ?u.5444

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.5465

mc: MonoidHomClass F M N

f: F

S: Submonoid N

a✝, b✝: M

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

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


↑f (a✝ * b✝) ∈ S

Goals accomplished! 🐙
#align submonoid.comap
Submonoid.comap: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
Submonoid.comap
#align add_submonoid.comap
AddSubmonoid.comap: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid N → AddSubmonoid M
AddSubmonoid.comap
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F), ↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S
to_additive
(attr := simp)] theorem
coe_comap: ∀ (S : Submonoid N) (f : F), ↑(comap f S) = ↑f ⁻¹' ↑S
coe_comap
(S :
Submonoid: (M : Type ?u.8191) → [inst : MulOneClass M] → Type ?u.8191
Submonoid
N: Type ?u.8152
N
) (
f: F
f
:
F: Type ?u.8176
F
) : (S.
comap: {M : Type ?u.8207} → {N : Type ?u.8206} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.8205} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:
Set: Type ?u.8204 → Type ?u.8204
Set
M: Type ?u.8149
M
) =
f: F
f
⁻¹' S :=
rfl: ∀ {α : Sort ?u.8679} {a : α}, a = a
rfl
#align submonoid.coe_comap
Submonoid.coe_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F), ↑(comap f S) = ↑f ⁻¹' ↑S
Submonoid.coe_comap
#align add_submonoid.coe_comap
AddSubmonoid.coe_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F), ↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S
AddSubmonoid.coe_comap
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M}, x ∈ AddSubmonoid.comap f S ↔ ↑f x ∈ S
to_additive
(attr := simp)] theorem
mem_comap: ∀ {S : Submonoid N} {f : F} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
mem_comap
{S :
Submonoid: (M : Type ?u.8832) → [inst : MulOneClass M] → Type ?u.8832
Submonoid
N: Type ?u.8793
N
} {
f: F
f
:
F: Type ?u.8817
F
} {
x: M
x
:
M: Type ?u.8790
M
} :
x: M
x
∈ S.
comap: {M : Type ?u.8852} → {N : Type ?u.8851} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.8850} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
↔
f: F
f
x: M
x
∈ S :=
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.mem_comap
Submonoid.mem_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M}, x ∈ comap f S ↔ ↑f x ∈ S
Submonoid.mem_comap
#align add_submonoid.mem_comap
AddSubmonoid.mem_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M}, x ∈ AddSubmonoid.comap f S ↔ ↑f x ∈ S
AddSubmonoid.mem_comap
@[
to_additive: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N), AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (AddMonoidHom.comp g f) S
to_additive
] theorem
comap_comap: ∀ (S : Submonoid P) (g : N →* P) (f : M →* N), comap f (comap g S) = comap (MonoidHom.comp g f) S
comap_comap
(S :
Submonoid: (M : Type ?u.9377) → [inst : MulOneClass M] → Type ?u.9377
Submonoid
P: Type ?u.9341
P
) (
g: N →* P
g
:
N: Type ?u.9338
N
→*
P: Type ?u.9341
P
) (
f: M →* N
f
:
M: Type ?u.9335
M
→*
N: Type ?u.9338
N
) : (S.
comap: {M : Type ?u.9411} → {N : Type ?u.9410} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.9409} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
g: N →* P
g
).
comap: {M : Type ?u.9484} → {N : Type ?u.9483} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.9482} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: M →* N
f
= S.
comap: {M : Type ?u.9556} → {N : Type ?u.9555} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.9554} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
(
g: N →* P
g
.
comp: {M : Type ?u.9573} → {N : Type ?u.9572} → {P : Type ?u.9571} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp
f: M →* N
f
) :=
rfl: ∀ {α : Sort ?u.9663} {a : α}, a = a
rfl
#align submonoid.comap_comap
Submonoid.comap_comap: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P] (S : Submonoid P) (g : N →* P) (f : M →* N), comap f (comap g S) = comap (MonoidHom.comp g f) S
Submonoid.comap_comap
#align add_submonoid.comap_comap
AddSubmonoid.comap_comap: ∀ {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N), AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (AddMonoidHom.comp g f) S
AddSubmonoid.comap_comap
@[
to_additive: ∀ {P : Type u_1} [inst : AddZeroClass P] (S : AddSubmonoid P), AddSubmonoid.comap (AddMonoidHom.id P) S = S
to_additive
(attr := simp)] theorem
comap_id: ∀ (S : Submonoid P), comap (MonoidHom.id P) S = S
comap_id
(S :
Submonoid: (M : Type ?u.9824) → [inst : MulOneClass M] → Type ?u.9824
Submonoid
P: Type ?u.9788
P
) : S.
comap: {M : Type ?u.9836} → {N : Type ?u.9835} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.9834} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
(
MonoidHom.id: (M : Type ?u.9851) → [inst : MulOneClass M] → M →* M
MonoidHom.id
P: Type ?u.9788
P
) = S :=
ext: ∀ {M : Type ?u.9911} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
ext
(

Goals accomplished! 🐙
M: Type ?u.9782

N: Type ?u.9785

P: Type u_1

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.9809

mc: MonoidHomClass F M N

S: Submonoid P


∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S

Goals accomplished! 🐙
) #align submonoid.comap_id
Submonoid.comap_id: ∀ {P : Type u_1} [inst : MulOneClass P] (S : Submonoid P), comap (MonoidHom.id P) S = S
Submonoid.comap_id
#align add_submonoid.comap_id
AddSubmonoid.comap_id: ∀ {P : Type u_1} [inst : AddZeroClass P] (S : AddSubmonoid P), AddSubmonoid.comap (AddMonoidHom.id P) S = S
AddSubmonoid.comap_id
/-- The image of a submonoid along a monoid homomorphism is a submonoid. -/ @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M → AddSubmonoid N
to_additive
"The image of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."] def
map: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
(
f: F
f
:
F: Type ?u.10959
F
) (S :
Submonoid: (M : Type ?u.10976) → [inst : MulOneClass M] → Type ?u.10976
Submonoid
M: Type ?u.10932
M
) :
Submonoid: (M : Type ?u.10985) → [inst : MulOneClass M] → Type ?u.10985
Submonoid
N: Type ?u.10935
N
where carrier :=
f: F
f
'' S one_mem' := ⟨
1: ?m.11366
1
, S.
one_mem: ∀ {M : Type ?u.11601} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ S
one_mem
,
map_one: ∀ {M : Type ?u.11610} {N : Type ?u.11611} {F : Type ?u.11609} [inst : One M] [inst_1 : One N] [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one
f: F
f
⟩ mul_mem' :=

Goals accomplished! 🐙
M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M


∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S
M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


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

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


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

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M


∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S
M: Type ?u.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid 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.10932

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


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

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


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

N: Type ?u.10935

P: Type ?u.10938

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.10959

mc: MonoidHomClass F M N

f: F

S: Submonoid M

x: M

hx: x ∈ ↑S

y: M

hy: y ∈ ↑S


↑f x * ↑f y = ↑f x * ↑f y

Goals accomplished! 🐙

Goals accomplished! 🐙
#align submonoid.map
Submonoid.map: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
Submonoid.map
#align add_submonoid.map
AddSubmonoid.map: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M → AddSubmonoid N
AddSubmonoid.map
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M), ↑(AddSubmonoid.map f S) = ↑f '' ↑S
to_additive
(attr := simp)] theorem
coe_map: ∀ (f : F) (S : Submonoid M), ↑(map f S) = ↑f '' ↑S
coe_map
(
f: F
f
:
F: Type ?u.13199
F
) (S :
Submonoid: (M : Type ?u.13216) → [inst : MulOneClass M] → Type ?u.13216
Submonoid
M: Type ?u.13172
M
) : (S.
map: {M : Type ?u.13230} → {N : Type ?u.13229} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.13228} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:
Set: Type ?u.13227 → Type ?u.13227
Set
N: Type ?u.13175
N
) =
f: F
f
'' S :=
rfl: ∀ {α : Sort ?u.13702} {a : α}, a = a
rfl
#align submonoid.coe_map
Submonoid.coe_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M), ↑(map f S) = ↑f '' ↑S
Submonoid.coe_map
#align add_submonoid.coe_map
AddSubmonoid.coe_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M), ↑(AddSubmonoid.map f S) = ↑f '' ↑S
AddSubmonoid.coe_map
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N}, y ∈ AddSubmonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
to_additive
(attr := simp)] theorem
mem_map: ∀ {f : F} {S : Submonoid M} {y : N}, y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
mem_map
{
f: F
f
:
F: Type ?u.13840
F
} {S :
Submonoid: (M : Type ?u.13857) → [inst : MulOneClass M] → Type ?u.13857
Submonoid
M: Type ?u.13813
M
} {
y: N
y
:
N: Type ?u.13816
N
} :
y: N
y
∈ S.
map: {M : Type ?u.13875} → {N : Type ?u.13874} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.13873} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
↔ ∃
x: ?m.14003
x
∈ S,
f: F
f
x: ?m.14003
x
=
y: N
y
:=

Goals accomplished! 🐙
M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N


y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N


y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N


y ∈ map f S ↔ ∃ x x_1, ↑f x = y
M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N


y ∈ map f S ↔ ∃ x x_1, ↑f x = y
M: Type u_1

N: Type u_2

P: Type ?u.13819

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type u_3

mc: MonoidHomClass F M N

f: F

S: Submonoid M

y: N


y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

Goals accomplished! 🐙
#align submonoid.mem_map
Submonoid.mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N}, y ∈ map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
Submonoid.mem_map
#align add_submonoid.mem_map
AddSubmonoid.mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N}, y ∈ AddSubmonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y
AddSubmonoid.mem_map
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M}, x ∈ S → ↑f x ∈ AddSubmonoid.map f S
to_additive
] theorem
mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
mem_map_of_mem
(
f: F
f
:
F: Type ?u.14498
F
) {S :
Submonoid: (M : Type ?u.14515) → [inst : MulOneClass M] → Type ?u.14515
Submonoid
M: Type ?u.14471
M
} {
x: M
x
:
M: Type ?u.14471
M
} (
hx: x ∈ S
hx
:
x: M
x
∈ S) :
f: F
f
x: M
x
∈ S.
map: {M : Type ?u.14771} → {N : Type ?u.14770} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.14769} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:=
mem_image_of_mem: ∀ {α : Type ?u.14896} {β : Type ?u.14897} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
mem_image_of_mem
f: F
f
hx: x ∈ S
hx
#align submonoid.mem_map_of_mem
Submonoid.mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
Submonoid.mem_map_of_mem
#align add_submonoid.mem_map_of_mem
AddSubmonoid.mem_map_of_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M}, x ∈ S → ↑f x ∈ AddSubmonoid.map f S
AddSubmonoid.mem_map_of_mem
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ AddSubmonoid.map f S
to_additive
] theorem
apply_coe_mem_map: ∀ (f : F) (S : Submonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ map f S
apply_coe_mem_map
(
f: F
f
:
F: Type ?u.15208
F
) (S :
Submonoid: (M : Type ?u.15225) → [inst : MulOneClass M] → Type ?u.15225
Submonoid
M: Type ?u.15181
M
) (
x: { x // x ∈ S }
x
: S) :
f: F
f
x: { x // x ∈ S }
x
∈ S.
map: {M : Type ?u.15578} → {N : Type ?u.15577} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.15576} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:=
mem_map_of_mem: ∀ {M : Type ?u.15703} {N : Type ?u.15704} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.15705} [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M}, x ∈ S → ↑f x ∈ map f S
mem_map_of_mem
f: F
f
x: { x // x ∈ S }
x
.
2: ∀ {α : Sort ?u.15789} {p : α → Prop} (self : Subtype p), p ↑self
2
#align submonoid.apply_coe_mem_map
Submonoid.apply_coe_mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ map f S
Submonoid.apply_coe_mem_map
#align add_submonoid.apply_coe_mem_map
AddSubmonoid.apply_coe_mem_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x ∈ S }), ↑f ↑x ∈ AddSubmonoid.map f S
AddSubmonoid.apply_coe_mem_map
@[
to_additive: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N), AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (AddMonoidHom.comp g f) S
to_additive
] theorem
map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P] (S : Submonoid M) (g : N →* P) (f : M →* N), map g (map f S) = map (MonoidHom.comp g f) S
map_map
(
g: N →* P
g
:
N: Type ?u.15866
N
→*
P: Type ?u.15869
P
) (
f: M →* N
f
:
M: Type ?u.15863
M
→*
N: Type ?u.15866
N
) : (S.
map: {M : Type ?u.15935} → {N : Type ?u.15934} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.15933} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: M →* N
f
).
map: {M : Type ?u.16008} → {N : Type ?u.16007} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.16006} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
g: N →* P
g
= S.
map: {M : Type ?u.16080} → {N : Type ?u.16079} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.16078} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
(
g: N →* P
g
.
comp: {M : Type ?u.16097} → {N : Type ?u.16096} → {P : Type ?u.16095} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp
f: M →* N
f
) :=
SetLike.coe_injective: ∀ {A : Type ?u.16186} {B : Type ?u.16187} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective
<|
image_image: ∀ {α : Type ?u.16206} {β : Type ?u.16208} {γ : Type ?u.16207} (g : β → γ) (f : α → β) (s : Set α), g '' (f '' s) = (fun x => g (f x)) '' s
image_image
_: ?m.16210 → ?m.16211
_
_: ?m.16209 → ?m.16210
_
_: Set ?m.16209
_
#align submonoid.map_map
Submonoid.map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P] (S : Submonoid M) (g : N →* P) (f : M →* N), map g (map f S) = map (MonoidHom.comp g f) S
Submonoid.map_map
#align add_submonoid.map_map
AddSubmonoid.map_map: ∀ {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N), AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (AddMonoidHom.comp g f) S
AddSubmonoid.map_map
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ {S : AddSubmonoid M} {x : M}, ↑f x ∈ AddSubmonoid.map f S ↔ x ∈ S
to_additive
] theorem
mem_map_iff_mem: ∀ {f : F}, Function.Injective ↑f → ∀ {S : Submonoid M} {x : M}, ↑f x ∈ map f S ↔ x ∈ S
mem_map_iff_mem
{
f: F
f
:
F: Type ?u.16377
F
} (
hf: Function.Injective ↑f
hf
:
Function.Injective: {α : Sort ?u.16395} → {β : Sort ?u.16394} → (α → β) → Prop
Function.Injective
f: F
f
) {S :
Submonoid: (M : Type ?u.16587) → [inst : MulOneClass M] → Type ?u.16587
Submonoid
M: Type ?u.16350
M
} {
x: M
x
:
M: Type ?u.16350
M
} :
f: F
f
x: M
x
∈ S.
map: {M : Type ?u.16774} → {N : Type ?u.16773} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.16772} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
↔
x: M
x
∈ S :=
hf: Function.Injective ↑f
hf
.
mem_set_image: ∀ {α : Type ?u.16922} {β : Type ?u.16923} {f : α → β}, Function.Injective f → ∀ {s : Set α} {a : α}, f a ∈ f '' s ↔ a ∈ s
mem_set_image
#align submonoid.mem_map_iff_mem
Submonoid.mem_map_iff_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ {S : Submonoid M} {x : M}, ↑f x ∈ map f S ↔ x ∈ S
Submonoid.mem_map_iff_mem
#align add_submonoid.mem_map_iff_mem
AddSubmonoid.mem_map_iff_mem: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ {S : AddSubmonoid M} {x : M}, ↑f x ∈ AddSubmonoid.map f S ↔ x ∈ S
AddSubmonoid.mem_map_iff_mem
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N}, AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
to_additive
] theorem
map_le_iff_le_comap: ∀ {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
map_le_iff_le_comap
{
f: F
f
:
F: Type ?u.17062
F
} {S :
Submonoid: (M : Type ?u.17079) → [inst : MulOneClass M] → Type ?u.17079
Submonoid
M: Type ?u.17035
M
} {T :
Submonoid: (M : Type ?u.17088) → [inst : MulOneClass M] → Type ?u.17088
Submonoid
N: Type ?u.17038
N
} : S.
map: {M : Type ?u.17100} → {N : Type ?u.17099} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.17098} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
≤ T ↔ S ≤ T.
comap: {M : Type ?u.17204} → {N : Type ?u.17203} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.17202} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:=
image_subset_iff: ∀ {α : Type ?u.17300} {β : Type ?u.17301} {s : Set α} {t : Set β} {f : α → β}, f '' s ⊆ t ↔ s ⊆ f ⁻¹' t
image_subset_iff
#align submonoid.map_le_iff_le_comap
Submonoid.map_le_iff_le_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
Submonoid.map_le_iff_le_comap
#align add_submonoid.map_le_iff_le_comap
AddSubmonoid.map_le_iff_le_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N}, AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
AddSubmonoid.map_le_iff_le_comap
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
to_additive
] theorem
gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
(
f: F
f
:
F: Type ?u.17445
F
) :
GaloisConnection: {α : Type ?u.17463} → {β : Type ?u.17462} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection
(
map: {M : Type ?u.17500} → {N : Type ?u.17499} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.17498} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.17619} → {N : Type ?u.17618} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.17617} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
) := fun
_: ?m.17768
_
_: ?m.17771
_
=>
map_le_iff_le_comap: ∀ {M : Type ?u.17773} {N : Type ?u.17774} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.17775} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N}, map f S ≤ T ↔ S ≤ comap f T
map_le_iff_le_comap
#align submonoid.gc_map_comap
Submonoid.gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
Submonoid.gc_map_comap
#align add_submonoid.gc_map_comap
AddSubmonoid.gc_map_comap: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
AddSubmonoid.gc_map_comap
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
to_additive
] theorem
map_le_of_le_comap: ∀ {T : Submonoid N} {f : F}, S ≤ comap f T → map f S ≤ T
map_le_of_le_comap
{T :
Submonoid: (M : Type ?u.17971) → [inst : MulOneClass M] → Type ?u.17971
Submonoid
N: Type ?u.17932
N
} {
f: F
f
:
F: Type ?u.17956
F
} : S ≤ T.
comap: {M : Type ?u.17986} → {N : Type ?u.17985} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.17984} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
→ S.
map: {M : Type ?u.18096} → {N : Type ?u.18095} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.18094} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
≤ T := (
gc_map_comap: ∀ {M : Type ?u.18194} {N : Type ?u.18195} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.18196} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
l_le: ∀ {α : Type ?u.18258} {β : Type ?u.18257} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
l_le
#align submonoid.map_le_of_le_comap
Submonoid.map_le_of_le_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F}, S ≤ comap f T → map f S ≤ T
Submonoid.map_le_of_le_comap
#align add_submonoid.map_le_of_le_comap
AddSubmonoid.map_le_of_le_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
AddSubmonoid.map_le_of_le_comap
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
to_additive
] theorem
le_comap_of_map_le: ∀ {T : Submonoid N} {f : F}, map f S ≤ T → S ≤ comap f T
le_comap_of_map_le
{T :
Submonoid: (M : Type ?u.18482) → [inst : MulOneClass M] → Type ?u.18482
Submonoid
N: Type ?u.18443
N
} {
f: F
f
:
F: Type ?u.18467
F
} : S.
map: {M : Type ?u.18497} → {N : Type ?u.18496} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.18495} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
≤ T → S ≤ T.
comap: {M : Type ?u.18607} → {N : Type ?u.18606} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.18605} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.18705} {N : Type ?u.18706} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.18707} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
le_u: ∀ {α : Type ?u.18769} {β : Type ?u.18768} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {a : α} {b : β}, l a ≤ b → a ≤ u b
le_u
#align submonoid.le_comap_of_map_le
Submonoid.le_comap_of_map_le: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F}, map f S ≤ T → S ≤ comap f T
Submonoid.le_comap_of_map_le
#align add_submonoid.le_comap_of_map_le
AddSubmonoid.le_comap_of_map_le: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F}, AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
AddSubmonoid.le_comap_of_map_le
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)
to_additive
] theorem
le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, S ≤ comap f (map f S)
le_comap_map
{
f: F
f
:
F: Type ?u.18978
F
} : S ≤ (S.
map: {M : Type ?u.18998} → {N : Type ?u.18997} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.18996} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
).
comap: {M : Type ?u.19061} → {N : Type ?u.19060} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.19059} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.19162} {N : Type ?u.19163} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.19164} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
le_u_l: ∀ {α : Type ?u.19226} {β : Type ?u.19225} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ (a : α), a ≤ u (l a)
le_u_l
_: ?m.19235
_
#align submonoid.le_comap_map
Submonoid.le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, S ≤ comap f (map f S)
Submonoid.le_comap_map
#align add_submonoid.le_comap_map
AddSubmonoid.le_comap_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)
AddSubmonoid.le_comap_map
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S
to_additive
] theorem
map_comap_le: ∀ {S : Submonoid N} {f : F}, map f (comap f S) ≤ S
map_comap_le
{S :
Submonoid: (M : Type ?u.19433) → [inst : MulOneClass M] → Type ?u.19433
Submonoid
N: Type ?u.19394
N
} {
f: F
f
:
F: Type ?u.19418
F
} : (S.
comap: {M : Type ?u.19447} → {N : Type ?u.19446} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.19445} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
).
map: {M : Type ?u.19505} → {N : Type ?u.19504} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.19503} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
≤ S := (
gc_map_comap: ∀ {M : Type ?u.19608} {N : Type ?u.19609} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.19610} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
l_u_le: ∀ {α : Type ?u.19672} {β : Type ?u.19671} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ (a : β), l (u a) ≤ a
l_u_le
_: ?m.19682
_
#align submonoid.map_comap_le
Submonoid.map_comap_le: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, map f (comap f S) ≤ S
Submonoid.map_comap_le
#align add_submonoid.map_comap_le
AddSubmonoid.map_comap_le: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S
AddSubmonoid.map_comap_le
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.map f)
to_additive
] theorem
monotone_map: ∀ {f : F}, Monotone (map f)
monotone_map
{
f: F
f
:
F: Type ?u.19870
F
} :
Monotone: {α : Type ?u.19888} → {β : Type ?u.19887} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
(
map: {M : Type ?u.19925} → {N : Type ?u.19924} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.19923} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) := (
gc_map_comap: ∀ {M : Type ?u.20119} {N : Type ?u.20120} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.20121} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
monotone_l: ∀ {α : Type ?u.20183} {β : Type ?u.20182} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → Monotone l
monotone_l
#align submonoid.monotone_map
Submonoid.monotone_map: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, Monotone (map f)
Submonoid.monotone_map
#align add_submonoid.monotone_map
AddSubmonoid.monotone_map: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.map f)
AddSubmonoid.monotone_map
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.comap f)
to_additive
] theorem
monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, Monotone (comap f)
monotone_comap
{
f: F
f
:
F: Type ?u.20368
F
} :
Monotone: {α : Type ?u.20386} → {β : Type ?u.20385} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
(
comap: {M : Type ?u.20423} → {N : Type ?u.20422} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.20421} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
) := (
gc_map_comap: ∀ {M : Type ?u.20617} {N : Type ?u.20618} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.20619} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
monotone_u: ∀ {α : Type ?u.20681} {β : Type ?u.20680} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → Monotone u
monotone_u
#align submonoid.monotone_comap
Submonoid.monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, Monotone (comap f)
Submonoid.monotone_comap
#align add_submonoid.monotone_comap
AddSubmonoid.monotone_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.comap f)
AddSubmonoid.monotone_comap
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
to_additive
(attr := simp)] theorem
map_comap_map: ∀ {f : F}, map f (comap f (map f S)) = map f S
map_comap_map
{
f: F
f
:
F: Type ?u.20866
F
} : ((S.
map: {M : Type ?u.20886} → {N : Type ?u.20885} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.20884} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
).
comap: {M : Type ?u.20949} → {N : Type ?u.20948} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.20947} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
).
map: {M : Type ?u.21005} → {N : Type ?u.21004} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21003} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
= S.
map: {M : Type ?u.21055} → {N : Type ?u.21054} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21053} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.21106} {N : Type ?u.21107} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.21108} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
l_u_l_eq_l: ∀ {α : Type ?u.21170} {β : Type ?u.21169} [inst : Preorder α] [inst_1 : PartialOrder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ (a : α), l (u (l a)) = l a
l_u_l_eq_l
_: ?m.21179
_
#align submonoid.map_comap_map
Submonoid.map_comap_map: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, map f (comap f (map f S)) = map f S
Submonoid.map_comap_map
#align add_submonoid.map_comap_map
AddSubmonoid.map_comap_map: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
AddSubmonoid.map_comap_map
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S
to_additive
(attr := simp)] theorem
comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, comap f (map f (comap f S)) = comap f S
comap_map_comap
{S :
Submonoid: (M : Type ?u.21440) → [inst : MulOneClass M] → Type ?u.21440
Submonoid
N: Type ?u.21401
N
} {
f: F
f
:
F: Type ?u.21425
F
} : ((S.
comap: {M : Type ?u.21454} → {N : Type ?u.21453} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21452} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
).
map: {M : Type ?u.21512} → {N : Type ?u.21511} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21510} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
).
comap: {M : Type ?u.21568} → {N : Type ?u.21567} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21566} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
= S.
comap: {M : Type ?u.21618} → {N : Type ?u.21617} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.21616} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.21670} {N : Type ?u.21671} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.21672} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
u_l_u_eq_u: ∀ {α : Type ?u.21734} {β : Type ?u.21733} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ (b : β), u (l (u b)) = u b
u_l_u_eq_u
_: ?m.21744
_
#align submonoid.comap_map_comap
Submonoid.comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F}, comap f (map f (comap f S)) = comap f S
Submonoid.comap_map_comap
#align add_submonoid.comap_map_comap
AddSubmonoid.comap_map_comap: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F}, AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S
AddSubmonoid.comap_map_comap
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F), AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
to_additive
] theorem
map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F), map f (S ⊔ T) = map f S ⊔ map f T
map_sup
(S T :
Submonoid: (M : Type ?u.22011) → [inst : MulOneClass M] → Type ?u.22011
Submonoid
M: Type ?u.21960
M
) (
f: F
f
:
F: Type ?u.21987
F
) : (S ⊔ T).
map: {M : Type ?u.22056} → {N : Type ?u.22055} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22054} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
= S.
map: {M : Type ?u.22119} → {N : Type ?u.22118} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22117} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
⊔ T.
map: {M : Type ?u.22213} → {N : Type ?u.22212} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22211} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.22626} {N : Type ?u.22627} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.22628} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
:
GaloisConnection: {α : Type ?u.22325} → {β : Type ?u.22324} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection
(
map: {M : Type ?u.22362} → {N : Type ?u.22361} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22360} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.22481} → {N : Type ?u.22480} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22479} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
)).
l_sup: ∀ {α : Type ?u.22691} {β : Type ?u.22690} {a₁ a₂ : α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {l : α → β} {u : β → α}, GaloisConnection l u → l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
l_sup
#align submonoid.map_sup
Submonoid.map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F), map f (S ⊔ T) = map f S ⊔ map f T
Submonoid.map_sup
#align add_submonoid.map_sup
AddSubmonoid.map_sup: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F), AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
AddSubmonoid.map_sup
@[
to_additive: ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid M), AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
to_additive
] theorem
map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid M), map f (iSup s) = ⨆ i, map f (s i)
map_iSup
{
ι: Sort u_1
ι
:
Sort _: Type ?u.22854
Sort
Sort _: Type ?u.22854
_
} (
f: F
f
:
F: Type ?u.22839
F
) (
s: ι → Submonoid M
s
:
ι: Sort ?u.22854
ι
→
Submonoid: (M : Type ?u.22861) → [inst : MulOneClass M] → Type ?u.22861
Submonoid
M: Type ?u.22812
M
) : (
iSup: {α : Type ?u.22872} → [inst : SupSet α] → {ι : Sort ?u.22871} → (ι → α) → α
iSup
s: ι → Submonoid M
s
).
map: {M : Type ?u.22904} → {N : Type ?u.22903} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22902} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
= ⨆
i: ?m.22968
i
, (
s: ι → Submonoid M
s
i: ?m.22968
i
).
map: {M : Type ?u.22972} → {N : Type ?u.22971} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.22970} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.23397} {N : Type ?u.23398} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.23399} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
:
GaloisConnection: {α : Type ?u.23096} → {β : Type ?u.23095} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection
(
map: {M : Type ?u.23133} → {N : Type ?u.23132} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23131} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.23252} → {N : Type ?u.23251} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23250} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
)).
l_iSup: ∀ {α : Type ?u.23463} {β : Type ?u.23462} {ι : Sort ?u.23461} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {f : ι → α}, l (iSup f) = ⨆ i, l (f i)
l_iSup
#align submonoid.map_supr
Submonoid.map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid M), map f (iSup s) = ⨆ i, map f (s i)
Submonoid.map_iSup
#align add_submonoid.map_supr
AddSubmonoid.map_iSup: ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid M), AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
AddSubmonoid.map_iSup
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid N) (f : F), AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T
to_additive
] theorem
comap_inf: ∀ (S T : Submonoid N) (f : F), comap f (S ⊓ T) = comap f S ⊓ comap f T
comap_inf
(S T :
Submonoid: (M : Type ?u.23645) → [inst : MulOneClass M] → Type ?u.23645
Submonoid
N: Type ?u.23597
N
) (
f: F
f
:
F: Type ?u.23621
F
) : (S ⊓ T).
comap: {M : Type ?u.23670} → {N : Type ?u.23669} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23668} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
= S.
comap: {M : Type ?u.23733} → {N : Type ?u.23732} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23731} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
⊓ T.
comap: {M : Type ?u.23827} → {N : Type ?u.23826} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23825} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.24220} {N : Type ?u.24221} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.24222} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
:
GaloisConnection: {α : Type ?u.23919} → {β : Type ?u.23918} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection
(
map: {M : Type ?u.23956} → {N : Type ?u.23955} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.23954} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.24075} → {N : Type ?u.24074} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.24073} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
)).
u_inf: ∀ {α : Type ?u.24285} {β : Type ?u.24284} {b₁ b₂ : β} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {l : α → β} {u : β → α}, GaloisConnection l u → u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
u_inf
#align submonoid.comap_inf
Submonoid.comap_inf: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S T : Submonoid N) (f : F), comap f (S ⊓ T) = comap f S ⊓ comap f T
Submonoid.comap_inf
#align add_submonoid.comap_inf
AddSubmonoid.comap_inf: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid N) (f : F), AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T
AddSubmonoid.comap_inf
@[
to_additive: ∀ {M : Type u_3} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid N), AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
to_additive
] theorem
comap_iInf: ∀ {ι : Sort u_1} (f : F) (s : ι → Submonoid N), comap f (iInf s) = ⨅ i, comap f (s i)
comap_iInf
{
ι: Sort u_1
ι
:
Sort _: Type ?u.24454
Sort
Sort _: Type ?u.24454
_
} (
f: F
f
:
F: Type ?u.24439
F
) (
s: ι → Submonoid N
s
:
ι: Sort ?u.24454
ι
→
Submonoid: (M : Type ?u.24461) → [inst : MulOneClass M] → Type ?u.24461
Submonoid
N: Type ?u.24415
N
) : (
iInf: {α : Type ?u.24472} → [inst : InfSet α] → {ι : Sort ?u.24471} → (ι → α) → α
iInf
s: ι → Submonoid N
s
).
comap: {M : Type ?u.24495} → {N : Type ?u.24494} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.24493} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
= ⨅
i: ?m.24559
i
, (
s: ι → Submonoid N
s
i: ?m.24559
i
).
comap: {M : Type ?u.24563} → {N : Type ?u.24562} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.24561} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
:= (
gc_map_comap: ∀ {M : Type ?u.24979} {N : Type ?u.24980} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.24981} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
:
GaloisConnection: {α : Type ?u.24678} → {β : Type ?u.24677} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Prop
GaloisConnection
(
map: {M : Type ?u.24715} → {N : Type ?u.24714} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.24713} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.24834} → {N : Type ?u.24833} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.24832} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
)).
u_iInf: ∀ {α : Type ?u.25045} {β : Type ?u.25044} {ι : Sort ?u.25043} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {f : ι → β}, u (iInf f) = ⨅ i, u (f i)
u_iInf
#align submonoid.comap_infi
Submonoid.comap_iInf: ∀ {M : Type u_3} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid N), comap f (iInf s) = ⨅ i, comap f (s i)
Submonoid.comap_iInf
#align add_submonoid.comap_infi
AddSubmonoid.comap_iInf: ∀ {M : Type u_3} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid N), AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
AddSubmonoid.comap_iInf
@[
to_additive: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.map f ⊥ = ⊥
to_additive
(attr := simp)] theorem
map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F), map f ⊥ = ⊥
map_bot
(
f: F
f
:
F: Type ?u.25213
F
) : (
⊥: ?m.25240
⊥
:
Submonoid: (M : Type ?u.25232) → [inst : MulOneClass M] → Type ?u.25232
Submonoid
M: Type ?u.25186
M
).
map: {M : Type ?u.25281} → {N : Type ?u.25280} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.25279} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
=
⊥: ?m.25340
⊥
:= (
gc_map_comap: ∀ {M : Type ?u.25399} {N : Type ?u.25400} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.25401} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
l_bot: ∀ {α : Type ?u.25463} {β : Type ?u.25462} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot β] [inst_3 : OrderBot α] {l : α → β} {u : β → α}, GaloisConnection l u → l ⊥ = ⊥
l_bot
#align submonoid.map_bot
Submonoid.map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F), map f ⊥ = ⊥
Submonoid.map_bot
#align add_submonoid.map_bot
AddSubmonoid.map_bot: ∀ {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.map f ⊥ = ⊥
AddSubmonoid.map_bot
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊤ = ⊤
to_additive
(attr := simp)] theorem
comap_top: ∀ (f : F), comap f ⊤ = ⊤
comap_top
(
f: F
f
:
F: Type ?u.25773
F
) : (
⊤: ?m.25800
⊤
:
Submonoid: (M : Type ?u.25792) → [inst : MulOneClass M] → Type ?u.25792
Submonoid
N: Type ?u.25749
N
).
comap: {M : Type ?u.25840} → {N : Type ?u.25839} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.25838} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
=
⊤: ?m.25899
⊤
:= (
gc_map_comap: ∀ {M : Type ?u.25956} {N : Type ?u.25957} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.25958} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
u_top: ∀ {α : Type ?u.26020} {β : Type ?u.26019} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α] [inst_3 : OrderTop β] {l : α → β} {u : β → α}, GaloisConnection l u → u ⊤ = ⊤
u_top
#align submonoid.comap_top
Submonoid.comap_top: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F), comap f ⊤ = ⊤
Submonoid.comap_top
#align add_submonoid.comap_top
AddSubmonoid.comap_top: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.comap f ⊤ = ⊤
AddSubmonoid.comap_top
@[
to_additive: ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.map (AddMonoidHom.id M) S = S
to_additive
(attr := simp)] theorem
map_id: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), map (MonoidHom.id M) S = S
map_id
(S :
Submonoid: (M : Type ?u.26345) → [inst : MulOneClass M] → Type ?u.26345
Submonoid
M: Type ?u.26303
M
) : S.
map: {M : Type ?u.26357} → {N : Type ?u.26356} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.26355} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
(
MonoidHom.id: (M : Type ?u.26372) → [inst : MulOneClass M] → M →* M
MonoidHom.id
M: Type ?u.26303
M
) = S :=
ext: ∀ {M : Type ?u.26432} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
ext
fun
_: ?m.26456
_
=> ⟨fun ⟨
_: ?m.26456
_
,
h: x✝¹ ∈ ↑S
h
,
rfl: ∀ {α : Sort ?u.26470} {a : α}, a = a
rfl
⟩ =>
h: x✝¹ ∈ ↑S
h
, fun
h: ?m.26771
h
=> ⟨
_: ?m.26778
_
,
h: ?m.26771
h
,
rfl: ∀ {α : Sort ?u.26803} {a : α}, a = a
rfl
⟩⟩ #align submonoid.map_id
Submonoid.map_id: ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), map (MonoidHom.id M) S = S
Submonoid.map_id
#align add_submonoid.map_id
AddSubmonoid.map_id: ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.map (AddMonoidHom.id M) S = S
AddSubmonoid.map_id
section GaloisCoinsertion variable {
ι: Type ?u.29867
ι
:
Type _: Type (?u.27001+1)
Type _
} {
f: F
f
:
F: Type ?u.30432
F
} (
hf: Function.Injective ↑f
hf
:
Function.Injective: {α : Sort ?u.31031} → {β : Sort ?u.31030} → (α → β) → Prop
Function.Injective
f: F
f
) /-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/ @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
to_additive
" `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. "] def
gciMapComap: GaloisCoinsertion (map f) (comap f)
gciMapComap
:
GaloisCoinsertion: {α : Type ?u.27436} → {β : Type ?u.27435} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → (β → α) → Type (max?u.27436?u.27435)
GaloisCoinsertion
(
map: {M : Type ?u.27473} → {N : Type ?u.27472} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.27471} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
) (
comap: {M : Type ?u.27592} → {N : Type ?u.27591} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.27590} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
) := (
gc_map_comap: ∀ {M : Type ?u.27738} {N : Type ?u.27739} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type ?u.27740} [mc : MonoidHomClass F M N] (f : F), GaloisConnection (map f) (comap f)
gc_map_comap
f: F
f
).
toGaloisCoinsertion: {α : Type ?u.27795} → {β : Type ?u.27794} → [inst : Preorder α] → [inst_1 : Preorder β] → {l : α → β} → {u : β → α} → GaloisConnection l u → (∀ (a : α), u (l a) ≤ a) → GaloisCoinsertion l u
toGaloisCoinsertion
fun
S: ?m.27830
S
x: ?m.27833
x
=>

Goals accomplished! 🐙
M: Type ?u.27197

N: Type ?u.27200

P: Type ?u.27203

inst✝²: MulOneClass M

inst✝¹: MulOneClass N

inst✝: MulOneClass P

S✝: Submonoid M

F: Type ?u.27224

mc: MonoidHomClass F M N

ι: Type ?u.27239

f: F

hf: Function.Injective ↑f

S: Submonoid M

x: M


x ∈ comap f (map f S) → x ∈ S

Goals accomplished! 🐙
#align submonoid.gci_map_comap
Submonoid.gciMapComap: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type u_3} → [mc : MonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (map f) (comap f)
Submonoid.gciMapComap
#align add_submonoid.gci_map_comap
AddSubmonoid.gciMapComap: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → {F : Type u_3} → [mc : AddMonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
AddSubmonoid.gciMapComap
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ (S : AddSubmonoid M), AddSubmonoid.comap f (AddSubmonoid.map f S) = S
to_additive
] theorem
comap_map_eq_of_injective: ∀ (S : Submonoid M), comap f (map f S) = S
comap_map_eq_of_injective
(S :
Submonoid: (M : Type ?u.29462) → [inst : MulOneClass M] → Type ?u.29462
Submonoid
M: Type ?u.29224
M
) : (S.
map: {M : Type ?u.29474} → {N : Type ?u.29473} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.29472} → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
map
f: F
f
).
comap: {M : Type ?u.29532} → {N : Type ?u.29531} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.29530} → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
comap
f: F
f
= S := (
gciMapComap: {M : Type ?u.29591} → {N : Type ?u.29590} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → {F : Type ?u.29589} → [mc : MonoidHomClass F M N] → {f : F} → Function.Injective ↑f → GaloisCoinsertion (map f) (comap f)
gciMapComap
hf: Function.Injective ↑f
hf
).
u_l_eq: ∀ {α : Type ?u.29657} {β : Type ?u.29656} {l : α → β} {u : β → α} [inst : PartialOrder α] [inst_1 : Preorder β], GaloisCoinsertion l u → ∀ (a : α), u (l a) = a
u_l_eq
_: ?m.29666
_
#align submonoid.comap_map_eq_of_injective
Submonoid.comap_map_eq_of_injective: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ (S : Submonoid M), comap f (map f S) = S
Submonoid.comap_map_eq_of_injective
#align add_submonoid.comap_map_eq_of_injective
AddSubmonoid.comap_map_eq_of_injective: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F}, Function.Injective ↑f → ∀ (S : AddSubmonoid M), AddSubmonoid.comap f (