group_theory.congruence - mathlib3 docs

source

structure add_con (M : Type u_1) [has_add M] :

Type u_1

to_setoid : setoid M
add' : ∀ {w x y z : M}, setoid.r w x → setoid.r y z → setoid.r (w + y) (x + z)

A congruence relation on a type with an addition is an equivalence relation which preserves addition.

Instances for add_con

source

structure con (M : Type u_1) [has_mul M] :

Type u_1

to_setoid : setoid M
mul' : ∀ {w x y z : M}, setoid.r w x → setoid.r y z → setoid.r (w * y) (x * z)

A congruence relation on a type with a multiplication is an equivalence relation which preserves multiplication.

Instances for con

source

inductive add_con_gen.rel {M : Type u_1} [has_add M] (r : M → M → Prop) :

M → M → Prop

of : ∀ {M : Type u_1} [_inst_1 : has_add M] {r : M → M → Prop} (x y : M), r x y → add_con_gen.rel r x y
refl : ∀ {M : Type u_1} [_inst_1 : has_add M] {r : M → M → Prop} (x : M), add_con_gen.rel r x x
symm : ∀ {M : Type u_1} [_inst_1 : has_add M] {r : M → M → Prop} (x y : M), add_con_gen.rel r x y → add_con_gen.rel r y x
trans : ∀ {M : Type u_1} [_inst_1 : has_add M] {r : M → M → Prop} (x y z : M), add_con_gen.rel r x y → add_con_gen.rel r y z → add_con_gen.rel r x z
add : ∀ {M : Type u_1} [_inst_1 : has_add M] {r : M → M → Prop} (w x y z : M), add_con_gen.rel r w x → add_con_gen.rel r y z → add_con_gen.rel r (w + y) (x + z)

The inductively defined smallest additive congruence relation containing a given binary relation.

source

inductive con_gen.rel {M : Type u_1} [has_mul M] (r : M → M → Prop) :

M → M → Prop

of : ∀ {M : Type u_1} [_inst_1 : has_mul M] {r : M → M → Prop} (x y : M), r x y → con_gen.rel r x y
refl : ∀ {M : Type u_1} [_inst_1 : has_mul M] {r : M → M → Prop} (x : M), con_gen.rel r x x
symm : ∀ {M : Type u_1} [_inst_1 : has_mul M] {r : M → M → Prop} (x y : M), con_gen.rel r x y → con_gen.rel r y x
trans : ∀ {M : Type u_1} [_inst_1 : has_mul M] {r : M → M → Prop} (x y z : M), con_gen.rel r x y → con_gen.rel r y z → con_gen.rel r x z
mul : ∀ {M : Type u_1} [_inst_1 : has_mul M] {r : M → M → Prop} (w x y z : M), con_gen.rel r w x → con_gen.rel r y z → con_gen.rel r (w * y) (x * z)

The inductively defined smallest multiplicative congruence relation containing a given binary relation.

source

def add_con_gen {M : Type u_1} [has_add M] (r : M → M → Prop) :

add_con M

The inductively defined smallest additive congruence relation containing a given binary relation.

Equations

