Documentation

Mathlib.GroupTheory.Congruence

Congruence relations #

This file defines congruence relations: equivalence relations that preserve a binary operation, which in this case is multiplication or addition. The principal definition is a structure extending a Setoid (an equivalence relation), and the inductive definition of the smallest congruence relation containing a binary relation is also given (see ConGen).

The file also proves basic properties of the quotient of a type by a congruence relation, and the complete lattice of congruence relations on a type. We then establish an order-preserving bijection between the set of congruence relations containing a congruence relation c and the set of congruence relations on the quotient by c.

The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid. There are results about the universal property of quotients of monoids, and the isomorphism theorems for monoids.

Implementation notes #

The inductive definition of a congruence relation could be a nested inductive type, defined using the equivalence closure of a binary relation EqvGen, but the recursor generated does not work. A nested inductive definition could conceivably shorten proofs, because they would allow invocation of the corresponding lemmas about EqvGen.

The lemmas refl, symm and trans are not tagged with @[refl], @[symm], and @[trans] respectively as these tags do not work on a structure coerced to a binary relation.

There is a coercion from elements of a type to the element's equivalence class under a congruence relation.

A congruence relation on a monoid M can be thought of as a submonoid of M × M× M for which membership is an equivalence relation, but whilst this fact is established in the file, it is not used, since this perspective adds more layers of definitional unfolding.

Tags #

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid, isomorphism theorems

structure AddCon (M : Type u_1) [inst : Add M] extends Setoid :

Type u_1

Additive congruence relations are closed under addition
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

structure Con (M : Type u_1) [inst : Mul M] extends Setoid :

Type u_1

Congruence relations are closed under multiplication
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

inductive AddConGen.Rel {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

M → M → Prop

of: ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} (x y : M), r x y → AddConGen.Rel r x y
refl: ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} (x : M), AddConGen.Rel r x x
symm: ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {x y : M}, AddConGen.Rel r x y → AddConGen.Rel r y x
trans: ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {x y z : M}, AddConGen.Rel r x y → AddConGen.Rel r y z → AddConGen.Rel r x z
add: ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {w x y z : M}, AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z)

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

Instances For

inductive ConGen.Rel {M : Type u_1} [inst : Mul M] (r : M → M → Prop) :

M → M → Prop

of: ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} (x y : M), r x y → ConGen.Rel r x y
refl: ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} (x : M), ConGen.Rel r x x
symm: ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {x y : M}, ConGen.Rel r x y → ConGen.Rel r y x
trans: ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → ConGen.Rel r x z
mul: ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → ConGen.Rel r (w * y) (x * z)

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

Instances For

def addConGen.proof_1 {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

Equivalence (AddConGen.Rel r)

Equations

(_ : Equivalence (AddConGen.Rel r)) = (_ : Equivalence (AddConGen.Rel r))

def addConGen {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

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

Equations

One or more equations did not get rendered due to their size.

def addConGen.proof_2 {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

∀ {w x y z : M}, AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z)

Equations

(_ : AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z)) = (_ : AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z))

def conGen {M : Type u_1} [inst : Mul M] (r : M → M → Prop) :

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

Equations

