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
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
A congruence relation on a type with an addition is an equivalence relation which preserves addition.
- r : M → M → Prop
- iseqv : Equivalence ⇑self.toSetoid
Additive congruence relations are closed under addition
Instances For
A congruence relation on a type with a multiplication is an equivalence relation which preserves multiplication.
- r : M → M → Prop
- iseqv : Equivalence ⇑self.toSetoid
Congruence relations are closed under multiplication
Instances For
The inductively defined smallest additive congruence relation containing a given binary relation.
- 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)
Instances For
The inductively defined smallest multiplicative congruence relation containing a given binary relation.
- 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)
Instances For
Additive congruence relations are reflexive.
Additive congruence relations are symmetric.
Additive congruence relations are transitive.
Given a type M
with an addition, x, y ∈ M
, and an additive congruence relation
c
on M
, (x, y) ∈ M × M
iff x
is related to y
by c
.
Given a type M
with a multiplication, a congruence relation c
on M
, and elements of M
x, y
, (x, y) ∈ M × M
iff x
is related to y
by c
.
The kernel of an addition-preserving function as an additive congruence relation.
Equations
- AddCon.addKer f h = { toSetoid := Setoid.ker f, add' := ⋯ }
Instances For
The kernel of a multiplication-preserving function as a congruence relation.
Equations
- Con.mulKer f h = { toSetoid := Setoid.ker f, mul' := ⋯ }
Instances For
Given types with additions M, N
, the product of two congruence relations
c
on M
and d
on N
: (x₁, x₂), (y₁, y₂) ∈ M × N
are related by c.prod d
iff x₁
is related to y₁
by c
and x₂
is related to y₂
by d
.
Equations
- c.prod d = { toSetoid := c.prod d.toSetoid, add' := ⋯ }
Instances For
The quotient by a decidable additive congruence relation has decidable equality.
Equations
- c.instDecidableEqQuotientOfDecidableCoeForallProp = inferInstanceAs (DecidableEq (Quotient c.toSetoid))
The quotient by a decidable congruence relation has decidable equality.
Equations
- c.instDecidableEqQuotientOfDecidableCoeForallProp = inferInstanceAs (DecidableEq (Quotient c.toSetoid))
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
Instances For
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
Instances For
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
Instances For
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
Instances For
A version of Quotient.hrecOn₂'
for quotients by AddCon
.
Equations
- AddCon.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h
Instances For
A version of Quotient.hrecOn₂'
for quotients by Con
.
Equations
- Con.hrecOn₂ a b f h = Quotient.hrecOn₂' a b f h
Instances For
A version of AddCon.induction_on
for predicates which take
two arguments.
A version of Con.induction_on
for predicates which take two arguments.
The addition induced on the quotient by an additive congruence relation on a type with an addition.
Equations
- c.hasAdd = { add := Quotient.map₂' (fun (x1 x2 : M) => x1 + x2) ⋯ }
The multiplication induced on the quotient by a congruence relation on a type with a multiplication.
Equations
- c.hasMul = { mul := Quotient.map₂' (fun (x1 x2 : M) => x1 * x2) ⋯ }
The kernel of the quotient map induced by an additive congruence
relation c
equals c
.
The kernel of the quotient map induced by a congruence relation c
equals c
.
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.
Definition of the function on the quotient by a congruence relation c
induced by a function
that is constant on c
's equivalence classes.
Makes an additive isomorphism of quotients by two additive congruence relations, given that the relations are equal.
Equations
- AddCon.congr h = { toEquiv := Quotient.congr (Equiv.refl M) ⋯, map_add' := ⋯ }
Instances For
Equations
- AddCon.instPartialOrder = PartialOrder.mk ⋯
Equations
- Con.instPartialOrder = PartialOrder.mk ⋯
The complete lattice of additive congruence relations on a given type with an addition.
Equations
- AddCon.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The complete lattice of congruence relations on a given type with a multiplication.
Equations
- Con.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The inductively defined smallest additive congruence relation
containing a binary relation r
equals the infimum of the set of additive congruence relations
containing r
.
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
.
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
'.
The supremum of a set of additive congruence relations S
equals
the smallest additive congruence relation containing the binary relation 'there exists c ∈ S
such that x
is related to y
by c
'.
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.
There is a Galois insertion of additive congruence relations on a type with
an addition M
into binary relations on M
.
Equations
Instances For
There is a Galois insertion of congruence relations on a type with a multiplication M
into
binary relations on M
.
Equations
Instances For
Given a function f
, the smallest additive congruence relation containing the
binary relation on f
's image defined by 'x ≈ y
iff the elements of f⁻¹(x)
are related to the
elements of f⁻¹(y)
by an additive congruence relation c
.'
Instances For
Given a function f
, the smallest congruence relation containing the binary relation on f
's
image defined by 'x ≈ y
iff the elements of f⁻¹(x)
are related to the elements of f⁻¹(y)
by a congruence relation c
.'
Instances For
Given a surjective addition-preserving function f
whose kernel is contained in
an additive congruence relation c
, the additive congruence relation on f
's codomain defined
by 'x ≈ y
iff the elements of f⁻¹(x)
are related to the elements of f⁻¹(y)
by c
.'
Equations
- c.mapOfSurjective f H h hf = { toSetoid := c.mapOfSurjective f h hf, add' := ⋯ }
Instances For
Given a surjective multiplicative-preserving function f
whose kernel is contained in a
congruence relation c
, the congruence relation on f
's codomain defined by 'x ≈ y
iff the
elements of f⁻¹(x)
are related to the elements of f⁻¹(y)
by c
.'
Equations
- c.mapOfSurjective f H h hf = { toSetoid := c.mapOfSurjective f h hf, mul' := ⋯ }
Instances For
A specialization of 'the smallest additive congruence relation containing
an additive congruence relation c
equals c
'.
A specialization of 'the smallest congruence relation containing a congruence relation c
equals c
'.
Given types with additions M, N
and an additive congruence relation c
on N
,
an addition-preserving map f : M → N
induces an additive congruence relation on f
's domain
defined by 'x ≈ y
iff f(x)
is related to f(y)
by c
.'
Equations
- AddCon.comap f H c = { toSetoid := Setoid.comap f c.toSetoid, add' := ⋯ }
Instances For
Given types with multiplications M, N
and a congruence relation c
on N
, a
multiplication-preserving map f : M → N
induces a congruence relation on f
's domain
defined by 'x ≈ y
iff f(x)
is related to f(y)
by c
.'
Equations
- Con.comap f H c = { toSetoid := Setoid.comap f c.toSetoid, mul' := ⋯ }
Instances For
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.
Instances For
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.
Instances For
The quotient of an AddMonoid
by an additive congruence relation is
an AddMonoid
.
Equations
- c.addZeroClass = AddZeroClass.mk ⋯ ⋯
The quotient of a monoid by a congruence relation is a monoid.
Equations
- c.mulOneClass = MulOneClass.mk ⋯ ⋯
The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the monoid's 1.
The AddSubmonoid
of M × M
defined by an additive congruence
relation on an AddMonoid
M
.
Instances For
The submonoid of M × M
defined by a congruence relation on a monoid M
.
Instances For
The additive congruence relation on an AddMonoid
M
from
an AddSubmonoid
of M × M
for which membership is an equivalence relation.
Equations
- AddCon.ofAddSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, add' := ⋯ }
Instances For
The congruence relation on a monoid M
from a submonoid of M × M
for which membership
is an equivalence relation.
Equations
- Con.ofSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, mul' := ⋯ }
Instances For
Coercion from a congruence relation c
on an AddMonoid
M
to the AddSubmonoid
of M × M
whose elements are (x, y)
such that x
is related to y
by c
.
Coercion from a congruence relation c
on a monoid M
to the submonoid of M × M
whose
elements are (x, y)
such that x
is related to y
by c
.
The kernel of an AddMonoid
homomorphism as an additive congruence relation.
Equations
- AddCon.ker f = AddCon.addKer ⇑f ⋯
Instances For
The kernel of a monoid homomorphism as a congruence relation.
Equations
- Con.ker f = Con.mulKer ⇑f ⋯
Instances For
The definition of the additive congruence relation defined by an
AddMonoid
homomorphism's kernel.
The definition of the congruence relation defined by a monoid homomorphism's kernel.
There exists an element of the quotient of an AddMonoid
by a congruence relation
(namely 0).
Equations
- AddCon.Quotient.inhabited = { default := ↑0 }
There exists an element of the quotient of a monoid by a congruence relation (namely 1).
Equations
- Con.Quotient.inhabited = { default := ↑1 }
The kernel of the natural homomorphism from an AddMonoid
to its
quotient by an additive congruence relation c
equals c
.
The kernel of the natural homomorphism from a monoid to its quotient by a congruence
relation c
equals c
.
The natural homomorphism from an AddMonoid
to its quotient by a congruence
relation is surjective.
The natural homomorphism from a monoid to its quotient by a congruence relation is surjective.
Given an AddMonoid
homomorphism f : N → M
and an additive congruence relation
c
on M
, the additive congruence relation induced on N
by f
equals the kernel of c
's
quotient homomorphism composed with f
.
Given a monoid homomorphism f : N → M
and a congruence relation c
on M
, the congruence
relation induced on N
by f
equals the kernel of c
's quotient homomorphism composed with
f
.
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
- c.lift f H = { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The homomorphism on the quotient of a monoid by a congruence relation c
induced by a
homomorphism constant on c
's equivalence classes.
Equations
- c.lift f H = { toFun := fun (x : c.Quotient) => Con.liftOn x ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The diagram describing the universal property for quotients of AddMonoid
s
commutes.
The diagram describing the universal property for quotients of monoids commutes.
The diagram describing the universal property for quotients of
AddMonoid
s commutes.
The diagram describing the universal property for quotients of monoids commutes.
The diagram describing the universal property for quotients of
AddMonoid
s commutes.
The diagram describing the universal property for quotients of monoids commutes.
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.
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.
Homomorphisms on the quotient of an AddMonoid
by an additive congruence relation
are equal if they are equal on elements that are coercions from the AddMonoid
.
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.
The uniqueness part of the universal property for quotients of AddMonoid
s.
The uniqueness part of the universal property for quotients of monoids.
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.
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.
Surjective AddMonoid
homomorphisms constant on an additive congruence
relation c
's equivalence classes induce a surjective homomorphism on c
's quotient.
Surjective monoid homomorphisms constant on a congruence relation c
's equivalence classes
induce a surjective homomorphism on c
's quotient.
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.
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.
The homomorphism induced on the quotient of an AddMonoid
by the kernel
of an AddMonoid
homomorphism.
Equations
- AddCon.kerLift f = (AddCon.ker f).lift f ⋯
Instances For
The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.
Equations
- Con.kerLift f = (Con.ker f).lift f ⋯
Instances For
The diagram described by the universal property for quotients
of AddMonoid
s, when the additive congruence relation is the kernel of the homomorphism,
commutes.
The diagram described by the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, commutes.
Given an AddMonoid
homomorphism f
, the induced homomorphism
on the quotient by f
's kernel has the same image as f
.
Given a monoid homomorphism f
, the induced homomorphism on the quotient by f
's kernel has
the same image as f
.
An AddMonoid
homomorphism f
induces an injective homomorphism on the quotient
by f
's kernel.
A monoid homomorphism f
induces an injective homomorphism on the quotient by f
's kernel.
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
- c.map d h = c.lift d.mk' ⋯
Instances For
Given congruence relations c, d
on a monoid such that d
contains c
, d
's quotient
map induces a homomorphism from the quotient by c
to the quotient by d
.
Equations
- c.map d h = c.lift d.mk' ⋯
Instances For
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.
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.
The first isomorphism theorem for AddMonoid
s.
Equations
- AddCon.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) ⋯, map_add' := ⋯ }
Instances For
The first isomorphism theorem for monoids.
Equations
- Con.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((MulEquiv.submonoidCongr ⋯).toMonoidHom.comp (Con.kerLift f).mrangeRestrict) ⋯, map_mul' := ⋯ }
Instances For
The first isomorphism theorem for AddMonoid
s in the case of a homomorphism
with right inverse.
Equations
- AddCon.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(AddCon.kerLift f), invFun := AddCon.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.
Equations
- Con.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(Con.kerLift f), invFun := Con.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
The first isomorphism theorem for AddMonoid
s in the case of a surjective
homomorphism.
For a computable
version, see AddCon.quotientKerEquivOfRightInverse
.
Equations
Instances For
The first isomorphism theorem for Monoids in the case of a surjective homomorphism.
For a computable
version, see Con.quotientKerEquivOfRightInverse
.
Equations
Instances For
The second isomorphism theorem for AddMonoid
s.
Equations
- c.comapQuotientEquiv f = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivRange (c.mk'.comp f))
Instances For
The second isomorphism theorem for monoids.
Equations
- c.comapQuotientEquiv f = (Con.congr ⋯).trans (Con.quotientKerEquivRange (c.mk'.comp f))
Instances For
The third isomorphism theorem for AddMonoid
s.
Equations
- c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_add' := ⋯ }
Instances For
The third isomorphism theorem for monoids.
Equations
- c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_mul' := ⋯ }
Instances For
Equations
- c.zero = { zero := Quotient.mk'' 0 }
Equations
- c.one = { one := Quotient.mk'' 1 }
Equations
- AddCon.Quotient.nsmul c = { smul := fun (n : ℕ) => Quotient.map' (fun (x : M) => n • x) ⋯ }
The quotient of an AddSemigroup
by an additive congruence relation is
an AddSemigroup
.
Equations
- c.addSemigroup = AddSemigroup.mk ⋯
The quotient of a semigroup by a congruence relation is a semigroup.
Equations
- c.semigroup = Semigroup.mk ⋯
The quotient of an AddCommSemigroup
by an additive congruence relation is
an AddCommSemigroup
.
Equations
- c.addCommSemigroup = AddCommSemigroup.mk ⋯
The quotient of a commutative semigroup by a congruence relation is a semigroup.
Equations
- c.commSemigroup = CommSemigroup.mk ⋯
The quotient of an AddMonoid
by an additive congruence relation is
an AddMonoid
.
Equations
- c.addMonoid = AddMonoid.mk ⋯ ⋯ AddMonoid.nsmul ⋯ ⋯
The quotient of an AddCommMonoid
by an additive congruence
relation is an AddCommMonoid
.
Equations
- c.addCommMonoid = AddCommMonoid.mk ⋯
The quotient of a CommMonoid
by a congruence relation is a CommMonoid
.
Equations
- c.commMonoid = CommMonoid.mk ⋯
Sometimes, an additive group is defined as a quotient of a monoid
by an additive congruence relation.
Usually, the inverse operation is defined as Setoid.map f _
for some f
.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both ∀ x y, c x y → c (f x) (f y)
(to define the operation)
and ∀ x, c (f x + x) 0
(to prove the group laws), one can only prove the latter.
Sometimes, a group is defined as a quotient of a monoid by a congruence relation.
Usually, the inverse operation is defined as Setoid.map f _
for some f
.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both ∀ x y, c x y → c (f x) (f y)
(to define the operation)
and ∀ x, c (f x * x) 1
(to prove the group laws), one can only prove the latter.
The negation induced on the quotient by an additive congruence relation on a type with a negation.
Equations
- c.hasNeg = { neg := Quotient.map' Neg.neg ⋯ }
The inversion induced on the quotient by a congruence relation on a type with an inversion.
Equations
- c.hasInv = { inv := Quotient.map' Inv.inv ⋯ }
The subtraction induced on the quotient by an additive congruence relation on a type with a subtraction.
Equations
- c.hasSub = { sub := Quotient.map₂' (fun (x1 x2 : M) => x1 - x2) ⋯ }
The division induced on the quotient by a congruence relation on a type with a division.
Equations
- c.hasDiv = { div := Quotient.map₂' (fun (x1 x2 : M) => x1 / x2) ⋯ }
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 : M) => z • x) ⋯ }
The quotient of an AddGroup
by an additive congruence relation is
an AddGroup
.
Equations
- c.addGroup = AddGroup.mk ⋯
In order to define a function (Con.Quotient c)ˣ → α
on the units of Con.Quotient c
,
where c : Con M
is a multiplicative congruence on a monoid, it suffices to define a function f
that takes elements x y : M
with proofs of c (x * y) 1
and c (y * x) 1
, and returns an element
of α
provided that f x y _ _ = f x' y' _ _
whenever c x x'
and c y y'
.
Equations
- AddCon.liftOnAddUnits u f Hf = AddCon.hrecOn₂ (↑u) (↑(-u)) (fun (x y : M) (hxy : ↑x + ↑y = 0) (hyx : ↑y + ↑x = 0) => f x y ⋯ ⋯) ⋯ ⋯ ⋯
Instances For
In order to define a function (Con.Quotient c)ˣ → α
on the units of Con.Quotient c
,
where c : Con M
is a multiplicative congruence on a monoid, it suffices to define a function f
that takes elements x y : M
with proofs of c (x * y) 1
and c (y * x) 1
, and returns an element
of α
provided that f x y _ _ = f x' y' _ _
whenever c x x'
and c y y'
.
Equations
- Con.liftOnUnits u f Hf = Con.hrecOn₂ (↑u) (↑u⁻¹) (fun (x y : M) (hxy : ↑x * ↑y = 1) (hyx : ↑y * ↑x = 1) => f x y ⋯ ⋯) ⋯ ⋯ ⋯
Instances For
Equations
- c.instVAdd = { vadd := fun (a : α) => Quotient.map' (fun (x : M) => a +ᵥ x) ⋯ }
Equations
- c.instSMul = { smul := fun (a : α) => Quotient.map' (fun (x : M) => a • x) ⋯ }
Equations
- c.addAction = AddAction.mk ⋯ ⋯
Equations
- c.mulAction = MulAction.mk ⋯ ⋯
Equations
- c.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