add_con_gen r = {to_setoid := {r := add_con_gen.rel r, iseqv := _}, add' := _}

source

def con_gen {M : Type u_1} [has_mul M] (r : M → M → Prop) :

con M

The inductively defined smallest multiplicative congruence relation containing a given binary relation.

Equations

con_gen r = {to_setoid := {r := con_gen.rel r, iseqv := _}, mul' := _}

source

@[protected, instance]

def con.inhabited {M : Type u_1} [has_mul M] :

inhabited (con M)

Equations

con.inhabited = {default := con_gen empty_relation}

source

@[protected, instance]

def add_con.inhabited {M : Type u_1} [has_add M] :

inhabited (add_con M)

Equations

add_con.inhabited = {default := add_con_gen empty_relation}

source

@[protected, instance]

def add_con.has_coe_to_fun {M : Type u_1} [has_add M] :

has_coe_to_fun (add_con M) (λ (_x : add_con M), M → M → Prop)

A coercion from an additive congruence relation to its underlying binary relation.

Equations

add_con.has_coe_to_fun = {coe := λ (c : add_con M) (x y : M), setoid.r x y}

source

@[protected, instance]

def con.has_coe_to_fun {M : Type u_1} [has_mul M] :

has_coe_to_fun (con M) (λ (_x : con M), M → M → Prop)

A coercion from a congruence relation to its underlying binary relation.

Equations

con.has_coe_to_fun = {coe := λ (c : con M) (x y : M), setoid.r x y}

source

@[simp]

theorem con.rel_eq_coe {M : Type u_1} [has_mul M] (c : con M) :

setoid.r = ⇑c

source

@[simp]

theorem add_con.rel_eq_coe {M : Type u_1} [has_add M] (c : add_con M) :

setoid.r = ⇑c

source

@[protected]

theorem con.refl {M : Type u_1} [has_mul M] (c : con M) (x : M) :

⇑c x x

Congruence relations are reflexive.

source

@[protected]

theorem add_con.refl {M : Type u_1} [has_add M] (c : add_con M) (x : M) :

⇑c x x

Additive congruence relations are reflexive.

source

@[protected]

theorem add_con.symm {M : Type u_1} [has_add M] (c : add_con M) {x y : M} :

⇑c x y → ⇑c y x

Additive congruence relations are symmetric.

source

@[protected]

theorem con.symm {M : Type u_1} [has_mul M] (c : con M) {x y : M} :

⇑c x y → ⇑c y x

Congruence relations are symmetric.

source

@[protected]

theorem add_con.trans {M : Type u_1} [has_add M] (c : add_con M) {x y z : M} :

⇑c x y → ⇑c y z → ⇑c x z

Additive congruence relations are transitive.

source

@[protected]

theorem con.trans {M : Type u_1} [has_mul M] (c : con M) {x y z : M} :

⇑c x y → ⇑c y z → ⇑c x z

Congruence relations are transitive.

source

@[protected]

theorem con.mul {M : Type u_1} [has_mul M] (c : con M) {w x y z : M} :

⇑c w x → ⇑c y z → ⇑c (w * y) (x * z)

Multiplicative congruence relations preserve multiplication.

source

@[protected]

theorem add_con.add {M : Type u_1} [has_add M] (c : add_con M) {w x y z : M} :

⇑c w x → ⇑c y z → ⇑c (w + y) (x + z)

Additive congruence relations preserve addition.

source

@[simp]

theorem add_con.rel_mk {M : Type u_1} [has_add M] {s : setoid M} {h : ∀ {w x y z : M}, setoid.r w x → setoid.r y z → setoid.r (w + y) (x + z)} {a b : M} :

⇑{to_setoid := s, add' := h} a b ↔ setoid.r a b

source

@[simp]

theorem con.rel_mk {M : Type u_1} [has_mul M] {s : setoid M} {h : ∀ {w x y z : M}, setoid.r w x → setoid.r y z → setoid.r (w * y) (x * z)} {a b : M} :

⇑{to_setoid := s, mul' := h} a b ↔ setoid.r a b

source

@[protected, instance]

def con.has_mem {M : Type u_1} [has_mul M] :

has_mem (M × M) (con M)

Given a type M with a multiplication, a congruence relation c on M, and elements of M x, y, (x, y) ∈ M × M iff x is related to y by c.

Equations

con.has_mem = {mem := λ (x : M × M) (c : con M), ⇑c x.fst x.snd}

source

@[protected, instance]

def add_con.has_mem {M : Type u_1} [has_add M] :

has_mem (M × M) (add_con M)

Given a type M with an addition, x, y ∈ M, and an additive congruence relation c on M, (x, y) ∈ M × M iff x is related to y by c.

Equations

add_con.has_mem = {mem := λ (x : M × M) (c : add_con M), ⇑c x.fst x.snd}

source

theorem con.ext' {M : Type u_1} [has_mul M] {c d : con M} (H : setoid.r = setoid.r) :

c = d

The map sending a congruence relation to its underlying binary relation is injective.

source

theorem add_con.ext' {M : Type u_1} [has_add M] {c d : add_con M} (H : setoid.r = setoid.r) :

c = d

The map sending an additive congruence relation to its underlying binary relation is injective.

source

@[ext]

theorem con.ext {M : Type u_1} [has_mul M] {c d : con M} (H : ∀ (x y : M), ⇑c x y ↔ ⇑d x y) :

c = d

Extensionality rule for congruence relations.

source

@[ext]

theorem add_con.ext {M : Type u_1} [has_add M] {c d : add_con M} (H : ∀ (x y : M), ⇑c x y ↔ ⇑d x y) :

c = d

Extensionality rule for additive congruence relations.

source

theorem con.to_setoid_inj {M : Type u_1} [has_mul M] {c d : con M} (H : c.to_setoid = d.to_setoid) :

c = d

The map sending a congruence relation to its underlying equivalence relation is injective.

source

theorem add_con.to_setoid_inj {M : Type u_1} [has_add M] {c d : add_con M} (H : c.to_setoid = d.to_setoid) :

c = d

The map sending an additive congruence relation to its underlying equivalence relation is injective.

source

theorem add_con.ext_iff {M : Type u_1} [has_add M] {c d : add_con M} :

(∀ (x y : M), ⇑c x y ↔ ⇑d x y) ↔ c = d

Iff version of extensionality rule for additive congruence relations.

source

theorem con.ext_iff {M : Type u_1} [has_mul M] {c d : con M} :

(∀ (x y : M), ⇑c x y ↔ ⇑d x y) ↔ c = d

Iff version of extensionality rule for congruence relations.

source

theorem con.ext'_iff {M : Type u_1} [has_mul M] {c d : con M} :

setoid.r = setoid.r ↔ c = d

Two congruence relations are equal iff their underlying binary relations are equal.

source

theorem add_con.ext'_iff {M : Type u_1} [has_add M] {c d : add_con M} :

setoid.r = setoid.r ↔ c = d

Two additive congruence relations are equal iff their underlying binary relations are equal.

source

def add_con.add_ker {M : Type u_1} {P : Type u_3} [has_add M] [has_add P] (f : M → P) (h : ∀ (x y : M), f (x + y) = f x + f y) :

add_con M

The kernel of an addition-preserving function as an additive congruence relation.

Equations

add_con.add_ker f h = {to_setoid := setoid.ker f, add' := _}

source

def con.mul_ker {M : Type u_1} {P : Type u_3} [has_mul M] [has_mul P] (f : M → P) (h : ∀ (x y : M), f (x * y) = f x * f y) :

con M

The kernel of a multiplication-preserving function as a congruence relation.

Equations

con.mul_ker f h = {to_setoid := setoid.ker f, mul' := _}

source

@[protected]

def con.prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (c : con M) (d : con N) :

con (M × N)

Given types with multiplications M, N, the product of two congruence relations c on M and d on N: (x₁, x₂), (y₁, y₂) ∈ M × N are related by c.prod d iff x₁ is related to y₁ by c and x₂ is related to y₂ by d.

Equations

c.prod d = {to_setoid := {r := setoid.r (c.to_setoid.prod d.to_setoid), iseqv := _}, mul' := _}

source

@[protected]

def add_con.prod {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (c : add_con M) (d : add_con N) :

add_con (M × N)

Given types with additions M, N, the product of two congruence relations c on M and d on N: (x₁, x₂), (y₁, y₂) ∈ M × N are related by c.prod d iff x₁ is related to y₁ by c and x₂ is related to y₂ by d.

Equations

c.prod d = {to_setoid := {r := setoid.r (c.to_setoid.prod d.to_setoid), iseqv := _}, add' := _}

source

def con.pi {ι : Type u_1} {f : ι → Type u_2} [Π (i : ι), has_mul (f i)] (C : Π (i : ι), con (f i)) :

con (Π (i : ι), f i)

The product of an indexed collection of congruence relations.

Equations

con.pi C = {to_setoid := {r := setoid.r pi_setoid, iseqv := _}, mul' := _}

source

def add_con.pi {ι : Type u_1} {f : ι → Type u_2} [Π (i : ι), has_add (f i)] (C : Π (i : ι), add_con (f i)) :

add_con (Π (i : ι), f i)

The product of an indexed collection of additive congruence relations.

Equations

add_con.pi C = {to_setoid := {r := setoid.r pi_setoid, iseqv := _}, add' := _}

source

@[protected]

def add_con.quotient {M : Type u_1} [has_add M] (c : add_con M) :

Type u_1

Defining the quotient by an additive congruence relation of a type with an addition.

Equations

c.quotient = quotient c.to_setoid

Instances for add_con.quotient

source

@[protected]

def con.quotient {M : Type u_1} [has_mul M] (c : con M) :

Type u_1

Defining the quotient by a congruence relation of a type with a multiplication.

Equations

c.quotient = quotient c.to_setoid

Instances for con.quotient

source

@[protected, instance]

def con.quotient.has_coe_t {M : Type u_1} [has_mul M] (c : con M) :

has_coe_t M c.quotient

Coercion from a type with a multiplication to its quotient by a congruence relation.

See Note [use has_coe_t].

Equations

con.quotient.has_coe_t c = {coe := quotient.mk c.to_setoid}

source

@[protected, instance]

def add_con.quotient.has_coe_t {M : Type u_1} [has_add M] (c : add_con M) :

has_coe_t M c.quotient

Coercion from a type with an addition to its quotient by an additive congruence relation

Equations

add_con.quotient.has_coe_t c = {coe := quotient.mk c.to_setoid}

source

@[protected, instance]

def con.quotient.decidable_eq {M : Type u_1} [has_mul M] (c : con M) [d : Π (a b : M), decidable (⇑c a b)] :

decidable_eq c.quotient

The quotient by a decidable congruence relation has decidable equality.

Equations

con.quotient.decidable_eq c = quotient.decidable_eq

source

@[protected, instance]

def add_con.quotient.decidable_eq {M : Type u_1} [has_add M] (c : add_con M) [d : Π (a b : M), decidable (⇑c a b)] :

decidable_eq c.quotient

The quotient by a decidable additive congruence relation has decidable equality.

Equations

add_con.quotient.decidable_eq c = quotient.decidable_eq

source

@[simp]

theorem con.quot_mk_eq_coe {M : Type u_1} [has_mul M] (c : con M) (x : M) :

quot.mk ⇑c x = ↑x

source

@[simp]

theorem add_con.quot_mk_eq_coe {M : Type u_1} [has_add M] (c : add_con M) (x : M) :

quot.mk ⇑c x = ↑x

source

@[protected]

def con.lift_on {M : Type u_1} [has_mul M] {β : Sort u_2} {c : con M} (q : c.quotient) (f : M → β) (h : ∀ (a b : M), ⇑c a b → f a = f b) :

β

The function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

Equations

con.lift_on q f h = quotient.lift_on' q f h

source

@[protected]

def add_con.lift_on {M : Type u_1} [has_add M] {β : Sort u_2} {c : add_con M} (q : c.quotient) (f : M → β) (h : ∀ (a b : M), ⇑c a b → f a = f b) :

β

The function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

Equations

add_con.lift_on q f h = quotient.lift_on' q f h

source

@[protected]

def add_con.lift_on₂ {M : Type u_1} [has_add M] {β : Sort u_2} {c : add_con M} (q r : c.quotient) (f : M → M → β) (h : ∀ (a₁ a₂ b₁ b₂ : M), ⇑c a₁ b₁ → ⇑c a₂ b₂ → f a₁ a₂ = f b₁ b₂) :

β

The binary function on the quotient by a congruence relation c induced by a binary function that is constant on c's equivalence classes.

Equations

add_con.lift_on₂ q r f h = quotient.lift_on₂' q r f h

source

@[protected]

def con.lift_on₂ {M : Type u_1} [has_mul M] {β : Sort u_2} {c : con M} (q r : c.quotient) (f : M → M → β) (h : ∀ (a₁ a₂ b₁ b₂ : M), ⇑c a₁ b₁ → ⇑c a₂ b₂ → f a₁ a₂ = f b₁ b₂) :

β

The binary function on the quotient by a congruence relation c induced by a binary function that is constant on c's equivalence classes.

Equations

con.lift_on₂ q r f h = quotient.lift_on₂' q r f h

source

@[protected]

def add_con.hrec_on₂ {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {cM : add_con M} {cN : add_con N} {φ : cM.quotient → cN.quotient → Sort u_3} (a : cM.quotient) (b : cN.quotient) (f : Π (x : M) (y : N), φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ⇑cM x x' → ⇑cN y y' → f x y == f x' y') :

φ a b

A version of quotient.hrec_on₂' for quotients by add_con.

Equations

add_con.hrec_on₂ a b f h = quotient.hrec_on₂' a b f h

source

@[protected]

def con.hrec_on₂ {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {cM : con M} {cN : con N} {φ : cM.quotient → cN.quotient → Sort u_3} (a : cM.quotient) (b : cN.quotient) (f : Π (x : M) (y : N), φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ⇑cM x x' → ⇑cN y y' → f x y == f x' y') :

φ a b

A version of quotient.hrec_on₂' for quotients by con.

Equations

con.hrec_on₂ a b f h = quotient.hrec_on₂' a b f h

source

@[simp]

theorem add_con.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {cM : add_con M} {cN : add_con N} {φ : cM.quotient → cN.quotient → Sort u_3} (a : M) (b : N) (f : Π (x : M) (y : N), φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ⇑cM x x' → ⇑cN y y' → f x y == f x' y') :

add_con.hrec_on₂ ↑a ↑b f h = f a b

source

@[simp]

theorem con.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {cM : con M} {cN : con N} {φ : cM.quotient → cN.quotient → Sort u_3} (a : M) (b : N) (f : Π (x : M) (y : N), φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ⇑cM x x' → ⇑cN y y' → f x y == f x' y') :

con.hrec_on₂ ↑a ↑b f h = f a b

source

@[protected]

theorem add_con.induction_on {M : Type u_1} [has_add M] {c : add_con M} {C : c.quotient → Prop} (q : c.quotient) (H : ∀ (x : M), C ↑x) :

C q

The inductive principle used to prove propositions about the elements of a quotient by an additive congruence relation.

source

@[protected]

theorem con.induction_on {M : Type u_1} [has_mul M] {c : con M} {C : c.quotient → Prop} (q : c.quotient) (H : ∀ (x : M), C ↑x) :

C q

The inductive principle used to prove propositions about the elements of a quotient by a congruence relation.

source

@[protected]

theorem con.induction_on₂ {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {c : con M} {d : con N} {C : c.quotient → d.quotient → Prop} (p : c.quotient) (q : d.quotient) (H : ∀ (x : M) (y : N), C ↑x ↑y) :

C p q

A version of con.induction_on for predicates which take two arguments.

source

@[protected]

theorem add_con.induction_on₂ {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {c : add_con M} {d : add_con N} {C : c.quotient → d.quotient → Prop} (p : c.quotient) (q : d.quotient) (H : ∀ (x : M) (y : N), C ↑x ↑y) :

C p q

A version of add_con.induction_on for predicates which take two arguments.

source

@[protected, simp]

theorem con.eq {M : Type u_1} [has_mul M] (c : con M) {a b : M} :

↑a = ↑b ↔ ⇑c a b

Two elements are related by a congruence relation c iff they are represented by the same element of the quotient by c.

source

@[protected, simp]

theorem add_con.eq {M : Type u_1} [has_add M] (c : add_con M) {a b : M} :

↑a = ↑b ↔ ⇑c a b

Two elements are related by an additive congruence relation c iff they are represented by the same element of the quotient by c.

source

@[protected, instance]

def con.has_mul {M : Type u_1} [has_mul M] (c : con M) :

has_mul c.quotient

The multiplication induced on the quotient by a congruence relation on a type with a multiplication.

Equations

c.has_mul = {mul := quotient.map₂' has_mul.mul _}

source

@[protected, instance]

def add_con.has_add {M : Type u_1} [has_add M] (c : add_con M) :

has_add c.quotient

The addition induced on the quotient by an additive congruence relation on a type with an addition.

Equations

c.has_add = {add := quotient.map₂' has_add.add _}

source

@[simp]

theorem con.mul_ker_mk_eq {M : Type u_1} [has_mul M] (c : con M) :

con.mul_ker coe _ = c

The kernel of the quotient map induced by a congruence relation c equals c.

source

@[simp]

theorem add_con.add_ker_mk_eq {M : Type u_1} [has_add M] (c : add_con M) :

add_con.add_ker coe _ = c

The kernel of the quotient map induced by an additive congruence relation c equals c.

source

@[simp]

theorem con.coe_mul {M : Type u_1} [has_mul M] {c : con M} (x y : M) :

↑(x * y) = ↑x * ↑y

The coercion to the quotient of a congruence relation commutes with multiplication (by definition).

source

@[simp]

theorem add_con.coe_add {M : Type u_1} [has_add M] {c : add_con M} (x y : M) :

↑(x + y) = ↑x + ↑y

The coercion to the quotient of an additive congruence relation commutes with addition (by definition).

source

@[protected, simp]

theorem con.lift_on_coe {M : Type u_1} [has_mul M] {β : Sort u_2} (c : con M) (f : M → β) (h : ∀ (a b : M), ⇑c a b → f a = f b) (x : M) :

con.lift_on ↑x f h = f x

Definition of the function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

source

@[protected, simp]

theorem add_con.lift_on_coe {M : Type u_1} [has_add M] {β : Sort u_2} (c : add_con M) (f : M → β) (h : ∀ (a b : M), ⇑c a b → f a = f b) (x : M) :

add_con.lift_on ↑x f h = f x

Definition of the function on the quotient by an additive congruence relation c induced by a function that is constant on c's equivalence classes.

source

@[protected]

def add_con.congr {M : Type u_1} [has_add M] {c d : add_con M} (h : c = d) :

c.quotient ≃+ d.quotient

Makes an additive isomorphism of quotients by two additive congruence relations, given that the relations are equal.

Equations

add_con.congr h = {to_fun := (quotient.congr (equiv.refl M) _).to_fun, inv_fun := (quotient.congr (equiv.refl M) _).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[protected]

def con.congr {M : Type u_1} [has_mul M] {c d : con M} (h : c = d) :

c.quotient ≃* d.quotient

Makes an isomorphism of quotients by two congruence relations, given that the relations are equal.

Equations

con.congr h = {to_fun := (quotient.congr (equiv.refl M) _).to_fun, inv_fun := (quotient.congr (equiv.refl M) _).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[protected, instance]

def con.has_le {M : Type u_1} [has_mul M] :

has_le (con M)

For congruence relations c, d on a type M with a multiplication, c ≤ d iff ∀ x y ∈ M, x is related to y by d if x is related to y by c.

Equations

con.has_le = {le := λ (c d : con M), ∀ ⦃x y : M⦄, ⇑c x y → ⇑d x y}

source

@[protected, instance]

def add_con.has_le {M : Type u_1} [has_add M] :

has_le (add_con M)

For additive congruence relations c, d on a type M with an addition, c ≤ d iff ∀ x y ∈ M, x is related to y by d if x is related to y by c.

Equations

add_con.has_le = {le := λ (c d : add_con M), ∀ ⦃x y : M⦄, ⇑c x y → ⇑d x y}

source

theorem con.le_def {M : Type u_1} [has_mul M] {c d : con M} :

c ≤ d ↔ ∀ {x y : M}, ⇑c x y → ⇑d x y

Definition of ≤ for congruence relations.

source

theorem add_con.le_def {M : Type u_1} [has_add M] {c d : add_con M} :

c ≤ d ↔ ∀ {x y : M}, ⇑c x y → ⇑d x y

Definition of ≤ for additive congruence relations.

source

@[protected, instance]

def add_con.has_Inf {M : Type u_1} [has_add M] :

has_Inf (add_con M)

The infimum of a set of additive congruence relations on a given type with an addition.

Equations

add_con.has_Inf = {Inf := λ (S : set (add_con M)), {to_setoid := {r := λ (x y : M), ∀ (c : add_con M), c ∈ S → ⇑c x y, iseqv := _}, add' := _}}

source

@[protected, instance]

def con.has_Inf {M : Type u_1} [has_mul M] :

has_Inf (con M)

The infimum of a set of congruence relations on a given type with a multiplication.

Equations

con.has_Inf = {Inf := λ (S : set (con M)), {to_setoid := {r := λ (x y : M), ∀ (c : con M), c ∈ S → ⇑c x y, iseqv := _}, mul' := _}}

source

theorem add_con.Inf_to_setoid {M : Type u_1} [has_add M] (S : set (add_con M)) :

(has_Inf.Inf S).to_setoid = has_Inf.Inf (add_con.to_setoid '' S)

The infimum of a set of additive congruence relations is the same as the infimum of the set's image under the map to the underlying equivalence relation.

source

theorem con.Inf_to_setoid {M : Type u_1} [has_mul M] (S : set (con M)) :

(has_Inf.Inf S).to_setoid = has_Inf.Inf (con.to_setoid '' S)

The infimum of a set of congruence relations is the same as the infimum of the set's image under the map to the underlying equivalence relation.

source

theorem add_con.Inf_def {M : Type u_1} [has_add M] (S : set (add_con M)) :

⇑(has_Inf.Inf S) = has_Inf.Inf (coe_fn '' S)

The infimum of a set of additive congruence relations is the same as the infimum of the set's image under the map to the underlying binary relation.

source

theorem con.Inf_def {M : Type u_1} [has_mul M] (S : set (con M)) :

⇑(has_Inf.Inf S) = has_Inf.Inf (coe_fn '' S)

The infimum of a set of congruence relations is the same as the infimum of the set's image under the map to the underlying binary relation.

source

@[protected, instance]

def add_con.partial_order {M : Type u_1} [has_add M] :

partial_order (add_con M)

Equations

add_con.partial_order = {le := has_le.le add_con.has_le, lt := λ (c d : add_con M), c ≤ d ∧ ¬d ≤ c, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def con.partial_order {M : Type u_1} [has_mul M] :

partial_order (con M)

Equations

con.partial_order = {le := has_le.le con.has_le, lt := λ (c d : con M), c ≤ d ∧ ¬d ≤ c, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def con.complete_lattice {M : Type u_1} [has_mul M] :

complete_lattice (con M)

The complete lattice of congruence relations on a given type with a multiplication.

Equations

con.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (con M) con.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (con M) con.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (con M) con.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (c d : con M), {to_setoid := c.to_setoid ⊓ d.to_setoid, mul' := _}, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (con M) con.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (con M) con.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := {to_setoid := {r := setoid.r complete_lattice.top, iseqv := _}, mul' := _}, bot := {to_setoid := {r := setoid.r complete_lattice.bot, iseqv := _}, mul' := _}, le_top := _, bot_le := _}

source

@[protected, instance]

def add_con.complete_lattice {M : Type u_1} [has_add M] :

complete_lattice (add_con M)

The complete lattice of additive congruence relations on a given type with an addition.

Equations

add_con.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_con M) add_con.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (add_con M) add_con.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (add_con M) add_con.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (c d : add_con M), {to_setoid := c.to_setoid ⊓ d.to_setoid, add' := _}, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_con M) add_con.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (add_con M) add_con.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := {to_setoid := {r := setoid.r complete_lattice.top, iseqv := _}, add' := _}, bot := {to_setoid := {r := setoid.r complete_lattice.bot, iseqv := _}, add' := _}, le_top := _, bot_le := _}

source

theorem con.inf_def {M : Type u_1} [has_mul M] {c d : con M} :

setoid.r = setoid.r ⊓ setoid.r

The infimum of two congruence relations equals the infimum of the underlying binary operations.

source

theorem add_con.inf_def {M : Type u_1} [has_add M] {c d : add_con M} :

setoid.r = setoid.r ⊓ setoid.r

The infimum of two additive congruence relations equals the infimum of the underlying binary operations.

source

theorem con.inf_iff_and {M : Type u_1} [has_mul M] {c d : con M} {x y : M} :

⇑(c ⊓ d) x y ↔ ⇑c x y ∧ ⇑d x y

Definition of the infimum of two congruence relations.

source

theorem add_con.inf_iff_and {M : Type u_1} [has_add M] {c d : add_con M} {x y : M} :

⇑(c ⊓ d) x y ↔ ⇑c x y ∧ ⇑d x y

Definition of the infimum of two additive congruence relations.

source

theorem add_con.add_con_gen_eq {M : Type u_1} [has_add M] (r : M → M → Prop) :

add_con_gen r = has_Inf.Inf {s : add_con M | ∀ (x y : M), r x y → ⇑s x y}

The inductively defined smallest additive congruence relation containing a binary relation r equals the infimum of the set of additive congruence relations containing r.

source

theorem con.con_gen_eq {M : Type u_1} [has_mul M] (r : M → M → Prop) :

con_gen r = has_Inf.Inf {s : con M | ∀ (x y : M), r x y → ⇑s x y}

The inductively defined smallest congruence relation containing a binary relation r equals the infimum of the set of congruence relations containing r.

source

theorem con.con_gen_le {M : Type u_1} [has_mul M] {r : M → M → Prop} {c : con M} (h : ∀ (x y : M), r x y → setoid.r x y) :

con_gen r ≤ c

The smallest congruence relation containing a binary relation r is contained in any congruence relation containing r.

source

theorem add_con.add_con_gen_le {M : Type u_1} [has_add M] {r : M → M → Prop} {c : add_con M} (h : ∀ (x y : M), r x y → setoid.r x y) :

add_con_gen r ≤ c

The smallest additive congruence relation containing a binary relation r is contained in any additive congruence relation containing r.

source

theorem add_con.add_con_gen_mono {M : Type u_1} [has_add M] {r s : M → M → Prop} (h : ∀ (x y : M), r x y → s x y) :

add_con_gen r ≤ add_con_gen s

Given binary relations r, s with r contained in s, the smallest additive congruence relation containing s contains the smallest additive congruence relation containing r.

source

theorem con.con_gen_mono {M : Type u_1} [has_mul M] {r s : M → M → Prop} (h : ∀ (x y : M), r x y → s x y) :

con_gen r ≤ con_gen s

Given binary relations r, s with r contained in s, the smallest congruence relation containing s contains the smallest congruence relation containing r.

source

@[simp]

theorem add_con.add_con_gen_of_add_con {M : Type u_1} [has_add M] (c : add_con M) :

add_con_gen ⇑c = c

Additive congruence relations equal the smallest additive congruence relation in which they are contained.

source

@[simp]

theorem con.con_gen_of_con {M : Type u_1} [has_mul M] (c : con M) :

con_gen ⇑c = c

Congruence relations equal the smallest congruence relation in which they are contained.

source

@[simp]

theorem add_con.add_con_gen_idem {M : Type u_1} [has_add M] (r : M → M → Prop) :

add_con_gen ⇑(add_con_gen r) = add_con_gen r

The map sending a binary relation to the smallest additive congruence relation in which it is contained is idempotent.

source

@[simp]

theorem con.con_gen_idem {M : Type u_1} [has_mul M] (r : M → M → Prop) :

con_gen ⇑(con_gen r) = con_gen r

The map sending a binary relation to the smallest congruence relation in which it is contained is idempotent.

source

theorem add_con.sup_eq_add_con_gen {M : Type u_1} [has_add M] (c d : add_con M) :

c ⊔ d = add_con_gen (λ (x y : M), ⇑c x y ∨ ⇑d x y)

The supremum of additive congruence relations c, d equals the smallest additive congruence relation containing the binary relation 'x is related to y by c or d'.

source

theorem con.sup_eq_con_gen {M : Type u_1} [has_mul M] (c d : con M) :

c ⊔ d = con_gen (λ (x y : M), ⇑c x y ∨ ⇑d x y)

The supremum of congruence relations c, d equals the smallest congruence relation containing the binary relation 'x is related to y by c or d'.

source

theorem con.sup_def {M : Type u_1} [has_mul M] {c d : con M} :

c ⊔ d = con_gen (setoid.r ⊔ setoid.r)

The supremum of two congruence relations equals the smallest congruence relation containing the supremum of the underlying binary operations.

source

theorem add_con.sup_def {M : Type u_1} [has_add M] {c d : add_con M} :

c ⊔ d = add_con_gen (setoid.r ⊔ setoid.r)

The supremum of two additive congruence relations equals the smallest additive congruence relation containing the supremum of the underlying binary operations.

source

theorem con.Sup_eq_con_gen {M : Type u_1} [has_mul M] (S : set (con M)) :

has_Sup.Sup S = con_gen (λ (x y : M), ∃ (c : con M), c ∈ S ∧ ⇑c x y)

The supremum of a set of congruence relations S equals the smallest congruence relation containing the binary relation 'there exists c ∈ S such that x is related to y by c'.

source

theorem add_con.Sup_eq_add_con_gen {M : Type u_1} [has_add M] (S : set (add_con M)) :

has_Sup.Sup S = add_con_gen (λ (x y : M), ∃ (c : add_con M), c ∈ S ∧ ⇑c x y)

The supremum of a set of additive congruence relations S equals the smallest additive congruence relation containing the binary relation 'there exists c ∈ S such that x is related to y by c'.

source

theorem add_con.Sup_def {M : Type u_1} [has_add M] {S : set (add_con M)} :

has_Sup.Sup S = add_con_gen (has_Sup.Sup (coe_fn '' S))

The supremum of a set of additive congruence relations is the same as the smallest additive congruence relation containing the supremum of the set's image under the map to the underlying binary relation.

source

theorem con.Sup_def {M : Type u_1} [has_mul M] {S : set (con M)} :

has_Sup.Sup S = con_gen (has_Sup.Sup (coe_fn '' S))

The supremum of a set of congruence relations is the same as the smallest congruence relation containing the supremum of the set's image under the map to the underlying binary relation.

source

@[protected]

def con.gi (M : Type u_1) [has_mul M] :

galois_insertion con_gen coe_fn

There is a Galois insertion of congruence relations on a type with a multiplication M into binary relations on M.

Equations

con.gi M = {choice := λ (r : M → M → Prop) (h : ⇑(con_gen r) ≤ r), con_gen r, gc := _, le_l_u := _, choice_eq := _}

source

@[protected]

def add_con.gi (M : Type u_1) [has_add M] :

galois_insertion add_con_gen coe_fn

There is a Galois insertion of additive congruence relations on a type with an addition M into binary relations on M.

Equations

add_con.gi M = {choice := λ (r : M → M → Prop) (h : ⇑(add_con_gen r) ≤ r), add_con_gen r, gc := _, le_l_u := _, choice_eq := _}

source

def add_con.map_gen {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (c : add_con M) (f : M → N) :

add_con N

Given a function f, the smallest additive congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by an additive congruence relation c.'

Equations

c.map_gen f = add_con_gen (λ (x y : N), ∃ (a b : M), f a = x ∧ f b = y ∧ ⇑c a b)

source

def con.map_gen {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (c : con M) (f : M → N) :

con N

Given a function f, the smallest congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by a congruence relation c.'

Equations

c.map_gen f = con_gen (λ (x y : N), ∃ (a b : M), f a = x ∧ f b = y ∧ ⇑c a b)

source

def con.map_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (c : con M) (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (h : con.mul_ker f H ≤ c) (hf : function.surjective f) :

con N

Given a surjective multiplicative-preserving function f whose kernel is contained in a congruence relation c, the congruence relation on f's codomain defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by c.'

Equations

c.map_of_surjective f H h hf = {to_setoid := {r := setoid.r (c.to_setoid.map_of_surjective f h hf), iseqv := _}, mul' := _}

source

def add_con.map_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (c : add_con M) (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (h : add_con.add_ker f H ≤ c) (hf : function.surjective f) :

add_con N

Given a surjective addition-preserving function f whose kernel is contained in an additive congruence relation c, the additive congruence relation on f's codomain defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by c.'

Equations

c.map_of_surjective f H h hf = {to_setoid := {r := setoid.r (c.to_setoid.map_of_surjective f h hf), iseqv := _}, add' := _}

source

theorem add_con.map_of_surjective_eq_map_gen {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {c : add_con M} {f : M → N} (H : ∀ (x y : M), f (x + y) = f x + f y) (h : add_con.add_ker f H ≤ c) (hf : function.surjective f) :

c.map_gen f = c.map_of_surjective f H h hf

A specialization of 'the smallest additive congruence relation containing an additive congruence relation c equals c'.

source

theorem con.map_of_surjective_eq_map_gen {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {c : con M} {f : M → N} (H : ∀ (x y : M), f (x * y) = f x * f y) (h : con.mul_ker f H ≤ c) (hf : function.surjective f) :

c.map_gen f = c.map_of_surjective f H h hf

A specialization of 'the smallest congruence relation containing a congruence relation c equals c'.

source

def con.comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (c : con N) :

con M

Given types with multiplications M, N and a congruence relation c on N, a multiplication-preserving map f : M → N induces a congruence relation on f's domain defined by 'x ≈ y iff f(x) is related to f(y) by c.'

Equations

con.comap f H c = {to_setoid := {r := setoid.r (setoid.comap f c.to_setoid), iseqv := _}, mul' := _}

source

def add_con.comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (c : add_con N) :

add_con M

Given types with additions M, N and an additive congruence relation c on N, an addition-preserving map f : M → N induces an additive congruence relation on f's domain defined by 'x ≈ y iff f(x) is related to f(y) by c.'

Equations

add_con.comap f H c = {to_setoid := {r := setoid.r (setoid.comap f c.to_setoid), iseqv := _}, add' := _}

source

@[simp]

theorem add_con.comap_rel {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : M → N} (H : ∀ (x y : M), f (x + y) = f x + f y) {c : add_con N} {x y : M} :

⇑(add_con.comap f H c) x y ↔ ⇑c (f x) (f y)

source

@[simp]

theorem con.comap_rel {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M → N} (H : ∀ (x y : M), f (x * y) = f x * f y) {c : con N} {x y : M} :

⇑(con.comap f H c) x y ↔ ⇑c (f x) (f y)

source

def con.correspondence {M : Type u_1} [has_mul M] (c : con M) :

{d // c ≤ d} ≃o con c.quotient

Given a congruence relation c on a type M with a multiplication, the order-preserving bijection between the set of congruence relations containing c and the congruence relations on the quotient of M by c.

Equations

c.correspondence = {to_equiv := {to_fun := λ (d : {d // c ≤ d}), d.val.map_of_surjective coe _ _ _, inv_fun := λ (d : con c.quotient), ⟨con.comap coe _ d, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

def add_con.correspondence {M : Type u_1} [has_add M] (c : add_con M) :

{d // c ≤ d} ≃o add_con c.quotient

Given an additive congruence relation c on a type M with an addition, the order-preserving bijection between the set of additive congruence relations containing c and the additive congruence relations on the quotient of M by c.

Equations

c.correspondence = {to_equiv := {to_fun := λ (d : {d // c ≤ d}), d.val.map_of_surjective coe _ _ _, inv_fun := λ (d : add_con c.quotient), ⟨add_con.comap coe _ d, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[protected, instance]

def con.mul_one_class {M : Type u_1} [mul_one_class M] (c : con M) :

mul_one_class c.quotient

The quotient of a monoid by a congruence relation is a monoid.

Equations

c.mul_one_class = {one := ↑1, mul := has_mul.mul c.has_mul, one_mul := _, mul_one := _}

source

@[protected, instance]

def add_con.add_zero_class {M : Type u_1} [add_zero_class M] (c : add_con M) :

add_zero_class c.quotient

The quotient of an add_monoid by an additive congruence relation is an add_monoid.

Equations

c.add_zero_class = {zero := ↑0, add := has_add.add c.has_add, zero_add := _, add_zero := _}

source

@[simp]

theorem con.coe_one {M : Type u_1} [mul_one_class M] {c : con M} :

↑1 = 1

The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the monoid's 1.

source

@[simp]

theorem add_con.coe_zero {M : Type u_1} [add_zero_class M] {c : add_con M} :

↑0 = 0

The 0 of the quotient of an add_monoid by an additive congruence relation is the equivalence class of the add_monoid's 0.

source

@[protected]

def con.submonoid (M : Type u_1) [mul_one_class M] (c : con M) :

submonoid (M × M)

The submonoid of M × M defined by a congruence relation on a monoid M.

Equations

con.submonoid M c = {carrier := {x : M × M | ⇑c x.fst x.snd}, mul_mem' := _, one_mem' := _}

source

@[protected]

def add_con.add_submonoid (M : Type u_1) [add_zero_class M] (c : add_con M) :

add_submonoid (M × M)

The add_submonoid of M × M defined by an additive congruence relation on an add_monoid M.

Equations

add_con.add_submonoid M c = {carrier := {x : M × M | ⇑c x.fst x.snd}, add_mem' := _, zero_mem' := _}

source

def con.of_submonoid {M : Type u_1} [mul_one_class M] (N : submonoid (M × M)) (H : equivalence (λ (x y : M), (x, y) ∈ N)) :

con M

The congruence relation on a monoid M from a submonoid of M × M for which membership is an equivalence relation.

Equations

con.of_submonoid N H = {to_setoid := {r := λ (x y : M), (x, y) ∈ N, iseqv := H}, mul' := _}

source

def add_con.of_add_submonoid {M : Type u_1} [add_zero_class M] (N : add_submonoid (M × M)) (H : equivalence (λ (x y : M), (x, y) ∈ N)) :

add_con M

The additive congruence relation on an add_monoid M from an add_submonoid of M × M for which membership is an equivalence relation.

Equations

add_con.of_add_submonoid N H = {to_setoid := {r := λ (x y : M), (x, y) ∈ N, iseqv := H}, add' := _}

source

@[protected, instance]

def con.to_submonoid {M : Type u_1} [mul_one_class M] :

has_coe (con M) (submonoid (M × M))

Coercion from a congruence relation c on a monoid M to the submonoid of M × M whose elements are (x, y) such that x is related to y by c.

Equations

con.to_submonoid = {coe := λ (c : con M), con.submonoid M c}

source

@[protected, instance]

def add_con.to_add_submonoid {M : Type u_1} [add_zero_class M] :

has_coe (add_con M) (add_submonoid (M × M))

Coercion from a congruence relation c on an add_monoid M to the add_submonoid of M × M whose elements are (x, y) such that x is related to y by c.

Equations

add_con.to_add_submonoid = {coe := λ (c : add_con M), add_con.add_submonoid M c}

source

theorem con.mem_coe {M : Type u_1} [mul_one_class M] {c : con M} {x y : M} :

(x, y) ∈ ↑c ↔ (x, y) ∈ c

source

theorem add_con.mem_coe {M : Type u_1} [add_zero_class M] {c : add_con M} {x y : M} :

(x, y) ∈ ↑c ↔ (x, y) ∈ c

source

theorem add_con.to_add_submonoid_inj {M : Type u_1} [add_zero_class M] (c d : add_con M) (H : ↑c = ↑d) :

c = d

source

theorem con.to_submonoid_inj {M : Type u_1} [mul_one_class M] (c d : con M) (H : ↑c = ↑d) :

c = d

source

theorem add_con.le_iff {M : Type u_1} [add_zero_class M] {c d : add_con M} :

c ≤ d ↔ ↑c ≤ ↑d

source

theorem con.le_iff {M : Type u_1} [mul_one_class M] {c d : con M} :

c ≤ d ↔ ↑c ≤ ↑d

source

def con.ker {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) :

con M

The kernel of a monoid homomorphism as a congruence relation.

Equations

con.ker f = con.mul_ker ⇑f _

source

def add_con.ker {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) :

add_con M

The kernel of an add_monoid homomorphism as an additive congruence relation.

Equations

add_con.ker f = add_con.add_ker ⇑f _

source

@[simp]

theorem con.ker_rel {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) {x y : M} :

⇑(con.ker f) x y ↔ ⇑f x = ⇑f y

The definition of the congruence relation defined by a monoid homomorphism's kernel.

source

@[simp]

theorem add_con.ker_rel {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) {x y : M} :

⇑(add_con.ker f) x y ↔ ⇑f x = ⇑f y

The definition of the additive congruence relation defined by an add_monoid homomorphism's kernel.

source

@[protected, instance]

def add_con.quotient.inhabited {M : Type u_1} [add_zero_class M] {c : add_con M} :

inhabited c.quotient

There exists an element of the quotient of an add_monoid by a congruence relation (namely 0).

Equations

add_con.quotient.inhabited = {default := ↑0}

source

@[protected, instance]

def con.quotient.inhabited {M : Type u_1} [mul_one_class M] {c : con M} :

inhabited c.quotient

There exists an element of the quotient of a monoid by a congruence relation (namely 1).

Equations

con.quotient.inhabited = {default := ↑1}

source

def con.mk' {M : Type u_1} [mul_one_class M] (c : con M) :

M →* c.quotient

The natural homomorphism from a monoid to its quotient by a congruence relation.

Equations

c.mk' = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}

source

def add_con.mk' {M : Type u_1} [add_zero_class M] (c : add_con M) :

M →+ c.quotient

The natural homomorphism from an add_monoid to its quotient by an additive congruence relation.

Equations

c.mk' = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

theorem con.mk'_ker {M : Type u_1} [mul_one_class M] (c : con M) :

con.ker c.mk' = c

The kernel of the natural homomorphism from a monoid to its quotient by a congruence relation c equals c.

source

@[simp]

theorem add_con.mk'_ker {M : Type u_1} [add_zero_class M] (c : add_con M) :

add_con.ker c.mk' = c

The kernel of the natural homomorphism from an add_monoid to its quotient by an additive congruence relation c equals c.

source

theorem con.mk'_surjective {M : Type u_1} [mul_one_class M] {c : con M} :

function.surjective ⇑(c.mk')

The natural homomorphism from a monoid to its quotient by a congruence relation is surjective.

source

theorem add_con.mk'_surjective {M : Type u_1} [add_zero_class M] {c : add_con M} :

function.surjective ⇑(c.mk')

The natural homomorphism from an add_monoid to its quotient by a congruence relation is surjective.

source

@[simp]

theorem add_con.coe_mk' {M : Type u_1} [add_zero_class M] {c : add_con M} :

⇑(c.mk') = coe

source

@[simp]

theorem con.coe_mk' {M : Type u_1} [mul_one_class M] {c : con M} :

⇑(c.mk') = coe

source

@[simp]

theorem con.mrange_mk' {M : Type u_1} [mul_one_class M] {c : con M} :

monoid_hom.mrange c.mk' = ⊤

source

@[simp]

theorem add_con.mrange_mk' {M : Type u_1} [add_zero_class M] {c : add_con M} :

add_monoid_hom.mrange c.mk' = ⊤

source

theorem add_con.ker_apply_eq_preimage {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {f : M →+ P} (x : M) :

⇑(add_con.ker f) x = ⇑f ⁻¹' {⇑f x}

The elements related to x ∈ M, M an add_monoid, by the kernel of an add_monoid homomorphism are those in the preimage of f(x) under f.

source

theorem con.ker_apply_eq_preimage {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {f : M →* P} (x : M) :

⇑(con.ker f) x = ⇑f ⁻¹' {⇑f x}

The elements related to x ∈ M, M a monoid, by the kernel of a monoid homomorphism are those in the preimage of f(x) under f.

source

theorem con.comap_eq {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {c : con M} {f : N →* M} :

con.comap ⇑f _ c = con.ker (c.mk'.comp f)

Given a monoid homomorphism f : N → M and a congruence relation c on M, the congruence relation induced on N by f equals the kernel of c's quotient homomorphism composed with f.

source

theorem add_con.comap_eq {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {c : add_con M} {f : N →+ M} :

add_con.comap ⇑f _ c = add_con.ker (c.mk'.comp f)

Given an add_monoid homomorphism f : N → M and an additive congruence relation c on M, the additive congruence relation induced on N by f equals the kernel of c's quotient homomorphism composed with f.

source

def con.lift {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (c : con M) (f : M →* P) (H : c ≤ con.ker f) :

c.quotient →* P

The homomorphism on the quotient of a monoid by a congruence relation c induced by a homomorphism constant on c's equivalence classes.

Equations

c.lift f H = {to_fun := λ (x : c.quotient), con.lift_on x ⇑f _, map_one' := _, map_mul' := _}

source

def add_con.lift {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (c : add_con M) (f : M →+ P) (H : c ≤ add_con.ker f) :

c.quotient →+ P

The homomorphism on the quotient of an add_monoid by an additive congruence relation c induced by a homomorphism constant on c's equivalence classes.

Equations

c.lift f H = {to_fun := λ (x : c.quotient), add_con.lift_on x ⇑f _, map_zero' := _, map_add' := _}

source

theorem add_con.lift_mk' {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (H : c ≤ add_con.ker f) (x : M) :

⇑(c.lift f H) (⇑(c.mk') x) = ⇑f x

The diagram describing the universal property for quotients of add_monoids commutes.

source

theorem con.lift_mk' {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (H : c ≤ con.ker f) (x : M) :

⇑(c.lift f H) (⇑(c.mk') x) = ⇑f x

The diagram describing the universal property for quotients of monoids commutes.

source

@[simp]

theorem con.lift_coe {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (H : c ≤ con.ker f) (x : M) :

⇑(c.lift f H) ↑x = ⇑f x

The diagram describing the universal property for quotients of monoids commutes.

source

@[simp]

theorem add_con.lift_coe {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (H : c ≤ add_con.ker f) (x : M) :

⇑(c.lift f H) ↑x = ⇑f x

The diagram describing the universal property for quotients of add_monoids commutes.

source

@[simp]

theorem con.lift_comp_mk' {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (H : c ≤ con.ker f) :

(c.lift f H).comp c.mk' = f

The diagram describing the universal property for quotients of monoids commutes.

source

@[simp]

theorem add_con.lift_comp_mk' {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (H : c ≤ add_con.ker f) :

(c.lift f H).comp c.mk' = f

The diagram describing the universal property for quotients of add_monoids commutes.

source

@[simp]

theorem add_con.lift_apply_mk' {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} (f : c.quotient →+ P) :

c.lift (f.comp c.mk') _ = f

Given a homomorphism f from the quotient of an add_monoid by an additive congruence relation, f equals the homomorphism on the quotient induced by f composed with the natural map from the add_monoid to the quotient.

source

@[simp]

theorem con.lift_apply_mk' {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} (f : c.quotient →* P) :

c.lift (f.comp c.mk') _ = f

Given a homomorphism f from the quotient of a monoid by a congruence relation, f equals the homomorphism on the quotient induced by f composed with the natural map from the monoid to the quotient.

source

theorem add_con.lift_funext {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} (f g : c.quotient →+ P) (h : ∀ (a : M), ⇑f ↑a = ⇑g ↑a) :

f = g

Homomorphisms on the quotient of an add_monoid by an additive congruence relation are equal if they are equal on elements that are coercions from the add_monoid.

source

theorem con.lift_funext {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} (f g : c.quotient →* P) (h : ∀ (a : M), ⇑f ↑a = ⇑g ↑a) :

f = g

Homomorphisms on the quotient of a monoid by a congruence relation are equal if they are equal on elements that are coercions from the monoid.

source

theorem add_con.lift_unique {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (H : c ≤ add_con.ker f) (g : c.quotient →+ P) (Hg : g.comp c.mk' = f) :

g = c.lift f H

The uniqueness part of the universal property for quotients of add_monoids.

source

theorem con.lift_unique {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (H : c ≤ con.ker f) (g : c.quotient →* P) (Hg : g.comp c.mk' = f) :

g = c.lift f H

The uniqueness part of the universal property for quotients of monoids.

source

theorem add_con.lift_range {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (H : c ≤ add_con.ker f) :

add_monoid_hom.mrange (c.lift f H) = add_monoid_hom.mrange f

Given an additive congruence relation c on an add_monoid and a homomorphism f constant on c's equivalence classes, f has the same image as the homomorphism that f induces on the quotient.

source

theorem con.lift_range {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (H : c ≤ con.ker f) :

monoid_hom.mrange (c.lift f H) = monoid_hom.mrange f

Given a congruence relation c on a monoid and a homomorphism f constant on c's equivalence classes, f has the same image as the homomorphism that f induces on the quotient.

source

theorem con.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {c : con M} {f : M →* P} (h : c ≤ con.ker f) (hf : function.surjective ⇑f) :

function.surjective ⇑(c.lift f h)

Surjective monoid homomorphisms constant on a congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

source

theorem add_con.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {c : add_con M} {f : M →+ P} (h : c ≤ add_con.ker f) (hf : function.surjective ⇑f) :

function.surjective ⇑(c.lift f h)

Surjective add_monoid homomorphisms constant on an additive congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

source

theorem con.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (c : con M) (f : M →* P) (H : c ≤ con.ker f) (h : function.injective ⇑(c.lift f H)) :

con.ker f = c

Given a monoid homomorphism f from M to P, the kernel of f is the unique congruence relation on M whose induced map from the quotient of M to P is injective.

source

theorem add_con.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (c : add_con M) (f : M →+ P) (H : c ≤ add_con.ker f) (h : function.injective ⇑(c.lift f H)) :

add_con.ker f = c

Given an add_monoid homomorphism f from M to P, the kernel of f is the unique additive congruence relation on M whose induced map from the quotient of M to P is injective.

source

def add_con.ker_lift {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) :

(add_con.ker f).quotient →+ P

The homomorphism induced on the quotient of an add_monoid by the kernel of an add_monoid homomorphism.

Equations

add_con.ker_lift f = (add_con.ker f).lift f _

source

def con.ker_lift {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) :

(con.ker f).quotient →* P

The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.

Equations

con.ker_lift f = (con.ker f).lift f _

source

@[simp]

theorem con.ker_lift_mk {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {f : M →* P} (x : M) :

⇑(con.ker_lift f) ↑x = ⇑f x

The diagram described by the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, commutes.

source

@[simp]

theorem add_con.ker_lift_mk {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {f : M →+ P} (x : M) :

⇑(add_con.ker_lift f) ↑x = ⇑f x

The diagram described by the universal property for quotients of add_monoids, when the additive congruence relation is the kernel of the homomorphism, commutes.

source

@[simp]

theorem add_con.ker_lift_range_eq {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] {f : M →+ P} :

add_monoid_hom.mrange (add_con.ker_lift f) = add_monoid_hom.mrange f

Given an add_monoid homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

source

@[simp]

theorem con.ker_lift_range_eq {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] {f : M →* P} :

monoid_hom.mrange (con.ker_lift f) = monoid_hom.mrange f

Given a monoid homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

source

theorem con.ker_lift_injective {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) :

function.injective ⇑(con.ker_lift f)

A monoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

source

theorem add_con.ker_lift_injective {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) :

function.injective ⇑(add_con.ker_lift f)

An add_monoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

source

def con.map {M : Type u_1} [mul_one_class M] (c d : con M) (h : c ≤ d) :

c.quotient →* d.quotient

Given congruence relations c, d on a monoid such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

Equations

c.map d h = c.lift d.mk' _

source

def add_con.map {M : Type u_1} [add_zero_class M] (c d : add_con M) (h : c ≤ d) :

c.quotient →+ d.quotient

Given additive congruence relations c, d on an add_monoid such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

Equations

c.map d h = c.lift d.mk' _

source

theorem add_con.map_apply {M : Type u_1} [add_zero_class M] {c d : add_con M} (h : c ≤ d) (x : c.quotient) :

⇑(c.map d h) x = ⇑(c.lift d.mk' _) x

Given additive congruence relations c, d on an add_monoid such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

source

theorem con.map_apply {M : Type u_1} [mul_one_class M] {c d : con M} (h : c ≤ d) (x : c.quotient) :

⇑(c.map d h) x = ⇑(c.lift d.mk' _) x

Given congruence relations c, d on a monoid such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

source

noncomputable def add_con.quotient_ker_equiv_range {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) :

(add_con.ker f).quotient ≃+ ↥(add_monoid_hom.mrange f)

The first isomorphism theorem for add_monoids.

Equations

source

noncomputable def con.quotient_ker_equiv_range {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) :

(con.ker f).quotient ≃* ↥(monoid_hom.mrange f)

The first isomorphism theorem for monoids.

Equations

source

def add_con.quotient_ker_equiv_of_right_inverse {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) (g : P → M) (hf : function.right_inverse g ⇑f) :

(add_con.ker f).quotient ≃+ P

The first isomorphism theorem for add_monoids in the case of a homomorphism with right inverse.

Equations

add_con.quotient_ker_equiv_of_right_inverse f g hf = {to_fun := ⇑(add_con.ker_lift f), inv_fun := coe ∘ g, left_inv := _, right_inv := hf, map_add' := _}

source

@[simp]

theorem con.quotient_ker_equiv_of_right_inverse_apply {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) (g : P → M) (hf : function.right_inverse g ⇑f) (ᾰ : (con.ker f).quotient) :

⇑(con.quotient_ker_equiv_of_right_inverse f g hf) ᾰ = ⇑(con.ker_lift f) ᾰ

source

@[simp]

theorem add_con.quotient_ker_equiv_of_right_inverse_symm_apply {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) (g : P → M) (hf : function.right_inverse g ⇑f) (ᾰ : P) :

⇑((add_con.quotient_ker_equiv_of_right_inverse f g hf).symm) ᾰ = (coe ∘ g) ᾰ

source

@[simp]

theorem con.quotient_ker_equiv_of_right_inverse_symm_apply {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) (g : P → M) (hf : function.right_inverse g ⇑f) (ᾰ : P) :

⇑((con.quotient_ker_equiv_of_right_inverse f g hf).symm) ᾰ = (coe ∘ g) ᾰ

source

@[simp]

theorem add_con.quotient_ker_equiv_of_right_inverse_apply {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) (g : P → M) (hf : function.right_inverse g ⇑f) (ᾰ : (add_con.ker f).quotient) :

⇑(add_con.quotient_ker_equiv_of_right_inverse f g hf) ᾰ = ⇑(add_con.ker_lift f) ᾰ

source

def con.quotient_ker_equiv_of_right_inverse {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) (g : P → M) (hf : function.right_inverse g ⇑f) :

(con.ker f).quotient ≃* P

The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.

Equations

con.quotient_ker_equiv_of_right_inverse f g hf = {to_fun := ⇑(con.ker_lift f), inv_fun := coe ∘ g, left_inv := _, right_inv := hf, map_mul' := _}

source

noncomputable def add_con.quotient_ker_equiv_of_surjective {M : Type u_1} {P : Type u_3} [add_zero_class M] [add_zero_class P] (f : M →+ P) (hf : function.surjective ⇑f) :

(add_con.ker f).quotient ≃+ P

The first isomorphism theorem for add_monoids in the case of a surjective homomorphism.

For a computable version, see add_con.quotient_ker_equiv_of_right_inverse.

Equations

add_con.quotient_ker_equiv_of_surjective f hf = add_con.quotient_ker_equiv_of_right_inverse f (Exists.some _) _

source

noncomputable def con.quotient_ker_equiv_of_surjective {M : Type u_1} {P : Type u_3} [mul_one_class M] [mul_one_class P] (f : M →* P) (hf : function.surjective ⇑f) :

(con.ker f).quotient ≃* P

The first isomorphism theorem for monoids in the case of a surjective homomorphism.

For a computable version, see con.quotient_ker_equiv_of_right_inverse.

Equations

con.quotient_ker_equiv_of_surjective f hf = con.quotient_ker_equiv_of_right_inverse f (Exists.some _) _

source

noncomputable def add_con.comap_quotient_equiv {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (c : add_con M) (f : N →+ M) :

(add_con.comap ⇑f _ c).quotient ≃+ ↥(add_monoid_hom.mrange (c.mk'.comp f))

The second isomorphism theorem for add_monoids.

Equations

c.comap_quotient_equiv f = (add_con.congr add_con.comap_eq).trans (add_con.quotient_ker_equiv_range (c.mk'.comp f))

source

noncomputable def con.comap_quotient_equiv {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (c : con M) (f : N →* M) :

(con.comap ⇑f _ c).quotient ≃* ↥(monoid_hom.mrange (c.mk'.comp f))

The second isomorphism theorem for monoids.

Equations

c.comap_quotient_equiv f = (con.congr con.comap_eq).trans (con.quotient_ker_equiv_range (c.mk'.comp f))

source

def con.quotient_quotient_equiv_quotient {M : Type u_1} [mul_one_class M] (c d : con M) (h : c ≤ d) :

(con.ker (c.map d h)).quotient ≃* d.quotient

The third isomorphism theorem for monoids.

Equations

c.quotient_quotient_equiv_quotient d h = {to_fun := (c.to_setoid.quotient_quotient_equiv_quotient d.to_setoid h).to_fun, inv_fun := (c.to_setoid.quotient_quotient_equiv_quotient d.to_setoid h).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_con.quotient_quotient_equiv_quotient {M : Type u_1} [add_zero_class M] (c d : add_con M) (h : c ≤ d) :

(add_con.ker (c.map d h)).quotient ≃+ d.quotient

The third isomorphism theorem for add_monoids.

Equations

c.quotient_quotient_equiv_quotient d h = {to_fun := (c.to_setoid.quotient_quotient_equiv_quotient d.to_setoid h).to_fun, inv_fun := (c.to_setoid.quotient_quotient_equiv_quotient d.to_setoid h).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[protected]

theorem add_con.nsmul {M : Type u_1} [add_monoid M] (c : add_con M) (n : ℕ) {w x : M} :

⇑c w x → ⇑c (n • w) (n • x)

Additive congruence relations preserve natural scaling.

source

@[protected]

theorem con.pow {M : Type u_1} [monoid M] (c : con M) (n : ℕ) {w x : M} :

⇑c w x → ⇑c (w ^ n) (x ^ n)

Multiplicative congruence relations preserve natural powers.

source

@[protected, instance]

def con.quotient.has_one {M : Type u_1} [mul_one_class M] (c : con M) :

has_one c.quotient

Equations

con.quotient.has_one c = {one := ↑1}

source

@[protected, instance]

def add_con.quotient.has_zero {M : Type u_1} [add_zero_class M] (c : add_con M) :

has_zero c.quotient

Equations

add_con.quotient.has_zero c = {zero := ↑0}

source

theorem add_con.vadd {α : Type u_1} {M : Type u_2} [add_zero_class M] [has_vadd α M] [vadd_assoc_class α M M] (c : add_con M) (a : α) {w x : M} (h : ⇑c w x) :

⇑c (a +ᵥ w) (a +ᵥ x)

source

theorem con.smul {α : Type u_1} {M : Type u_2} [mul_one_class M] [has_smul α M] [is_scalar_tower α M M] (c : con M) (a : α) {w x : M} (h : ⇑c w x) :

⇑c (a • w) (a • x)

source

@[protected, instance]

def add_con.quotient.has_nsmul {M : Type u_1} [add_monoid M] (c : add_con M) :

has_smul ℕ c.quotient

Equations

add_con.quotient.has_nsmul c = {smul := λ (n : ℕ), quotient.map' (has_smul.smul n) _}

source

@[protected, instance]

def con.nat.has_pow {M : Type u_1} [monoid M] (c : con M) :

has_pow c.quotient ℕ

Equations

con.nat.has_pow c = {pow := λ (x : c.quotient) (n : ℕ), quotient.map' (λ (x : M), x ^ n) _ x}

source

@[protected, instance]

def add_con.add_semigroup {M : Type u_1} [add_semigroup M] (c : add_con M) :

add_semigroup c.quotient

The quotient of an add_semigroup by an additive congruence relation is an add_semigroup.

Equations

c.add_semigroup = function.surjective.add_semigroup quotient.mk' _ _

source

@[protected, instance]

def con.semigroup {M : Type u_1} [semigroup M] (c : con M) :

semigroup c.quotient

The quotient of a semigroup by a congruence relation is a semigroup.

Equations

c.semigroup = function.surjective.semigroup quotient.mk' _ _

source

@[protected, instance]

def add_con.add_comm_semigroup {M : Type u_1} [add_comm_semigroup M] (c : add_con M) :

add_comm_semigroup c.quotient

The quotient of an add_comm_semigroup by an additive congruence relation is an add_semigroup.

Equations

c.add_comm_semigroup = function.surjective.add_comm_semigroup quotient.mk' _ _

source

@[protected, instance]

def con.comm_semigroup {M : Type u_1} [comm_semigroup M] (c : con M) :

comm_semigroup c.quotient

The quotient of a commutative semigroup by a congruence relation is a semigroup.

Equations

c.comm_semigroup = function.surjective.comm_semigroup quotient.mk' _ _

source

@[protected, instance]

def con.monoid {M : Type u_1} [monoid M] (c : con M) :

monoid c.quotient

The quotient of a monoid by a congruence relation is a monoid.

Equations

c.monoid = function.surjective.monoid quotient.mk' _ _ _ _

source

@[protected, instance]

def add_con.add_monoid {M : Type u_1} [add_monoid M] (c : add_con M) :

add_monoid c.quotient

The quotient of an add_monoid by an additive congruence relation is an add_monoid.

Equations

c.add_monoid = function.surjective.add_monoid quotient.mk' _ _ _ _

source

@[protected, instance]

def add_con.add_comm_monoid {M : Type u_1} [add_comm_monoid M] (c : add_con M) :

add_comm_monoid c.quotient

The quotient of an add_comm_monoid by an additive congruence relation is an add_comm_monoid.

Equations

c.add_comm_monoid = function.surjective.add_comm_monoid quotient.mk' _ _ _ _

source

@[protected, instance]

def con.comm_monoid {M : Type u_1} [comm_monoid M] (c : con M) :

comm_monoid c.quotient

The quotient of a comm_monoid by a congruence relation is a comm_monoid.

Equations

c.comm_monoid = function.surjective.comm_monoid quotient.mk' _ _ _ _

source

@[protected]

theorem add_con.neg {M : Type u_1} [add_group M] (c : add_con M) {w x : M} :

⇑c w x → ⇑c (-w) (-x)

Additive congruence relations preserve negation.

source

@[protected]

theorem con.inv {M : Type u_1} [group M] (c : con M) {w x : M} :

⇑c w x → ⇑c w⁻¹ x⁻¹

Multiplicative congruence relations preserve inversion.

source

@[protected]

theorem add_con.sub {M : Type u_1} [add_group M] (c : add_con M) {w x y z : M} :

⇑c w x → ⇑c y z → ⇑c (w - y) (x - z)

Additive congruence relations preserve subtraction.

source

@[protected]

theorem con.div {M : Type u_1} [group M] (c : con M) {w x y z : M} :

⇑c w x → ⇑c y z → ⇑c (w / y) (x / z)

Multiplicative congruence relations preserve division.

source

@[protected]

theorem con.zpow {M : Type u_1} [group M] (c : con M) (n : ℤ) {w x : M} :

⇑c w x → ⇑c (w ^ n) (x ^ n)

Multiplicative congruence relations preserve integer powers.

source

@[protected]

theorem add_con.zsmul {M : Type u_1} [add_group M] (c : add_con M) (n : ℤ) {w x : M} :

⇑c w x → ⇑c (n • w) (n • x)

Additive congruence relations preserve integer scaling.

source

@[protected, instance]

def add_con.has_neg {M : Type u_1} [add_group M] (c : add_con M) :

has_neg c.quotient

The negation induced on the quotient by an additive congruence relation on a type with an negation.

Equations

c.has_neg = {neg := quotient.map' has_neg.neg _}

source

@[protected, instance]

def con.has_inv {M : Type u_1} [group M] (c : con M) :

has_inv c.quotient

The inversion induced on the quotient by a congruence relation on a type with a inversion.

Equations

c.has_inv = {inv := quotient.map' has_inv.inv _}

source

@[protected, instance]

def add_con.has_sub {M : Type u_1} [add_group M] (c : add_con M) :

has_sub c.quotient

The subtraction induced on the quotient by an additive congruence relation on a type with a subtraction.

Equations

c.has_sub = {sub := quotient.map₂' has_sub.sub _}

source

@[protected, instance]

def con.has_div {M : Type u_1} [group M] (c : con M) :

has_div c.quotient

The division induced on the quotient by a congruence relation on a type with a division.

Equations

c.has_div = {div := quotient.map₂' has_div.div _}

source

@[protected, instance]

def add_con.quotient.has_zsmul {M : Type u_1} [add_group M] (c : add_con M) :

has_smul ℤ c.quotient

The integer scaling induced on the quotient by a congruence relation on a type with a subtraction.

Equations

add_con.quotient.has_zsmul c = {smul := λ (z : ℤ), quotient.map' (has_smul.smul z) _}

source

@[protected, instance]

def con.has_zpow {M : Type u_1} [group M] (c : con M) :

has_pow c.quotient ℤ

The integer power induced on the quotient by a congruence relation on a type with a division.

Equations

c.has_zpow = {pow := λ (x : c.quotient) (z : ℤ), quotient.map' (λ (x : M), x ^ z) _ x}

source

@[protected, instance]

def add_con.add_group {M : Type u_1} [add_group M] (c : add_con M) :

add_group c.quotient

The quotient of an add_group by an additive congruence relation is an add_group.

Equations

c.add_group = function.surjective.add_group quotient.mk' _ _ _ _ _ _ _

source

@[protected, instance]

def con.group {M : Type u_1} [group M] (c : con M) :

group c.quotient

The quotient of a group by a congruence relation is a group.

Equations

c.group = function.surjective.group quotient.mk' _ _ _ _ _ _ _

source

def con.lift_on_units {M : Type u_1} {α : Type u_4} [monoid M] {c : con M} (u : c.quotient ˣ) (f : Π (x y : M), ⇑c (x * y) 1 → ⇑c (y * x) 1 → α) (Hf : ∀ (x y : M) (hxy : ⇑c (x * y) 1) (hyx : ⇑c (y * x) 1) (x' y' : M) (hxy' : ⇑c (x' * y') 1) (hyx' : ⇑c (y' * x') 1), ⇑c x x' → ⇑c y y' → f x y hxy hyx = f x' y' hxy' hyx') :

α

In order to define a function (con.quotient c)ˣ → α on the units of con.quotient c, where c : con M is a multiplicative congruence on a monoid, it suffices to define a function f that takes elements x y : M with proofs of c (x * y) 1 and c (y * x) 1, and returns an element of α provided that f x y _ _ = f x' y' _ _ whenever c x x' and c y y'.

Equations

con.lift_on_units u f Hf = con.hrec_on₂ ↑u ↑u⁻¹ (λ (x y : M) (hxy : ↑x * ↑y = 1) (hyx : ↑y * ↑x = 1), f x y _ _) _ _ _

source

def add_con.lift_on_add_units {M : Type u_1} {α : Type u_4} [add_monoid M] {c : add_con M} (u : add_units c.quotient) (f : Π (x y : M), ⇑c (x + y) 0 → ⇑c (y + x) 0 → α) (Hf : ∀ (x y : M) (hxy : ⇑c (x + y) 0) (hyx : ⇑c (y + x) 0) (x' y' : M) (hxy' : ⇑c (x' + y') 0) (hyx' : ⇑c (y' + x') 0), ⇑c x x' → ⇑c y y' → f x y hxy hyx = f x' y' hxy' hyx') :

α

In order to define a function (con.quotient c)ˣ → α on the units of con.quotient c, where c : con M is a multiplicative congruence on a monoid, it suffices to define a function f that takes elements x y : M with proofs of c (x * y) 1 and c (y * x) 1, and returns an element of α provided that f x y _ _ = f x' y' _ _ whenever c x x' and c y y'.

Equations

add_con.lift_on_add_units u f Hf = add_con.hrec_on₂ ↑u (↑-u) (λ (x y : M) (hxy : ↑x + ↑y = 0) (hyx : ↑y + ↑x = 0), f x y _ _) _ _ _

source

@[simp]

theorem con.lift_on_units_mk {M : Type u_1} {α : Type u_4} [monoid M] {c : con M} (f : Π (x y : M), ⇑c (x * y) 1 → ⇑c (y * x) 1 → α) (Hf : ∀ (x y : M) (hxy : ⇑c (x * y) 1) (hyx : ⇑c (y * x) 1) (x' y' : M) (hxy' : ⇑c (x' * y') 1) (hyx' : ⇑c (y' * x') 1), ⇑c x x' → ⇑c y y' → f x y hxy hyx = f x' y' hxy' hyx') (x y : M) (hxy : ↑x * ↑y = 1) (hyx : ↑y * ↑x = 1) :

con.lift_on_units {val := ↑x, inv := ↑y, val_inv := hxy, inv_val := hyx} f Hf = f x y _ _

source

@[simp]

theorem add_con.lift_on_add_units_mk {M : Type u_1} {α : Type u_4} [add_monoid M] {c : add_con M} (f : Π (x y : M), ⇑c (x + y) 0 → ⇑c (y + x) 0 → α) (Hf : ∀ (x y : M) (hxy : ⇑c (x + y) 0) (hyx : ⇑c (y + x) 0) (x' y' : M) (hxy' : ⇑c (x' + y') 0) (hyx' : ⇑c (y' + x') 0), ⇑c x x' → ⇑c y y' → f x y hxy hyx = f x' y' hxy' hyx') (x y : M) (hxy : ↑x + ↑y = 0) (hyx : ↑y + ↑x = 0) :

add_con.lift_on_add_units {val := ↑x, neg := ↑y, val_neg := hxy, neg_val := hyx} f Hf = f x y _ _

source

theorem add_con.induction_on_add_units {M : Type u_1} [add_monoid M] {c : add_con M} {p : add_units c.quotient → Prop} (u : add_units c.quotient) (H : ∀ (x y : M) (hxy : ⇑c (x + y) 0) (hyx : ⇑c (y + x) 0), p {val := ↑x, neg := ↑y, val_neg := _, neg_val := _}) :

p u

source

theorem con.induction_on_units {M : Type u_1} [monoid M] {c : con M} {p : c.quotient ˣ → Prop} (u : c.quotient ˣ) (H : ∀ (x y : M) (hxy : ⇑c (x * y) 1) (hyx : ⇑c (y * x) 1), p {val := ↑x, inv := ↑y, val_inv := _, inv_val := _}) :

p u

source

@[protected, instance]

def con.has_smul {α : Type u_1} {M : Type u_2} [mul_one_class M] [has_smul α M] [is_scalar_tower α M M] (c : con M) :

has_smul α c.quotient

Equations

c.has_smul = {smul := λ (a : α), quotient.map' (has_smul.smul a) _}

source

@[protected, instance]

def add_con.has_vadd {α : Type u_1} {M : Type u_2} [add_zero_class M] [has_vadd α M] [vadd_assoc_class α M M] (c : add_con M) :

has_vadd α c.quotient

Equations

c.has_vadd = {vadd := λ (a : α), quotient.map' (has_vadd.vadd a) _}

source

theorem con.coe_smul {α : Type u_1} {M : Type u_2} [mul_one_class M] [has_smul α M] [is_scalar_tower α M M] (c : con M) (a : α) (x : M) :

↑(a • x) = a • ↑x

source

theorem add_con.coe_vadd {α : Type u_1} {M : Type u_2} [add_zero_class M] [has_vadd α M] [vadd_assoc_class α M M] (c : add_con M) (a : α) (x : M) :

↑(a +ᵥ x) = a +ᵥ ↑x

source

@[protected, instance]

def con.mul_action {α : Type u_1} {M : Type u_2} [monoid α] [mul_one_class M] [mul_action α M] [is_scalar_tower α M M] (c : con M) :

mul_action α c.quotient

Equations

c.mul_action = {to_has_smul := {smul := has_smul.smul c.has_smul}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def add_con.add_action {α : Type u_1} {M : Type u_2} [add_monoid α] [add_zero_class M] [add_action α M] [vadd_assoc_class α M M] (c : add_con M) :

add_action α c.quotient

Equations

c.add_action = {to_has_vadd := {vadd := has_vadd.vadd c.has_vadd}, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def con.mul_distrib_mul_action {α : Type u_1} {M : Type u_2} [monoid α] [monoid M] [mul_distrib_mul_action α M] [is_scalar_tower α M M] (c : con M) :

mul_distrib_mul_action α c.quotient

Equations

c.mul_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := has_smul.smul c.has_smul}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}

mathlib3 documentation

Congruence relations #

Implementation notes #

Tags #