conGen r = { toSetoid := { r := ConGen.Rel r, iseqv := (_ : Equivalence (ConGen.Rel r)) }, mul' := (_ : ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → ConGen.Rel r (w * y) (x * z)) }

instance AddCon.instInhabitedCon {M : Type u_1} [inst : Add M] :

Inhabited (AddCon M)

Equations

AddCon.instInhabitedCon = { default := addConGen EmptyRelation }

instance Con.instInhabitedCon {M : Type u_1} [inst : Mul M] :

Inhabited (Con M)

Equations

Con.instInhabitedCon = { default := conGen EmptyRelation }

def AddCon.instFunLikeConForAllProp.proof_1 {M : Type u_1} [inst : Add M] (x : AddCon M) (y : AddCon M) (h : (fun c x y => Setoid.r x y) x = (fun c x y => Setoid.r x y) y) :

x = y

Equations

(_ : x = y) = (_ : x = y)

instance AddCon.instFunLikeConForAllProp {M : Type u_1} [inst : Add M] :

FunLike (AddCon M) M fun x => M → Prop

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

Equations

AddCon.instFunLikeConForAllProp = { coe := fun c x y => Setoid.r x y, coe_injective' := (_ : ∀ (x y : AddCon M), (fun c x y => Setoid.r x y) x = (fun c x y => Setoid.r x y) y → x = y) }

instance Con.instFunLikeConForAllProp {M : Type u_1} [inst : Mul M] :

FunLike (Con M) M fun x => M → Prop

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

Equations

Con.instFunLikeConForAllProp = { coe := fun c x y => Setoid.r x y, coe_injective' := (_ : ∀ (x y : Con M), (fun c x y => Setoid.r x y) x = (fun c x y => Setoid.r x y) y → x = y) }

@[simp]

theorem AddCon.rel_eq_coe {M : Type u_1} [inst : Add M] (c : AddCon M) :

Setoid.r = ↑c

@[simp]

theorem Con.rel_eq_coe {M : Type u_1} [inst : Mul M] (c : Con M) :

Setoid.r = ↑c

theorem AddCon.refl {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M) :

↑c x x

Additive congruence relations are reflexive.

theorem Con.refl {M : Type u_1} [inst : Mul M] (c : Con M) (x : M) :

↑c x x

Congruence relations are reflexive.

theorem AddCon.symm {M : Type u_1} [inst : Add M] (c : AddCon M) {x : M} {y : M} :

↑c x y → ↑c y x

Additive congruence relations are symmetric.

theorem Con.symm {M : Type u_1} [inst : Mul M] (c : Con M) {x : M} {y : M} :

↑c x y → ↑c y x

Congruence relations are symmetric.

theorem AddCon.trans {M : Type u_1} [inst : Add M] (c : AddCon M) {x : M} {y : M} {z : M} :

↑c x y → ↑c y z → ↑c x z

Additive congruence relations are transitive.

theorem Con.trans {M : Type u_1} [inst : Mul M] (c : Con M) {x : M} {y : M} {z : M} :

↑c x y → ↑c y z → ↑c x z

Congruence relations are transitive.

theorem AddCon.add {M : Type u_1} [inst : Add M] (c : AddCon M) {w : M} {x : M} {y : M} {z : M} :

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

Additive congruence relations preserve addition.

theorem Con.mul {M : Type u_1} [inst : Mul M] (c : Con M) {w : M} {x : M} {y : M} {z : M} :

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

Multiplicative congruence relations preserve multiplication.

@[simp]

theorem AddCon.rel_mk {M : Type u_1} [inst : 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 : M} {b : M} :

↑{ toSetoid := s, add' := h } a b ↔ Setoid.r a b

@[simp]

theorem Con.rel_mk {M : Type u_1} [inst : 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 : M} {b : M} :

↑{ toSetoid := s, mul' := h } a b ↔ Setoid.r a b

instance AddCon.instMembershipSumCon {M : Type u_1} [inst : Add M] :

Membership (M × M) (AddCon M)

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

Equations

AddCon.instMembershipSumCon = { mem := fun x c => ↑c x.fst x.snd }

instance Con.instMembershipProdCon {M : Type u_1} [inst : Mul M] :

Membership (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∈ M × M× M iff x is related to y by c.

Equations

Con.instMembershipProdCon = { mem := fun x c => ↑c x.fst x.snd }

theorem AddCon.ext' {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (H : Setoid.r = Setoid.r) :

c = d

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

theorem Con.ext' {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} (H : Setoid.r = Setoid.r) :

c = d

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

theorem AddCon.ext {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (H : ∀ (x y : M), ↑c x y ↔ ↑d x y) :

c = d

Extensionality rule for additive congruence relations.

theorem Con.ext {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} (H : ∀ (x y : M), ↑c x y ↔ ↑d x y) :

c = d

Extensionality rule for congruence relations.

theorem AddCon.toSetoid_inj {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (H : c.toSetoid = d.toSetoid) :

c = d

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

theorem Con.toSetoid_inj {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} (H : c.toSetoid = d.toSetoid) :

c = d

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

theorem AddCon.ext_iff {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} :

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

Iff version of extensionality rule for additive congruence relations.

theorem Con.ext_iff {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} :

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

Iff version of extensionality rule for congruence relations.

theorem AddCon.ext'_iff {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} :

Setoid.r = Setoid.r ↔ c = d

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

theorem Con.ext'_iff {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} :

Setoid.r = Setoid.r ↔ c = d

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

def AddCon.addKer.proof_1 {M : Type u_1} {P : Type u_2} [inst : Add M] [inst : Add P] (f : M → P) (h : ∀ (x y : M), f (x + y) = f x + f y) :

∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)

Equations

(_ : Setoid.r (w + y) (x + z)) = (_ : Setoid.r (w + y) (x + z))

def AddCon.addKer {M : Type u_1} {P : Type u_2} [inst : Add M] [inst : Add P] (f : M → P) (h : ∀ (x y : M), f (x + y) = f x + f y) :

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

Equations

AddCon.addKer f h = { toSetoid := Setoid.ker f, add' := (_ : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)) }

def Con.mulKer {M : Type u_1} {P : Type u_2} [inst : Mul M] [inst : Mul P] (f : M → P) (h : ∀ (x y : M), f (x * y) = f x * f y) :

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

Equations

Con.mulKer f h = { toSetoid := Setoid.ker f, mul' := (_ : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)) }

def AddCon.prod {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (c : AddCon M) (d : AddCon N) :

AddCon (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∈ M × N× N are related by c.prod d iff x₁ is related to y₁ by c and x₂ is related to y₂ by d.

Equations

One or more equations did not get rendered due to their size.

def AddCon.prod.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (c : AddCon M) (d : AddCon N) :

∀ {w x y z : M × N}, Setoid.r w x → Setoid.r y z → Setoid.Rel c.toSetoid (w + y).fst (x + z).fst ∧ Setoid.Rel d.toSetoid (w + y).snd (x + z).snd

Equations

One or more equations did not get rendered due to their size.

def AddCon.prod.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (c : AddCon M) (d : AddCon N) :

Equivalence Setoid.r

Equations

(_ : Equivalence Setoid.r) = (_ : Equivalence Setoid.r)

def Con.prod {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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∈ M × N× N are related by c.prod d iff x₁ is related to y₁ by c and x₂ is related to y₂ by d.

Equations

One or more equations did not get rendered due to their size.

def AddCon.pi.proof_1 {ι : Type u_1} {f : ι → Type u_2} [inst : (i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) :

Equivalence Setoid.r

Equations

(_ : Equivalence Setoid.r) = (_ : Equivalence Setoid.r)

def AddCon.pi.proof_2 {ι : Type u_1} {f : ι → Type u_2} [inst : (i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) :

{w x y z : (i : ι) → f i} → Setoid.r w x → Setoid.r y z → (i : ι) → ↑(C i) (w i + y i) (x i + z i)

Equations

(_ : ↑(C i) (w i + y i) (x i + z i)) = (_ : ↑(C i) (w i + y i) (x i + z i))

def AddCon.pi {ι : Type u_1} {f : ι → Type u_2} [inst : (i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) :

AddCon ((i : ι) → f i)

The product of an indexed collection of additive congruence relations.

Equations

AddCon.pi C = let src := piSetoid; { toSetoid := { r := Setoid.r, iseqv := (_ : Equivalence Setoid.r) }, add' := @AddCon.pi.proof_2 ι f inst C }

def Con.pi {ι : Type u_1} {f : ι → Type u_2} [inst : (i : ι) → 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 = let src := piSetoid; { toSetoid := { r := Setoid.r, iseqv := (_ : Equivalence Setoid.r) }, mul' := @Con.pi.proof_2 ι f inst C }

def AddCon.Quotient {M : Type u_1} [inst : Add M] (c : AddCon M) :

Type u_1

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

Equations

AddCon.Quotient c = Quotient c.toSetoid

def Con.Quotient {M : Type u_1} [inst : Mul M] (c : Con M) :

Type u_1

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

Equations

Con.Quotient c = Quotient c.toSetoid

def AddCon.toQuotient {M : Type u_1} [inst : Add M] {c : AddCon M} :

M → AddCon.Quotient c

The morphism into the quotient by an additive congruence relation

Equations

AddCon.toQuotient = Quotient.mk''

def Con.toQuotient {M : Type u_1} [inst : Mul M] {c : Con M} :

M → Con.Quotient c

The morphism into the quotient by a congruence relation

Equations

Con.toQuotient = Quotient.mk''

instance AddCon.instCoeTCQuotient {M : Type u_1} [inst : Add M] (c : AddCon M) :

CoeTC M (AddCon.Quotient c)

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

Equations

AddCon.instCoeTCQuotient c = { coe := AddCon.toQuotient }

instance Con.instCoeTCQuotient {M : Type u_1} [inst : Mul M] (c : Con M) :

CoeTC M (Con.Quotient c)

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

See Note [use has_coe_t].

Equations

Con.instCoeTCQuotient c = { coe := Con.toQuotient }

instance AddCon.instDecidableEqQuotient {M : Type u_1} [inst : Add M] (c : AddCon M) [inst : (a b : M) → Decidable (↑c a b)] :

DecidableEq (AddCon.Quotient c)

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

Equations

AddCon.instDecidableEqQuotient c = inferInstanceAs (DecidableEq (Quotient c.toSetoid))

instance Con.instDecidableEqQuotient {M : Type u_1} [inst : Mul M] (c : Con M) [inst : (a b : M) → Decidable (↑c a b)] :

DecidableEq (Con.Quotient c)

The quotient by a decidable congruence relation has decidable equality.

Equations

Con.instDecidableEqQuotient c = inferInstanceAs (DecidableEq (Quotient c.toSetoid))

@[simp]

theorem AddCon.quot_mk_eq_coe {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M) :

Quot.mk (↑c) x = ↑x

@[simp]

theorem Con.quot_mk_eq_coe {M : Type u_1} [inst : Mul M] (c : Con M) (x : M) :

Quot.mk (↑c) x = ↑x

def AddCon.liftOn {M : Type u_1} [inst : Add M] {β : Sort u_2} {c : AddCon M} (q : AddCon.Quotient c) (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

AddCon.liftOn q f h = Quotient.liftOn' q f h

def Con.liftOn {M : Type u_1} [inst : Mul M] {β : Sort u_2} {c : Con M} (q : Con.Quotient c) (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.liftOn q f h = Quotient.liftOn' q f h

def AddCon.liftOn₂ {M : Type u_1} [inst : Add M] {β : Sort u_2} {c : AddCon M} (q : AddCon.Quotient c) (r : AddCon.Quotient c) (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

AddCon.liftOn₂ q r f h = Quotient.liftOn₂' q r f h

def Con.liftOn₂ {M : Type u_1} [inst : Mul M] {β : Sort u_2} {c : Con M} (q : Con.Quotient c) (r : Con.Quotient c) (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.liftOn₂ q r f h = Quotient.liftOn₂' q r f h

def AddCon.hrecOn₂ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {cM : AddCon M} {cN : AddCon N} {φ : AddCon.Quotient cM → AddCon.Quotient cN → Sort u_3} (a : AddCon.Quotient cM) (b : AddCon.Quotient cN) (f : (x : M) → (y : N) → φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ↑cM x x' → ↑cN y y' → HEq (f x y) (f x' y')) :

φ a b

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

Equations

AddCon.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h

def Con.hrecOn₂ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {cM : Con M} {cN : Con N} {φ : Con.Quotient cM → Con.Quotient cN → Sort u_3} (a : Con.Quotient cM) (b : Con.Quotient cN) (f : (x : M) → (y : N) → φ ↑x ↑y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), ↑cM x x' → ↑cN y y' → HEq (f x y) (f x' y')) :

φ a b

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

Equations

Con.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h

@[simp]

theorem AddCon.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {cM : AddCon M} {cN : AddCon N} {φ : AddCon.Quotient cM → AddCon.Quotient cN → 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' → HEq (f x y) (f x' y')) :

AddCon.hrecOn₂ (↑a) (↑b) f h = f a b

@[simp]

theorem Con.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {cM : Con M} {cN : Con N} {φ : Con.Quotient cM → Con.Quotient cN → 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' → HEq (f x y) (f x' y')) :

Con.hrecOn₂ (↑a) (↑b) f h = f a b

theorem AddCon.induction_on {M : Type u_1} [inst : Add M] {c : AddCon M} {C : AddCon.Quotient c → Prop} (q : AddCon.Quotient c) (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.

theorem Con.induction_on {M : Type u_1} [inst : Mul M] {c : Con M} {C : Con.Quotient c → Prop} (q : Con.Quotient c) (H : (x : M) → C ↑x) :

C q

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

theorem AddCon.induction_on₂ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {c : AddCon M} {d : AddCon N} {C : AddCon.Quotient c → AddCon.Quotient d → Prop} (p : AddCon.Quotient c) (q : AddCon.Quotient d) (H : (x : M) → (y : N) → C ↑x ↑y) :

C p q

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

theorem Con.induction_on₂ {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {c : Con M} {d : Con N} {C : Con.Quotient c → Con.Quotient d → Prop} (p : Con.Quotient c) (q : Con.Quotient d) (H : (x : M) → (y : N) → C ↑x ↑y) :

C p q

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

@[simp]

theorem AddCon.eq {M : Type u_1} [inst : Add M] (c : AddCon M) {a : M} {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.

@[simp]

theorem Con.eq {M : Type u_1} [inst : Mul M] (c : Con M) {a : M} {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.

def AddCon.hasAdd.proof_1 {M : Type u_1} [inst : Add M] (c : AddCon M) :

(x x_1 : M) → Setoid.r x x_1 → (x_2 x_3 : M) → Setoid.r x_2 x_3 → ↑c (x + x_2) (x_1 + x_3)

Equations

(_ : ↑c (x + x) (x + x)) = (_ : ↑c (x + x) (x + x))

instance AddCon.hasAdd {M : Type u_1} [inst : Add M] (c : AddCon M) :

Add (AddCon.Quotient c)

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

Equations

AddCon.hasAdd c = { add := Quotient.map₂' (fun x x_1 => x + x_1) (AddCon.hasAdd.proof_1 c) }

instance Con.hasMul {M : Type u_1} [inst : Mul M] (c : Con M) :

Mul (Con.Quotient c)

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

Equations

Con.hasMul c = { mul := Quotient.map₂' (fun x x_1 => x * x_1) (Con.hasMul.proof_1 c) }

@[simp]

theorem AddCon.add_ker_mk_eq {M : Type u_1} [inst : Add M] (c : AddCon M) :

AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) = c

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

@[simp]

theorem Con.mul_ker_mk_eq {M : Type u_1} [inst : Mul M] (c : Con M) :

Con.mulKer Con.toQuotient (_ : ∀ (x x_1 : M), ↑(x * x_1) = ↑(x * x_1)) = c

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

@[simp]

theorem AddCon.coe_add {M : Type u_1} [inst : Add M] {c : AddCon M} (x : M) (y : M) :

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

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

@[simp]

theorem Con.coe_mul {M : Type u_1} [inst : Mul M] {c : Con M} (x : M) (y : M) :

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

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

@[simp]

theorem AddCon.liftOn_coe {M : Type u_2} [inst : Add M] {β : Sort u_1} (c : AddCon M) (f : M → β) (h : ∀ (a b : M), ↑c a b → f a = f b) (x : M) :

AddCon.liftOn (↑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.

@[simp]

theorem Con.liftOn_coe {M : Type u_2} [inst : Mul M] {β : Sort u_1} (c : Con M) (f : M → β) (h : ∀ (a b : M), ↑c a b → f a = f b) (x : M) :

Con.liftOn (↑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.

def AddCon.congr.proof_1 {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (h : c = d) (x : M) (y : M) :

↑c x y ↔ ↑d x y

Equations

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

def AddCon.congr {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (h : c = d) :

AddCon.Quotient c ≃+ AddCon.Quotient d

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.congr.proof_3 {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (h : c = d) :

Function.RightInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun

Equations

One or more equations did not get rendered due to their size.

def AddCon.congr.proof_4 {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (h : c = d) (x : AddCon.Quotient c) (y : AddCon.Quotient c) :

Equiv.toFun { toFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun, invFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun, left_inv := (_ : Function.LeftInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun), right_inv := (_ : Function.RightInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun) } (x + y) = Equiv.toFun { toFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun, invFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun, left_inv := (_ : Function.LeftInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun), right_inv := (_ : Function.RightInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun) } x + Equiv.toFun { toFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun, invFun := (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun, left_inv := (_ : Function.LeftInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun), right_inv := (_ : Function.RightInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun) } y

Equations

One or more equations did not get rendered due to their size.

def AddCon.congr.proof_2 {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} (h : c = d) :

Function.LeftInverse (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).invFun (Quotient.congr (Equiv.refl M) (_ : ∀ (x y : M), ↑c x y ↔ ↑d x y)).toFun

Equations

One or more equations did not get rendered due to their size.

def Con.congr {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} (h : c = d) :

Con.Quotient c ≃* Con.Quotient d

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

Equations

One or more equations did not get rendered due to their size.

instance AddCon.instLECon {M : Type u_1} [inst : Add M] :

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

Equations

AddCon.instLECon = { le := fun c d => ⦃x y : M⦄ → ↑c x y → ↑d x y }

instance Con.instLECon {M : Type u_1} [inst : Mul M] :

LE (Con M)

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

Equations

Con.instLECon = { le := fun c d => ⦃x y : M⦄ → ↑c x y → ↑d x y }

theorem AddCon.le_def {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} :

c ≤ d ↔ {x y : M} → ↑c x y → ↑d x y

Definition of ≤≤ for additive congruence relations.

theorem Con.le_def {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} :

c ≤ d ↔ {x y : M} → ↑c x y → ↑d x y

Definition of ≤≤ for congruence relations.

instance AddCon.instInfSetCon {M : Type u_1} [inst : Add M] :

InfSet (AddCon M)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.instInfSetCon.proof_1 {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

Equivalence fun x y => ∀ (c : AddCon M), c ∈ S → ↑c x y

Equations

(_ : Equivalence fun x y => ∀ (c : AddCon M), c ∈ S → ↑c x y) = (_ : Equivalence fun x y => ∀ (c : AddCon M), c ∈ S → ↑c x y)

def AddCon.instInfSetCon.proof_2 {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

{w x y z : M} → Setoid.r w x → Setoid.r y z → ∀ (c : AddCon M), c ∈ S → ↑c (w + y) (x + z)

Equations

(_ : ↑c (w + y) (x + z)) = (_ : ↑c (w + y) (x + z))

instance Con.instInfSetCon {M : Type u_1} [inst : Mul M] :

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

Equations

One or more equations did not get rendered due to their size.

abbrev AddCon.infₛ_toSetoid.match_1 {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) (r : Setoid M) (motive : r ∈ AddCon.toSetoid '' S → Prop) :

(x : r ∈ AddCon.toSetoid '' S) → ((c : AddCon M) → (hS : c ∈ S) → (hr : c.toSetoid = r) → motive (_ : ∃ a, a ∈ S ∧ a.toSetoid = r)) → motive x

Equations

AddCon.infₛ_toSetoid.match_1 S r motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem AddCon.infₛ_toSetoid {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

(infₛ S).toSetoid = infₛ (AddCon.toSetoid '' 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.

theorem Con.infₛ_toSetoid {M : Type u_1} [inst : Mul M] (S : Set (Con M)) :

(infₛ S).toSetoid = infₛ (Con.toSetoid '' 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.

theorem AddCon.infₛ_def {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

↑(infₛ S) = infₛ (FunLike.coe '' 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.

theorem Con.infₛ_def {M : Type u_1} [inst : Mul M] (S : Set (Con M)) :

↑(infₛ S) = infₛ (FunLike.coe '' 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.

def AddCon.instPartialOrderCon.proof_1 {M : Type u_1} [inst : Add M] :

(x : AddCon M) → (x_1 x_2 : M) → ↑x x_1 x_2 → ↑x x_1 x_2

Equations

(_ : ↑x x x → ↑x x x) = (_ : ↑x x x → ↑x x x)

def AddCon.instPartialOrderCon.proof_4 {M : Type u_1} [inst : Add M] :

∀ (x x_1 : AddCon M), x ≤ x_1 → x_1 ≤ x → x = x_1

Equations

(_ : x = x) = (_ : x = x)

instance AddCon.instPartialOrderCon {M : Type u_1} [inst : Add M] :

PartialOrder (AddCon M)

Equations

AddCon.instPartialOrderCon = PartialOrder.mk (_ : ∀ (x x_1 : AddCon M), x ≤ x_1 → x_1 ≤ x → x = x_1)

def AddCon.instPartialOrderCon.proof_3 {M : Type u_1} [inst : Add M] :

∀ (x x_1 : AddCon M), x < x_1 ↔ x < x_1

Equations

(_ : x < x ↔ x < x) = (_ : x < x ↔ x < x)

def AddCon.instPartialOrderCon.proof_2 {M : Type u_1} [inst : Add M] :

(x x_1 x_2 : AddCon M) → x ≤ x_1 → x_1 ≤ x_2 → (x_3 x_4 : M) → ↑x x_3 x_4 → ↑x_2 x_3 x_4

Equations

(_ : ↑x x x) = h2 x x (h1 x x h)

instance Con.instPartialOrderCon {M : Type u_1} [inst : Mul M] :

PartialOrder (Con M)

Equations

Con.instPartialOrderCon = PartialOrder.mk (_ : ∀ (x x_1 : Con M), x ≤ x_1 → x_1 ≤ x → x = x_1)

def AddCon.instCompleteLatticeCon.proof_4 {M : Type u_1} [inst : Add M] :

∀ (x x_1 : AddCon M) (x_2 x_3 : M), ↑(x ⊓ x_1) x_2 x_3 → Setoid.Rel x_1.toSetoid x_2 x_3

Equations

(_ : Setoid.Rel x.toSetoid x x) = (_ : Setoid.Rel x.toSetoid x x)

def AddCon.instCompleteLatticeCon.proof_13 {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M) (y : M) (h : ↑⊥ x y) :

↑c x y

Equations

(_ : ↑c x y) = (_ : ↑c x y)

instance AddCon.instCompleteLatticeCon {M : Type u_1} [inst : Add M] :

CompleteLattice (AddCon M)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.instCompleteLatticeCon.proof_9 {M : Type u_1} [inst : Add M] (s : Set (AddCon M)) (a : AddCon M) :

(∀ (b : AddCon M), b ∈ s → a ≤ b) → a ≤ infₛ s

Equations

(_ : ∀ (s : Set (AddCon M)) (a : AddCon M), (∀ (b : AddCon M), b ∈ s → a ≤ b) → a ≤ infₛ s) = (_ : ∀ (s : Set (AddCon M)) (a : AddCon M), (∀ (b : AddCon M), b ∈ s → a ≤ b) → a ≤ infₛ s)

def AddCon.instCompleteLatticeCon.proof_1 {M : Type u_1} [inst : Add M] (s : Set (AddCon M)) :

infₛ s ∈ lowerBounds s ∧ infₛ s ∈ upperBounds (lowerBounds s)

Equations

(_ : infₛ s ∈ lowerBounds s ∧ infₛ s ∈ upperBounds (lowerBounds s)) = (_ : infₛ s ∈ lowerBounds s ∧ infₛ s ∈ upperBounds (lowerBounds s))

def AddCon.instCompleteLatticeCon.proof_12 {M : Type u_1} [inst : Add M] :

∀ (x : AddCon M) (x_1 x_2 : M), ↑x x_1 x_2 → True

Equations

(_ : True) = trivial

def AddCon.instCompleteLatticeCon.proof_3 {M : Type u_1} [inst : Add M] :

∀ (x x_1 : AddCon M) (x_2 x_3 : M), ↑(x ⊓ x_1) x_2 x_3 → Setoid.Rel x.toSetoid x_2 x_3

Equations

(_ : Setoid.Rel x.toSetoid x x) = (_ : Setoid.Rel x.toSetoid x x)

def AddCon.instCompleteLatticeCon.proof_10 {M : Type u_1} :

∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r y z

Equations

(_ : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r y z) = (_ : ∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r y z)

def AddCon.instCompleteLatticeCon.proof_5 {M : Type u_1} [inst : Add M] :

∀ (x x_1 x_2 : AddCon M), x ≤ x_1 → x ≤ x_2 → ∀ (x_3 x_4 : M), ↑x x_3 x_4 → Setoid.Rel x_1.toSetoid x_3 x_4 ∧ Setoid.Rel x_2.toSetoid x_3 x_4

Equations

(_ : Setoid.Rel x.toSetoid x x ∧ Setoid.Rel x.toSetoid x x) = (_ : Setoid.Rel x.toSetoid x x ∧ Setoid.Rel x.toSetoid x x)

def AddCon.instCompleteLatticeCon.proof_7 {M : Type u_1} [inst : Add M] (s : Set (AddCon M)) (a : AddCon M) :

(∀ (b : AddCon M), b ∈ s → b ≤ a) → supₛ s ≤ a

Equations

(_ : ∀ (s : Set (AddCon M)) (a : AddCon M), (∀ (b : AddCon M), b ∈ s → b ≤ a) → supₛ s ≤ a) = (_ : ∀ (s : Set (AddCon M)) (a : AddCon M), (∀ (b : AddCon M), b ∈ s → b ≤ a) → supₛ s ≤ a)

def AddCon.instCompleteLatticeCon.proof_2 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : AddCon M) :

∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.Rel c.toSetoid (w + y) (x + z) ∧ Setoid.Rel d.toSetoid (w + y) (x + z)

Equations

(_ : Setoid.Rel c.toSetoid (w + y) (x + z) ∧ Setoid.Rel d.toSetoid (w + y) (x + z)) = (_ : Setoid.Rel c.toSetoid (w + y) (x + z) ∧ Setoid.Rel d.toSetoid (w + y) (x + z))

def AddCon.instCompleteLatticeCon.proof_8 {M : Type u_1} [inst : Add M] (s : Set (AddCon M)) (a : AddCon M) :

a ∈ s → infₛ s ≤ a

Equations

(_ : ∀ (s : Set (AddCon M)) (a : AddCon M), a ∈ s → infₛ s ≤ a) = (_ : ∀ (s : Set (AddCon M)) (a : AddCon M), a ∈ s → infₛ s ≤ a)

def AddCon.instCompleteLatticeCon.proof_6 {M : Type u_1} [inst : Add M] (s : Set (AddCon M)) (a : AddCon M) :

a ∈ s → a ≤ supₛ s

Equations

(_ : ∀ (s : Set (AddCon M)) (a : AddCon M), a ∈ s → a ≤ supₛ s) = (_ : ∀ (s : Set (AddCon M)) (a : AddCon M), a ∈ s → a ≤ supₛ s)

def AddCon.instCompleteLatticeCon.proof_11 {M : Type u_1} [inst : Add M] :

∀ {w x y z : M}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)

Equations

(_ : Setoid.r (w + y) (x + z)) = (_ : Setoid.r (w + y) (x + z))

instance Con.instCompleteLatticeCon {M : Type u_1} [inst : Mul M] :

CompleteLattice (Con M)

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

Equations

One or more equations did not get rendered due to their size.

theorem AddCon.inf_def {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} :

Setoid.r = Setoid.r ⊓ Setoid.r

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

theorem Con.inf_def {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} :

Setoid.r = Setoid.r ⊓ Setoid.r

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

theorem AddCon.inf_iff_and {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} {x : M} {y : M} :

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

Definition of the infimum of two additive congruence relations.

theorem Con.inf_iff_and {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} {x : M} {y : M} :

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

Definition of the infimum of two congruence relations.

theorem AddCon.addConGen_eq {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

addConGen r = infₛ { s | (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.

theorem Con.conGen_eq {M : Type u_1} [inst : Mul M] (r : M → M → Prop) :

conGen r = infₛ { s | (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.

theorem AddCon.addConGen_le {M : Type u_1} [inst : Add M] {r : M → M → Prop} {c : AddCon M} (h : ∀ (x y : M), r x y → Setoid.r x y) :

addConGen r ≤ c

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

theorem Con.conGen_le {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {c : Con M} (h : ∀ (x y : M), r x y → Setoid.r x y) :

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

theorem AddCon.addConGen_mono {M : Type u_1} [inst : Add M] {r : M → M → Prop} {s : M → M → Prop} (h : (x y : M) → r x y → s x y) :

addConGen r ≤ addConGen 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.

theorem Con.conGen_mono {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {s : M → M → Prop} (h : (x y : M) → r x y → s x y) :

conGen r ≤ conGen s

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

@[simp]

theorem AddCon.addConGen_of_addCon {M : Type u_1} [inst : Add M] (c : AddCon M) :

addConGen ↑c = c

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

@[simp]

theorem Con.conGen_of_con {M : Type u_1} [inst : Mul M] (c : Con M) :

conGen ↑c = c

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

theorem AddCon.addConGen_idem {M : Type u_1} [inst : Add M] (r : M → M → Prop) :

addConGen ↑(addConGen r) = addConGen r

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

theorem Con.conGen_idem {M : Type u_1} [inst : Mul M] (r : M → M → Prop) :

conGen ↑(conGen r) = conGen r

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

theorem AddCon.sup_eq_addConGen {M : Type u_1} [inst : Add M] (c : AddCon M) (d : AddCon M) :

c ⊔ d = addConGen fun x y => ↑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'.

theorem Con.sup_eq_conGen {M : Type u_1} [inst : Mul M] (c : Con M) (d : Con M) :

c ⊔ d = conGen fun x y => ↑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'.

theorem AddCon.sup_def {M : Type u_1} [inst : Add M] {c : AddCon M} {d : AddCon M} :

c ⊔ d = addConGen (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.

theorem Con.sup_def {M : Type u_1} [inst : Mul M] {c : Con M} {d : Con M} :

c ⊔ d = conGen (Setoid.r ⊔ Setoid.r)

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

abbrev AddCon.supₛ_eq_addConGen.match_1 {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

(x x_1 : M) → ∀ (motive : (∃ c, c ∈ S ∧ ↑c x x_1) → Prop) (x_2 : ∃ c, c ∈ S ∧ ↑c x x_1), (∀ (r : AddCon M) (hr : r ∈ S ∧ ↑r x x_1), motive (_ : ∃ c, c ∈ S ∧ ↑c x x_1)) → motive x_2

Equations

AddCon.supₛ_eq_addConGen.match_1 S x x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem AddCon.supₛ_eq_addConGen {M : Type u_1} [inst : Add M] (S : Set (AddCon M)) :

supₛ S = addConGen fun x y => ∃ c, 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∈ S such that x is related to y by c'.

theorem Con.supₛ_eq_conGen {M : Type u_1} [inst : Mul M] (S : Set (Con M)) :

supₛ S = conGen fun x y => ∃ c, 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∈ S such that x is related to y by c'.

theorem AddCon.supₛ_def {M : Type u_1} [inst : Add M] {S : Set (AddCon M)} :

supₛ S = addConGen (supₛ (FunLike.coe '' 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.

theorem Con.supₛ_def {M : Type u_1} [inst : Mul M] {S : Set (Con M)} :

supₛ S = conGen (supₛ (FunLike.coe '' 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.

def AddCon.gi (M : Type u_1) [inst : Add M] :

GaloisInsertion addConGen FunLike.coe

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.gi.proof_2 (M : Type u_1) [inst : Add M] (x : AddCon M) :

x ≤ addConGen ↑x

Equations

(_ : x ≤ addConGen ↑x) = (_ : x ≤ addConGen ↑x)

def AddCon.gi.proof_3 (M : Type u_1) [inst : Add M] :

∀ (x : M → M → Prop) (x_1 : ↑(addConGen x) ≤ x), (fun r x => addConGen r) x x_1 = (fun r x => addConGen r) x x_1

Equations

(_ : (fun r x => addConGen r) x x = (fun r x => addConGen r) x x) = (_ : (fun r x => addConGen r) x x = (fun r x => addConGen r) x x)

def AddCon.gi.proof_1 (M : Type u_1) [inst : Add M] :

∀ (x : M → M → Prop) (c : AddCon M), addConGen x ≤ c ↔ x ≤ ↑c

Equations

(_ : addConGen x ≤ c ↔ x ≤ ↑c) = (_ : addConGen x ≤ c ↔ x ≤ ↑c)

def Con.gi (M : Type u_1) [inst : Mul M] :

GaloisInsertion conGen FunLike.coe

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.mapGen {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (c : AddCon M) (f : M → N) :

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

Equations

AddCon.mapGen c f = addConGen fun x y => ∃ a b, f a = x ∧ f b = y ∧ ↑c a b

def Con.mapGen {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (c : Con M) (f : M → N) :

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

Equations

Con.mapGen c f = conGen fun x y => ∃ a b, f a = x ∧ f b = y ∧ ↑c a b

def AddCon.mapOfSurjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (c : AddCon M) (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H ≤ c) (hf : Function.Surjective f) :

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≈ y iff the elements of f⁻¹(x)⁻¹(x) are related to the elements of f⁻¹(y)⁻¹(y) by c.'

Equations

One or more equations did not get rendered due to their size.

def AddCon.mapOfSurjective.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (c : AddCon M) (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H ≤ c) (hf : Function.Surjective f) :

∀ {w x y z : N}, Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)

Equations

(_ : Setoid.r (w + y) (x + z)) = (_ : Setoid.r (w + y) (x + z))

def Con.mapOfSurjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (c : Con M) (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (h : Con.mulKer f H ≤ c) (hf : Function.Surjective f) :

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≈ y iff the elements of f⁻¹(x)⁻¹(x) are related to the elements of f⁻¹(y)⁻¹(y) by c.'

Equations

One or more equations did not get rendered due to their size.

theorem AddCon.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {c : AddCon M} {f : M → N} (H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H ≤ c) (hf : Function.Surjective f) :

AddCon.mapGen c f = AddCon.mapOfSurjective c f H h hf

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

theorem Con.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {c : Con M} {f : M → N} (H : ∀ (x y : M), f (x * y) = f x * f y) (h : Con.mulKer f H ≤ c) (hf : Function.Surjective f) :

Con.mapGen c f = Con.mapOfSurjective c f H h hf

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

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

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

Equations

AddCon.comap f H c = let src := Setoid.comap f c.toSetoid; { toSetoid := { r := Setoid.r, iseqv := (_ : Equivalence Setoid.r) }, add' := AddCon.comap.proof_1 f H c }

def AddCon.comap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (c : AddCon N) (w : M) (x : M) (y : M) (z : M) (h1 : Setoid.r w x) (h2 : Setoid.r y z) :

↑c (f (w + y)) (f (x + z))

Equations

(_ : ↑c (f (w + y)) (f (x + z))) = (_ : ↑c (f (w + y)) (f (x + z)))

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

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

Equations

Con.comap f H c = let src := Setoid.comap f c.toSetoid; { toSetoid := { r := Setoid.r, iseqv := (_ : Equivalence Setoid.r) }, mul' := Con.comap.proof_1 f H c }

@[simp]

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

↑(AddCon.comap f H c) x y ↔ ↑c (f x) (f y)

@[simp]

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

↑(Con.comap f H c) x y ↔ ↑c (f x) (f y)

def AddCon.correspondence.proof_3 {M : Type u_1} [inst : Add M] (c : AddCon M) (q : Quotient c.toSetoid) :

∃ a, Quotient.mk c.toSetoid a = q

Equations

(_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q) = (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)

def AddCon.correspondence.proof_7 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : AddCon (AddCon.Quotient c)) :

(fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) ((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d) = d

Equations

One or more equations did not get rendered due to their size.

def AddCon.correspondence.proof_4 {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M) (y : M) :

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

Equations

(_ : ↑(x + y) = ↑(x + y)) = (_ : ↑(x + y) = ↑(x + y))

def AddCon.correspondence.proof_1 {M : Type u_1} [inst : Add M] (c : AddCon M) :

∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

abbrev AddCon.correspondence.match_1 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : { d // c ≤ d }) (x : M) (y : M) (motive : ↑↑((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) ((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) d)) x y → Prop) :

(h : ↑↑((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) ((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) d)) x y) → ((a b : M) → (hx : ↑a = ↑x) → (hy : ↑b = ↑y) → (H : Setoid.Rel (↑d).toSetoid a b) → motive (_ : ∃ a b, ↑a = ↑x ∧ ↑b = ↑y ∧ Setoid.Rel (↑d).toSetoid a b)) → motive h

Equations

One or more equations did not get rendered due to their size.

def AddCon.correspondence {M : Type u_1} [inst : Add M] (c : AddCon M) :

{ d // c ≤ d } ≃o AddCon (AddCon.Quotient c)

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

One or more equations did not get rendered due to their size.

def AddCon.correspondence.proof_8 {M : Type u_1} [inst : Add M] (c : AddCon M) (s : { d // c ≤ d }) (t : { d // c ≤ d }) :

↑{ toFun := fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q), invFun := fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }, left_inv := (_ : ∀ (d : { d // c ≤ d }), (fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) ((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) d) = d), right_inv := (_ : ∀ (d : AddCon (AddCon.Quotient c)), (fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) ((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d) = d) } s ≤ ↑{ toFun := fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q), invFun := fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }, left_inv := (_ : ∀ (d : { d // c ≤ d }), (fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) ((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) d) = d), right_inv := (_ : ∀ (d : AddCon (AddCon.Quotient c)), (fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) ((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d) = d) } t ↔ s ≤ t

Equations

One or more equations did not get rendered due to their size.

abbrev AddCon.correspondence.match_2 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : AddCon (AddCon.Quotient c)) (x : AddCon.Quotient c) (y : AddCon.Quotient c) (motive : ↑((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) ((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d)) x y → Prop) :

(h : ↑((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) ((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d)) x y) → ((w w_1 : M) → (hx : ↑w = x) → (hy : ↑w_1 = y) → (H : Setoid.Rel (↑((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d)).toSetoid w w_1) → motive (_ : ∃ a b, ↑a = x ∧ ↑b = y ∧ Setoid.Rel (↑((fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) d)).toSetoid a b)) → motive h

Equations

One or more equations did not get rendered due to their size.

def AddCon.correspondence.proof_6 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : { d // c ≤ d }) :

(fun d => { val := AddCon.comap AddCon.toQuotient (_ : ∀ (x y : M), ↑(x + y) = ↑(x + y)) d, property := fun x y => (_ : ↑c x y → ↑d ↑x ↑y) }) ((fun d => AddCon.mapOfSurjective (↑d) AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) (_ : ∀ (q : Quotient c.toSetoid), ∃ a, Quotient.mk c.toSetoid a = q)) d) = d

Equations

One or more equations did not get rendered due to their size.

def AddCon.correspondence.proof_2 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : { d // c ≤ d }) :

AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d

Equations

(_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d) = (_ : AddCon.addKer AddCon.toQuotient (_ : ∀ (x x_1 : M), ↑(x + x_1) = ↑(x + x_1)) ≤ ↑d)

def AddCon.correspondence.proof_5 {M : Type u_1} [inst : Add M] (c : AddCon M) (d : AddCon (AddCon.Quotient c)) (x : M) (y : M) (h : ↑c x y) :

↑d ↑x ↑y

Equations

(_ : ↑d ↑x ↑y) = (_ : ↑d ↑x ↑y)

def Con.correspondence {M : Type u_1} [inst : Mul M] (c : Con M) :

{ d // c ≤ d } ≃o Con (Con.Quotient c)

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

One or more equations did not get rendered due to their size.

def AddCon.addZeroClass.proof_1 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (x : AddCon.Quotient c) :

0 + x = x

Equations

(_ : 0 + x = x) = (_ : 0 + x = x)

def AddCon.addZeroClass.proof_2 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (x : AddCon.Quotient c) :

x + 0 = x

Equations

(_ : x + 0 = x) = (_ : x + 0 = x)

instance AddCon.addZeroClass {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

AddZeroClass (AddCon.Quotient c)

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

Equations

AddCon.addZeroClass c = AddZeroClass.mk (_ : ∀ (x : AddCon.Quotient c), 0 + x = x) (_ : ∀ (x : AddCon.Quotient c), x + 0 = x)

instance Con.mulOneClass {M : Type u_1} [inst : MulOneClass M] (c : Con M) :

MulOneClass (Con.Quotient c)

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

Equations

Con.mulOneClass c = MulOneClass.mk (_ : ∀ (x : Con.Quotient c), 1 * x = x) (_ : ∀ (x : Con.Quotient c), x * 1 = x)

@[simp]

theorem AddCon.coe_zero {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} :

↑0 = 0

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

@[simp]

theorem Con.coe_one {M : Type u_1} [inst : MulOneClass 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.

def AddCon.addSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

Equations

(_ : Setoid.r 0 0) = (_ : Setoid.r 0 0)

def AddCon.addSubmonoid {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

AddSubmonoid (M × M)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.addSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

∀ {a b : M × M}, ↑c a.fst a.snd → ↑c b.fst b.snd → ↑c (a.fst + b.fst) (a.snd + b.snd)

Equations

(_ : ↑c a.fst a.snd → ↑c b.fst b.snd → ↑c (a.fst + b.fst) (a.snd + b.snd)) = (_ : ↑c a.fst a.snd → ↑c b.fst b.snd → ↑c (a.fst + b.fst) (a.snd + b.snd))

def Con.submonoid {M : Type u_1} [inst : MulOneClass M] (c : Con M) :

Submonoid (M × M)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.ofAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] (N : AddSubmonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N) :

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

Equations

AddCon.ofAddSubmonoid N H = { toSetoid := { r := fun x y => (x, y) ∈ N, iseqv := H }, add' := (_ : ∀ {w x y z : M}, (w, x) ∈ N → (y, z) ∈ N → (w, x) + (y, z) ∈ N) }

def AddCon.ofAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] (N : AddSubmonoid (M × M)) :

∀ {w x y z : M}, (w, x) ∈ N → (y, z) ∈ N → (w, x) + (y, z) ∈ N

Equations

(_ : (w, x) ∈ N → (y, z) ∈ N → (w, x) + (y, z) ∈ N) = (_ : (w, x) ∈ N → (y, z) ∈ N → (w, x) + (y, z) ∈ N)

def Con.ofSubmonoid {M : Type u_1} [inst : MulOneClass M] (N : Submonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N) :

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

Equations

Con.ofSubmonoid N H = { toSetoid := { r := fun x y => (x, y) ∈ N, iseqv := H }, mul' := (_ : ∀ {w x y z : M}, (w, x) ∈ N → (y, z) ∈ N → (w, x) * (y, z) ∈ N) }

instance AddCon.toAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

Coe (AddCon M) (AddSubmonoid (M × M))

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

Equations

AddCon.toAddSubmonoid = { coe := fun c => ↑c }

instance Con.toSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Coe (Con M) (Submonoid (M × M))

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

Equations

Con.toSubmonoid = { coe := fun c => ↑c }

theorem AddCon.mem_coe {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} {x : M} {y : M} :

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

theorem Con.mem_coe {M : Type u_1} [inst : MulOneClass M] {c : Con M} {x : M} {y : M} :

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

theorem AddCon.to_addSubmonoid_inj {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (H : ↑c = ↑d) :

c = d

theorem Con.to_submonoid_inj {M : Type u_1} [inst : MulOneClass M] (c : Con M) (d : Con M) (H : ↑c = ↑d) :

c = d

theorem AddCon.le_iff {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} {d : AddCon M} :

c ≤ d ↔ ↑c ≤ ↑d

theorem Con.le_iff {M : Type u_1} [inst : MulOneClass M] {c : Con M} {d : Con M} :

c ≤ d ↔ ↑c ≤ ↑d

def AddCon.ker.proof_1 {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (x : M) (y : M) :

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

Equations

(_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) = (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y)

def AddCon.ker {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

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

Equations

AddCon.ker f = AddCon.addKer ↑f (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y)

def Con.ker {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) :

The kernel of a monoid homomorphism as a congruence relation.

Equations

Con.ker f = Con.mulKer ↑f (_ : ∀ (x y : M), ↑f (x * y) = ↑f x * ↑f y)

@[simp]

theorem AddCon.ker_rel {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) {x : M} {y : M} :

↑(AddCon.ker f) x y ↔ ↑f x = ↑f y

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

@[simp]

theorem Con.ker_rel {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) {x : M} {y : M} :

↑(Con.ker f) x y ↔ ↑f x = ↑f y

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

instance AddCon.Quotient.inhabited {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} :

Inhabited (AddCon.Quotient c)

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

Equations

AddCon.Quotient.inhabited = { default := ↑0 }

instance Con.Quotient.inhabited {M : Type u_1} [inst : MulOneClass M] {c : Con M} :

Inhabited (Con.Quotient c)

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

Equations

Con.Quotient.inhabited = { default := ↑1 }

def AddCon.mk'.proof_2 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

∀ (x x_1 : M), ZeroHom.toFun { toFun := AddCon.toQuotient, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) = ZeroHom.toFun { toFun := AddCon.toQuotient, map_zero' := (_ : ↑0 = ↑0) } (x + x_1)

Equations

One or more equations did not get rendered due to their size.

def AddCon.mk'.proof_1 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddCon.mk' {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

M →+ AddCon.Quotient c

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

Equations

One or more equations did not get rendered due to their size.

def Con.mk' {M : Type u_1} [inst : MulOneClass M] (c : Con M) :

M →* Con.Quotient c

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem AddCon.mk'_ker {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

AddCon.ker (AddCon.mk' c) = c

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

@[simp]

theorem Con.mk'_ker {M : Type u_1} [inst : MulOneClass M] (c : Con M) :

Con.ker (Con.mk' c) = c

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

theorem AddCon.mk'_surjective {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} :

Function.Surjective ↑(AddCon.mk' c)

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

theorem Con.mk'_surjective {M : Type u_1} [inst : MulOneClass M] {c : Con M} :

Function.Surjective ↑(Con.mk' c)

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

@[simp]

theorem AddCon.coe_mk' {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} :

↑(AddCon.mk' c) = AddCon.toQuotient

@[simp]

theorem Con.coe_mk' {M : Type u_1} [inst : MulOneClass M] {c : Con M} :

↑(Con.mk' c) = Con.toQuotient

@[simp]

theorem AddCon.mrange_mk' {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} :

AddMonoidHom.mrange (AddCon.mk' c) = ⊤

@[simp]

theorem Con.mrange_mk' {M : Type u_1} [inst : MulOneClass M] {c : Con M} :

MonoidHom.mrange (Con.mk' c) = ⊤

theorem AddCon.ker_apply_eq_preimage {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {f : M →+ P} (x : M) :

↑(AddCon.ker f) x = ↑f ⁻¹' {↑f x}

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

theorem Con.ker_apply_eq_preimage {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {f : M →* P} (x : M) :

↑(Con.ker f) x = ↑f ⁻¹' {↑f x}

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

theorem AddCon.comap_eq {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {c : AddCon M} {f : N →+ M} :

AddCon.comap ↑f (_ : ∀ (a b : N), ↑f (a + b) = ↑f a + ↑f b) c = AddCon.ker (AddMonoidHom.comp (AddCon.mk' c) f)

Given an AddMonoid homomorphism f : N → M→ 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.

theorem Con.comap_eq {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {c : Con M} {f : N →* M} :

Con.comap ↑f (_ : ∀ (a b : N), ↑f (a * b) = ↑f a * ↑f b) c = Con.ker (MonoidHom.comp (Con.mk' c) f)

Given a monoid homomorphism f : N → M→ 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.

def AddCon.lift {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) :

AddCon.Quotient c →+ P

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.lift.proof_3 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) (x : AddCon.Quotient c) (y : AddCon.Quotient c) :

ZeroHom.toFun { toFun := fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h, map_zero' := (_ : (fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h, map_zero' := (_ : (fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0) } x + ZeroHom.toFun { toFun := fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h, map_zero' := (_ : (fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0) } y

Equations

One or more equations did not get rendered due to their size.

def AddCon.lift.proof_2 {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) :

(fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0

Equations

(_ : (fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0) = (_ : (fun x => AddCon.liftOn x ↑f fun x x_1 h => H x x_1 h) 0 = 0)

def AddCon.lift.proof_1 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) :

(x x_1 : M) → ↑c x x_1 → ↑(AddCon.ker f) x x_1

Equations

(_ : ↑(AddCon.ker f) x x) = H x x h

def Con.lift {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (c : Con M) (f : M →* P) (H : c ≤ Con.ker f) :

Con.Quotient c →* 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

One or more equations did not get rendered due to their size.

theorem AddCon.lift_mk' {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.ker f) (x : M) :

↑(AddCon.lift c f H) (↑(AddCon.mk' c) x) = ↑f x

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

theorem Con.lift_mk' {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) (x : M) :

↑(Con.lift c f H) (↑(Con.mk' c) x) = ↑f x

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

@[simp]

theorem AddCon.lift_coe {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.ker f) (x : M) :

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

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

@[simp]

theorem Con.lift_coe {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) (x : M) :

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

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

@[simp]

theorem AddCon.lift_comp_mk' {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.ker f) :

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

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

@[simp]

theorem Con.lift_comp_mk' {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) :

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

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

@[simp]

theorem AddCon.lift_apply_mk' {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} (f : AddCon.Quotient c →+ P) :

AddCon.lift c (AddMonoidHom.comp f (AddCon.mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) = f

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

@[simp]

theorem Con.lift_apply_mk' {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} (f : Con.Quotient c →* P) :

Con.lift c (MonoidHom.comp f (Con.mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) = 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.

theorem AddCon.lift_funext {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} (f : AddCon.Quotient c →+ P) (g : AddCon.Quotient c →+ P) (h : ∀ (a : M), ↑f ↑a = ↑g ↑a) :

f = g

Homomorphisms on the quotient of an AddMonoidby an additive congruence relation are equal if they are equal on elements that are coercions from theAddMonoid`.

theorem Con.lift_funext {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} (f : Con.Quotient c →* P) (g : Con.Quotient c →* 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.

theorem AddCon.lift_unique {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.ker f) (g : AddCon.Quotient c →+ P) (Hg : AddMonoidHom.comp g (AddCon.mk' c) = f) :

g = AddCon.lift c f H

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

theorem Con.lift_unique {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) (g : Con.Quotient c →* P) (Hg : MonoidHom.comp g (Con.mk' c) = f) :

g = Con.lift c f H

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

abbrev AddCon.lift_range.match_1 {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] {f : M →+ P} (x : P) (motive : x ∈ AddMonoidHom.mrange f → Prop) :

(x : x ∈ AddMonoidHom.mrange f) → ((y : M) → (hy : ↑f y = x) → motive (_ : ∃ y, ↑f y = x)) → motive x

Equations

AddCon.lift_range.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem AddCon.lift_range {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.ker f) :

AddMonoidHom.mrange (AddCon.lift c f H) = AddMonoidHom.mrange f

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

theorem Con.lift_range {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) :

MonoidHom.mrange (Con.lift c f H) = MonoidHom.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.

theorem AddCon.lift_surjective_of_surjective {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] {c : AddCon M} {f : M →+ P} (h : c ≤ AddCon.ker f) (hf : Function.Surjective ↑f) :

Function.Surjective ↑(AddCon.lift c f h)

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

theorem Con.lift_surjective_of_surjective {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] {c : Con M} {f : M →* P} (h : c ≤ Con.ker f) (hf : Function.Surjective ↑f) :

Function.Surjective ↑(Con.lift c f h)

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

theorem AddCon.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) (h : Function.Injective ↑(AddCon.lift c f H)) :

AddCon.ker f = c

Given an AddMonoid 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.

theorem Con.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (c : Con M) (f : M →* P) (H : c ≤ Con.ker f) (h : Function.Injective ↑(Con.lift c f H)) :

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.

def AddCon.kerLift.proof_1 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

(x x_1 : M) → ↑(AddCon.ker f) x x_1 → ↑(AddCon.ker f) x x_1

Equations

(_ : ↑(AddCon.ker f) x x → ↑(AddCon.ker f) x x) = (_ : ↑(AddCon.ker f) x x → ↑(AddCon.ker f) x x)

def AddCon.kerLift {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

AddCon.Quotient (AddCon.ker f) →+ P

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

Equations

AddCon.kerLift f = AddCon.lift (AddCon.ker f) f (AddCon.kerLift.proof_1 f)

def Con.kerLift {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) :

Con.Quotient (Con.ker f) →* P

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

Equations

Con.kerLift f = Con.lift (Con.ker f) f (Con.kerLift.proof_1 f)

@[simp]

theorem AddCon.kerLift_mk {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] {f : M →+ P} (x : M) :

↑(AddCon.kerLift f) ↑x = ↑f x

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

@[simp]

theorem Con.kerLift_mk {M : Type u_2} {P : Type u_1} [inst : MulOneClass M] [inst : MulOneClass P] {f : M →* P} (x : M) :

↑(Con.kerLift 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.

@[simp]

theorem AddCon.kerLift_range_eq {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] {f : M →+ P} :

AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f

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

@[simp]

theorem Con.kerLift_range_eq {M : Type u_2} {P : Type u_1} [inst : MulOneClass M] [inst : MulOneClass P] {f : M →* P} :

MonoidHom.mrange (Con.kerLift f) = MonoidHom.mrange f

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

theorem AddCon.kerLift_injective {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

Function.Injective ↑(AddCon.kerLift f)

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

theorem Con.kerLift_injective {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) :

Function.Injective ↑(Con.kerLift f)

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

def AddCon.map {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) :

AddCon.Quotient c →+ AddCon.Quotient d

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

Equations

AddCon.map c d h = AddCon.lift c (AddCon.mk' d) (AddCon.map.proof_1 c d h)

def AddCon.map.proof_1 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) (x : M) (y : M) (hc : ↑c x y) :

↑(AddCon.ker (AddCon.mk' d)) x y

Equations

(_ : ↑(AddCon.ker (AddCon.mk' d)) x y) = (_ : ↑(AddCon.ker (AddCon.mk' d)) x y)

def Con.map {M : Type u_1} [inst : MulOneClass M] (c : Con M) (d : Con M) (h : c ≤ d) :

Con.Quotient c →* Con.Quotient d

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

Con.map c d h = Con.lift c (Con.mk' d) (Con.map.proof_1 c d h)

theorem AddCon.map_apply {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} {d : AddCon M} (h : c ≤ d) (x : AddCon.Quotient c) :

↑(AddCon.map c d h) x = ↑(AddCon.lift c (AddCon.mk' d) (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑x = ↑x_1)) x

Given additive congruence relations c, d on an AddMonoid 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.

theorem Con.map_apply {M : Type u_1} [inst : MulOneClass M] {c : Con M} {d : Con M} (h : c ≤ d) (x : Con.Quotient c) :

↑(Con.map c d h) x = ↑(Con.lift c (Con.mk' d) (_ : ∀ (x x_1 : M), ↑c x x_1 → ↑x = ↑x_1)) 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.

def AddCon.quotientKerEquivRange.proof_3 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

Function.RightInverse (Equiv.ofBijective ↑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f))) (AddMonoidHom.mrangeRestrict (AddCon.kerLift f))) (_ : Function.Bijective (↑(AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f)).toEquiv ∘ fun x => ↑(AddMonoidHom.mrangeRestrict (AddCon.kerLift f)) x))).invFun (Equiv.ofBijective ↑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f))) (AddMonoidHom.mrangeRestrict (AddCon.kerLift f))) (_ : Function.Bijective (↑(AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f)).toEquiv ∘ fun x => ↑(AddMonoidHom.mrangeRestrict (AddCon.kerLift f)) x))).toFun

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivRange.proof_1 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

Function.Bijective (↑(AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f)).toEquiv ∘ fun x => ↑(AddMonoidHom.mrangeRestrict (AddCon.kerLift f)) x)

Equations

One or more equations did not get rendered due to their size.

noncomputable def AddCon.quotientKerEquivRange {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

AddCon.Quotient (AddCon.ker f) ≃+ { x // x ∈ AddMonoidHom.mrange f }

The first isomorphism theorem for AddMonoids.

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivRange.proof_2 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) :

Function.LeftInverse (Equiv.ofBijective ↑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f))) (AddMonoidHom.mrangeRestrict (AddCon.kerLift f))) (_ : Function.Bijective (↑(AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f)).toEquiv ∘ fun x => ↑(AddMonoidHom.mrangeRestrict (AddCon.kerLift f)) x))).invFun (Equiv.ofBijective ↑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f))) (AddMonoidHom.mrangeRestrict (AddCon.kerLift f))) (_ : Function.Bijective (↑(AddEquiv.addSubmonoidCongr (_ : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f)).toEquiv ∘ fun x => ↑(AddMonoidHom.mrangeRestrict (AddCon.kerLift f)) x))).toFun

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivRange.proof_4 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (a : AddCon.Quotient (AddCon.ker f)) (b : AddCon.Quotient (AddCon.ker f)) :

Equations

One or more equations did not get rendered due to their size.

abbrev AddCon.quotientKerEquivRange.match_1 {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (motive : { x // x ∈ AddMonoidHom.mrange (AddCon.kerLift f) } → Prop) :

(x : { x // x ∈ AddMonoidHom.mrange (AddCon.kerLift f) }) → ((w : P) → (z : AddCon.Quotient (AddCon.ker f)) → (hz : ↑(AddCon.kerLift f) z = w) → motive { val := w, property := (_ : ∃ y, ↑(AddCon.kerLift f) y = w) }) → motive x

Equations

AddCon.quotientKerEquivRange.match_1 f motive x h_1 = Subtype.casesOn x fun val property => Exists.casesOn property fun w h => h_1 val w h

noncomputable def Con.quotientKerEquivRange {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) :

Con.Quotient (Con.ker f) ≃* { x // x ∈ MonoidHom.mrange f }

The first isomorphism theorem for monoids.

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivOfRightInverse.proof_2 {M : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ↑f) (x : P) :

↑(AddCon.kerLift f) ((AddCon.toQuotient ∘ g) x) = x

Equations

(_ : ↑(AddCon.kerLift f) ((AddCon.toQuotient ∘ g) x) = x) = (_ : ↑(AddCon.kerLift f) ((AddCon.toQuotient ∘ g) x) = x)

def AddCon.quotientKerEquivOfRightInverse.proof_3 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (x : AddCon.Quotient (AddCon.ker f)) (y : AddCon.Quotient (AddCon.ker f)) :

ZeroHom.toFun (↑(AddCon.kerLift f)) (x + y) = ZeroHom.toFun (↑(AddCon.kerLift f)) x + ZeroHom.toFun (↑(AddCon.kerLift f)) y

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivOfRightInverse.proof_1 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ↑f) (x : AddCon.Quotient (AddCon.ker f)) :

(AddCon.toQuotient ∘ g) (↑(AddCon.kerLift f) x) = x

Equations

(_ : (AddCon.toQuotient ∘ g) (↑(AddCon.kerLift f) x) = x) = (_ : (AddCon.toQuotient ∘ g) (↑(AddCon.kerLift f) x) = x)

def AddCon.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ↑f) :

AddCon.Quotient (AddCon.ker f) ≃+ P

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Con.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ↑f) :

∀ (a : P), ↑(MulEquiv.symm (Con.quotientKerEquivOfRightInverse f g hf)) a = (Con.toQuotient ∘ g) a

@[simp]

theorem AddCon.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ↑f) :

∀ (a : P), ↑(AddEquiv.symm (AddCon.quotientKerEquivOfRightInverse f g hf)) a = (AddCon.toQuotient ∘ g) a

@[simp]

theorem AddCon.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ↑f) (a : AddCon.Quotient (AddCon.ker f)) :

↑(AddCon.quotientKerEquivOfRightInverse f g hf) a = ↑(AddCon.kerLift f) a

@[simp]

theorem Con.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ↑f) (a : Con.Quotient (Con.ker f)) :

↑(Con.quotientKerEquivOfRightInverse f g hf) a = ↑(Con.kerLift f) a

def Con.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ↑f) :

Con.Quotient (Con.ker f) ≃* P

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientKerEquivOfSurjective.proof_1 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ↑f) :

Function.HasRightInverse ↑f

Equations

(_ : Function.HasRightInverse ↑f) = (_ : Function.HasRightInverse ↑f)

def AddCon.quotientKerEquivOfSurjective.proof_2 {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ↑f) :

Function.RightInverse (Exists.choose (_ : Function.HasRightInverse ↑f)) ↑f

Equations

(_ : Function.RightInverse (Exists.choose (_ : Function.HasRightInverse ↑f)) ↑f) = (_ : Function.RightInverse (Exists.choose (_ : Function.HasRightInverse ↑f)) ↑f)

noncomputable def AddCon.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ↑f) :

AddCon.Quotient (AddCon.ker f) ≃+ P

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

For a computable version, see add_con.quotient_ker_equiv_of_right_inverse.

Equations

One or more equations did not get rendered due to their size.

noncomputable def Con.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass P] (f : M →* P) (hf : Function.Surjective ↑f) :

Con.Quotient (Con.ker f) ≃* P

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

For a computable version, see con.quotientKerEquivOfRightOnverse.

Equations

One or more equations did not get rendered due to their size.

noncomputable def AddCon.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (c : AddCon M) (f : N →+ M) :

AddCon.Quotient (AddCon.comap ↑f (_ : ∀ (a b : N), ↑f (a + b) = ↑f a + ↑f b) c) ≃+ { x // x ∈ AddMonoidHom.mrange (AddMonoidHom.comp (AddCon.mk' c) f) }

The second isomorphism theorem for AddMonoids.

Equations

One or more equations did not get rendered due to their size.

noncomputable def Con.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (c : Con M) (f : N →* M) :

Con.Quotient (Con.comap ↑f (_ : ∀ (a b : N), ↑f (a * b) = ↑f a * ↑f b) c) ≃* { x // x ∈ MonoidHom.mrange (MonoidHom.comp (Con.mk' c) f) }

The second isomorphism theorem for monoids.

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientQuotientEquivQuotient.proof_3 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) (x : AddCon.Quotient (AddCon.ker (AddCon.map c d h))) (y : AddCon.Quotient (AddCon.ker (AddCon.map c d h))) :

Equiv.toFun { toFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun, invFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun, left_inv := (_ : Function.LeftInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun), right_inv := (_ : Function.RightInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun) } (x + y) = Equiv.toFun { toFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun, invFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun, left_inv := (_ : Function.LeftInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun), right_inv := (_ : Function.RightInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun) } x + Equiv.toFun { toFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun, invFun := (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun, left_inv := (_ : Function.LeftInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun), right_inv := (_ : Function.RightInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun) } y

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientQuotientEquivQuotient {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) :

AddCon.Quotient (AddCon.ker (AddCon.map c d h)) ≃+ AddCon.Quotient d

The third isomorphism theorem for AddMonoids.

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientQuotientEquivQuotient.proof_1 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) :

Function.LeftInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun

Equations

One or more equations did not get rendered due to their size.

def AddCon.quotientQuotientEquivQuotient.proof_2 {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) :

Function.RightInverse (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).invFun (Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h).toFun

Equations

One or more equations did not get rendered due to their size.

def Con.quotientQuotientEquivQuotient {M : Type u_1} [inst : MulOneClass M] (c : Con M) (d : Con M) (h : c ≤ d) :

Con.Quotient (Con.ker (Con.map c d h)) ≃* Con.Quotient d

The third isomorphism theorem for monoids.

Equations

One or more equations did not get rendered due to their size.

theorem AddCon.nsmul {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) (n : ℕ) {w : M} {x : M} :

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

Additive congruence relations preserve natural scaling.

abbrev AddCon.nsmul.match_1 {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) (motive : ℕ → (x x_1 : M) → ↑c x x_1 → Prop) :

(x : ℕ) → (x_1 x_2 : M) → (x_3 : ↑c x_1 x_2) → ((w x : M) → (x_4 : ↑c w x) → motive 0 w x x_4) → ((n : ℕ) → (w x : M) → (h : ↑c w x) → motive (Nat.succ n) w x h) → motive x x_1 x_2 x_3

Equations

AddCon.nsmul.match_1 c motive x x x x h_1 h_2 = Nat.casesOn x (h_1 x x x) fun n => h_2 n x x x

theorem Con.pow {M : Type u_1} [inst : Monoid M] (c : Con M) (n : ℕ) {w : M} {x : M} :

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

Multiplicative congruence relations preserve natural powers.

instance AddCon.instZeroQuotientToAdd {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M) :

Zero (AddCon.Quotient c)

Equations

AddCon.instZeroQuotientToAdd c = { zero := ↑0 }

instance Con.instOneQuotientToMul {M : Type u_1} [inst : MulOneClass M] (c : Con M) :

One (Con.Quotient c)

Equations

Con.instOneQuotientToMul c = { one := ↑1 }

theorem AddCon.vadd {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] [inst : VAdd α M] [inst : VAddAssocClass α M M] (c : AddCon M) (a : α) {w : M} {x : M} (h : ↑c w x) :

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

theorem Con.smul {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] [inst : SMul α M] [inst : IsScalarTower α M M] (c : Con M) (a : α) {w : M} {x : M} (h : ↑c w x) :

↑c (a • w) (a • x)

instance AddCon.Quotient.nsmul {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

SMul ℕ (AddCon.Quotient c)

Equations

AddCon.Quotient.nsmul c = { smul := fun n => Quotient.map' ((fun x x_1 => x • x_1) n) (AddCon.Quotient.nsmul.proof_1 c n) }

instance Con.instPowQuotientToMulToMulOneClassNat {M : Type u_1} [inst : Monoid M] (c : Con M) :

Pow (Con.Quotient c) ℕ

Equations

Con.instPowQuotientToMulToMulOneClassNat c = { pow := fun x n => Quotient.map' (fun x => x ^ n) (Con.instPowQuotientToMulToMulOneClassNat.proof_1 c n) x }

def AddCon.addSemigroup.proof_2 {M : Type u_1} [inst : AddSemigroup M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1)

Equations

(_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x)) = (_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x))

def AddCon.addSemigroup.proof_1 {M : Type u_1} [inst : AddSemigroup M] (c : AddCon M) :

Function.Surjective Quotient.mk''

Equations

(_ : Function.Surjective Quotient.mk'') = (_ : Function.Surjective Quotient.mk'')

instance AddCon.addSemigroup {M : Type u_1} [inst : AddSemigroup M] (c : AddCon M) :

AddSemigroup (AddCon.Quotient c)

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

Equations

AddCon.addSemigroup c = Function.Surjective.addSemigroup Quotient.mk'' (_ : Function.Surjective Quotient.mk'') (_ : ∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))

instance Con.semigroup {M : Type u_1} [inst : Semigroup M] (c : Con M) :

Semigroup (Con.Quotient c)

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

Equations

Con.semigroup c = Function.Surjective.semigroup Quotient.mk'' (_ : Function.Surjective Quotient.mk'') (_ : ∀ (x x_1 : M), Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))

instance AddCon.addCommSemigroup {M : Type u_1} [inst : AddCommSemigroup M] (c : AddCon M) :

AddCommSemigroup (AddCon.Quotient c)

The quotient of an AddCommSemigroup by an additive congruence relation is an AddSemigroup.

Equations

AddCon.addCommSemigroup c = Function.Surjective.addCommSemigroup Quotient.mk'' (_ : Function.Surjective Quotient.mk'') (_ : ∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))

def AddCon.addCommSemigroup.proof_1 {M : Type u_1} [inst : AddCommSemigroup M] (c : AddCon M) :

Function.Surjective Quotient.mk''

Equations

(_ : Function.Surjective Quotient.mk'') = (_ : Function.Surjective Quotient.mk'')

def AddCon.addCommSemigroup.proof_2 {M : Type u_1} [inst : AddCommSemigroup M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1)

Equations

(_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x)) = (_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x))

instance Con.commSemigroup {M : Type u_1} [inst : CommSemigroup M] (c : Con M) :

CommSemigroup (Con.Quotient c)

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

Equations

Con.commSemigroup c = Function.Surjective.commSemigroup Quotient.mk'' (_ : Function.Surjective Quotient.mk'') (_ : ∀ (x x_1 : M), Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))

def AddCon.addMonoid.proof_3 {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1)

Equations

(_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x)) = (_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x))

def AddCon.addMonoid.proof_2 {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

Quotient.mk'' 0 = Quotient.mk'' 0

Equations

(_ : Quotient.mk'' 0 = Quotient.mk'' 0) = (_ : Quotient.mk'' 0 = Quotient.mk'' 0)

def AddCon.addMonoid.proof_1 {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

Function.Surjective Quotient.mk''

Equations

(_ : Function.Surjective Quotient.mk'') = (_ : Function.Surjective Quotient.mk'')

instance AddCon.addMonoid {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

AddMonoid (AddCon.Quotient c)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.addMonoid.proof_4 {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) :

∀ (x : M) (x_1 : ℕ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x)

Equations

(_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x)) = (_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x))

instance Con.monoid {M : Type u_1} [inst : Monoid M] (c : Con M) :

Monoid (Con.Quotient c)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.addCommMonoid.proof_2 {M : Type u_1} [inst : AddCommMonoid M] (c : AddCon M) :

Quotient.mk'' 0 = Quotient.mk'' 0

Equations

(_ : Quotient.mk'' 0 = Quotient.mk'' 0) = (_ : Quotient.mk'' 0 = Quotient.mk'' 0)

def AddCon.addCommMonoid.proof_3 {M : Type u_1} [inst : AddCommMonoid M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1)

Equations

(_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x)) = (_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x))

def AddCon.addCommMonoid.proof_4 {M : Type u_1} [inst : AddCommMonoid M] (c : AddCon M) :

∀ (x : M) (x_1 : ℕ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x)

Equations

(_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x)) = (_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x))

instance AddCon.addCommMonoid {M : Type u_1} [inst : AddCommMonoid M] (c : AddCon M) :

AddCommMonoid (AddCon.Quotient c)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.addCommMonoid.proof_1 {M : Type u_1} [inst : AddCommMonoid M] (c : AddCon M) :

Function.Surjective Quotient.mk''

Equations

(_ : Function.Surjective Quotient.mk'') = (_ : Function.Surjective Quotient.mk'')

instance Con.commMonoid {M : Type u_1} [inst : CommMonoid M] (c : Con M) :

CommMonoid (Con.Quotient c)

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

Equations

One or more equations did not get rendered due to their size.

theorem AddCon.neg {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {w : M} {x : M} :

↑c w x → ↑c (-w) (-x)

Additive congruence relations preserve negation.

theorem Con.inv {M : Type u_1} [inst : Group M] (c : Con M) {w : M} {x : M} :

↑c w x → ↑c w⁻¹ x⁻¹

Multiplicative congruence relations preserve inversion.

theorem AddCon.sub {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {w : M} {x : M} {y : M} {z : M} :

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

Additive congruence relations preserve subtraction.

theorem Con.div {M : Type u_1} [inst : Group M] (c : Con M) {w : M} {x : M} {y : M} {z : M} :

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

Multiplicative congruence relations preserve division.

theorem AddCon.zsmul {M : Type u_1} [inst : AddGroup M] (c : AddCon M) (n : ℤ) {w : M} {x : M} :

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

Additive congruence relations preserve integer scaling.

abbrev AddCon.zsmul.match_1 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) (motive : ℤ → (x x_1 : M) → ↑c x x_1 → Prop) :

(x : ℤ) → (x_1 x_2 : M) → (x_3 : ↑c x_1 x_2) → ((n : ℕ) → (w x : M) → (h : ↑c w x) → motive (Int.ofNat n) w x h) → ((n : ℕ) → (w x : M) → (h : ↑c w x) → motive (Int.negSucc n) w x h) → motive x x_1 x_2 x_3

Equations

AddCon.zsmul.match_1 c motive x x x x h_1 h_2 = Int.casesOn x (fun a => h_1 a x x x) fun a => h_2 a x x x

theorem Con.zpow {M : Type u_1} [inst : Group M] (c : Con M) (n : ℤ) {w : M} {x : M} :

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

Multiplicative congruence relations preserve integer powers.

instance AddCon.hasNeg {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

Neg (AddCon.Quotient c)

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

Equations

AddCon.hasNeg c = { neg := Quotient.map' Neg.neg (AddCon.hasNeg.proof_1 c) }

def AddCon.hasNeg.proof_1 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

(x x_1 : M) → ↑c x x_1 → ↑c (-x) (-x_1)

Equations

(_ : ↑c x x → ↑c (-x) (-x)) = (_ : ↑c x x → ↑c (-x) (-x))

instance Con.hasInv {M : Type u_1} [inst : Group M] (c : Con M) :

Inv (Con.Quotient c)

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

Equations

Con.hasInv c = { inv := Quotient.map' Inv.inv (Con.hasInv.proof_1 c) }

def AddCon.hasSub.proof_1 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

(x x_1 : M) → Setoid.r x x_1 → (x_2 x_3 : M) → Setoid.r x_2 x_3 → ↑c (x - x_2) (x_1 - x_3)

Equations

(_ : ↑c (x - x) (x - x)) = (_ : ↑c (x - x) (x - x))

instance AddCon.hasSub {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

Sub (AddCon.Quotient c)

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

Equations

AddCon.hasSub c = { sub := Quotient.map₂' (fun x x_1 => x - x_1) (AddCon.hasSub.proof_1 c) }

instance Con.hasDiv {M : Type u_1} [inst : Group M] (c : Con M) :

Div (Con.Quotient c)

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

Equations

Con.hasDiv c = { div := Quotient.map₂' (fun x x_1 => x / x_1) (Con.hasDiv.proof_1 c) }

instance AddCon.Quotient.zsmul {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

SMul ℤ (AddCon.Quotient c)

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

Equations

AddCon.Quotient.zsmul c = { smul := fun z => Quotient.map' ((fun x x_1 => x • x_1) z) (AddCon.Quotient.zsmul.proof_1 c z) }

instance Con.zpowinst {M : Type u_1} [inst : Group M] (c : Con M) :

Pow (Con.Quotient c) ℤ

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

Equations

Con.zpowinst c = { pow := fun x z => Quotient.map' (fun x => x ^ z) (Con.zpowinst.proof_1 c z) x }

def AddCon.addGroup.proof_1 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

Function.Surjective Quotient.mk''

Equations

(_ : Function.Surjective Quotient.mk'') = (_ : Function.Surjective Quotient.mk'')

def AddCon.addGroup.proof_5 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x - x_1) = Quotient.mk'' (x - x_1)

Equations

(_ : Quotient.mk'' (x - x) = Quotient.mk'' (x - x)) = (_ : Quotient.mk'' (x - x) = Quotient.mk'' (x - x))

def AddCon.addGroup.proof_3 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

∀ (x x_1 : M), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1)

Equations

(_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x)) = (_ : Quotient.mk'' (x + x) = Quotient.mk'' (x + x))

def AddCon.addGroup.proof_4 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

∀ (x : M), Quotient.mk'' (-x) = Quotient.mk'' (-x)

Equations

(_ : Quotient.mk'' (-x) = Quotient.mk'' (-x)) = (_ : Quotient.mk'' (-x) = Quotient.mk'' (-x))

def AddCon.addGroup.proof_7 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

∀ (x : M) (x_1 : ℤ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x)

Equations

(_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x)) = (_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x))

def AddCon.addGroup.proof_2 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

Quotient.mk'' 0 = Quotient.mk'' 0

Equations

(_ : Quotient.mk'' 0 = Quotient.mk'' 0) = (_ : Quotient.mk'' 0 = Quotient.mk'' 0)

instance AddCon.addGroup {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

AddGroup (AddCon.Quotient c)

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

Equations

One or more equations did not get rendered due to their size.

def AddCon.addGroup.proof_6 {M : Type u_1} [inst : AddGroup M] (c : AddCon M) :

∀ (x : M) (x_1 : ℕ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x)

Equations

(_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x)) = (_ : Quotient.mk'' (x • x) = Quotient.mk'' (x • x))

instance Con.group {M : Type u_1} [inst : Group M]