Lifting algebraic data classes along injective/surjective maps
This file provides definitions that are meant to deal with situations such as the following:
Suppose that G
is a group, and H
is a type endowed with
has_one H
, has_mul H
, and has_inv H
.
Suppose furthermore, that f : G → H
is a surjective map
that respects the multiplication, and the unit elements.
Then H
satisfies the group axioms.
The relevant definition in this case is function.surjective.group
.
Dually, there is also function.injective.group
.
And there are versions for (additive) (commutative) semigroups/monoids.
Injective
A type endowed with *
is a semigroup,
if it admits an injective map that preserves *
to a semigroup.
Equations
- function.injective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}
A type endowed with +
is an additive semigroup,
if it admits an injective map that preserves +
to an additive semigroup.
A type endowed with +
is an additive commutative semigroup,
if it admits an injective map that preserves +
to an additive commutative semigroup.
A type endowed with *
is a commutative semigroup,
if it admits an injective map that preserves *
to a commutative semigroup.
Equations
- function.injective.comm_semigroup f hf mul = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, mul_comm := _}
A type endowed with *
is a left cancel semigroup,
if it admits an injective map that preserves *
to a left cancel semigroup.
Equations
- function.injective.left_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_left_cancel := _}
A type endowed with +
is an additive left cancel semigroup,
if it admits an injective map that preserves +
to an additive left cancel semigroup.
A type endowed with *
is a right cancel semigroup,
if it admits an injective map that preserves *
to a right cancel semigroup.
Equations
- function.injective.right_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_right_cancel := _}
A type endowed with +
is an additive right cancel semigroup,
if it admits an injective map that preserves +
to an additive right cancel semigroup.
A type endowed with 0
and +
is an additive monoid,
if it admits an injective map that preserves 0
and +
to an additive monoid.
A type endowed with 1
and *
is a monoid,
if it admits an injective map that preserves 1
and *
to a monoid.
Equations
- function.injective.monoid f hf one mul = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, one := 1, one_mul := _, mul_one := _}
A type endowed with 1
and *
is a left cancel monoid,
if it admits an injective map that preserves 1
and *
to a left cancel monoid.
Equations
- function.injective.left_cancel_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _}
A type endowed with 0
and +
is an additive left cancel monoid,
if it admits an injective map that preserves 0
and +
to an additive left cancel monoid.
A type endowed with 0
and +
is an additive commutative monoid,
if it admits an injective map that preserves 0
and +
to an additive commutative monoid.
A type endowed with 1
and *
is a commutative monoid,
if it admits an injective map that preserves 1
and *
to a commutative monoid.
Equations
- function.injective.comm_monoid f hf one mul = {mul := comm_semigroup.mul (function.injective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _}
A type endowed with 0
, +
, unary -
, and binary -
is a sub_neg_monoid
if it admits an injective map that preserves 0
, +
, unary -
, and binary -
to
a sub_neg_monoid
.
A type endowed with 1
, *
, ⁻¹
, and /
is a div_inv_monoid
if it admits an injective map that preserves 1
, *
, ⁻¹
, and /
to a div_inv_monoid
.
Equations
- function.injective.div_inv_monoid f hf one mul inv div = {mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, inv := has_inv.inv _inst_3, div := has_div.div _inst_4, div_eq_mul_inv := _}
A type endowed with 1
, *
and ⁻¹
is a group,
if it admits an injective map that preserves 1
, *
and ⁻¹
to a group.
Equations
- function.injective.group f hf one mul inv = {mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, inv := has_inv.inv _inst_3, div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ has_inv.inv, div_eq_mul_inv := _, mul_left_inv := _}
A type endowed with 0
and +
is an additive group,
if it admits an injective map that preserves 0
and +
to an additive group.
A type endowed with 0
, +
and -
(unary and binary) is an additive group,
if it admits an injective map to an additive group that preserves these operations.
This version of injective.add_group
makes sure that the -
operation is defeq
to the specified subtraction operator.
A type endowed with 1
, *
, ⁻¹
and /
is a group,
if it admits an injective map to a group that preserves these operations.
This version of injective.group
makes sure that the /
operation is defeq
to the specified division operator.
Equations
- function.injective.group_div f hf one mul inv div = {mul := div_inv_monoid.mul (function.injective.div_inv_monoid f hf one mul inv div), mul_assoc := _, one := div_inv_monoid.one (function.injective.div_inv_monoid f hf one mul inv div), one_mul := _, mul_one := _, inv := div_inv_monoid.inv (function.injective.div_inv_monoid f hf one mul inv div), div := div_inv_monoid.div (function.injective.div_inv_monoid f hf one mul inv div), div_eq_mul_inv := _, mul_left_inv := _}
A type endowed with 1
, *
and ⁻¹
is a commutative group,
if it admits an injective map that preserves 1
, *
and ⁻¹
to a commutative group.
Equations
- function.injective.comm_group f hf one mul inv = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, inv := group.inv (function.injective.group f hf one mul inv), div := group.div (function.injective.group f hf one mul inv), div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}
A type endowed with 0
and +
is an additive commutative group,
if it admits an injective map that preserves 0
and +
to an additive commutative group.
A type endowed with 1
, *
, ⁻¹
and /
is a commutative group,
if it admits an injective map to a commutative group that preserves these operations.
This version of injective.comm_group
makes sure that the /
operation is defeq
to the specified division operator.
Equations
- function.injective.comm_group_div f hf one mul inv div = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, inv := group.inv (function.injective.group_div f hf one mul inv div), div := group.div (function.injective.group_div f hf one mul inv div), div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}
A type endowed with 0
, +
and -
is an additive commutative group,
if it admits an injective map to an additive commutative group that preserves these operations.
This version of injective.add_comm_group
makes sure that the -
operation is defeq
to the specified subtraction operator.
Surjective
A type endowed with +
is an additive semigroup,
if it admits a surjective map that preserves +
from an additive semigroup.
A type endowed with *
is a semigroup,
if it admits a surjective map that preserves *
from a semigroup.
Equations
- function.surjective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}
A type endowed with *
is a commutative semigroup,
if it admits a surjective map that preserves *
from a commutative semigroup.
Equations
- function.surjective.comm_semigroup f hf mul = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, mul_comm := _}
A type endowed with +
is an additive commutative semigroup,
if it admits a surjective map that preserves +
from an additive commutative semigroup.
A type endowed with 1
and *
is a monoid,
if it admits a surjective map that preserves 1
and *
from a monoid.
Equations
- function.surjective.monoid f hf one mul = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, one := 1, one_mul := _, mul_one := _}
A type endowed with 0
and +
is an additive monoid,
if it admits a surjective map that preserves 0
and +
to an additive monoid.
A type endowed with 0
and +
is an additive commutative monoid,
if it admits a surjective map that preserves 0
and +
to an additive commutative monoid.
A type endowed with 1
and *
is a commutative monoid,
if it admits a surjective map that preserves 1
and *
from a commutative monoid.
Equations
- function.surjective.comm_monoid f hf one mul = {mul := comm_semigroup.mul (function.surjective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _}
A type endowed with 1
, *
and ⁻¹
is a group,
if it admits a surjective map that preserves 1
, *
and ⁻¹
from a group.
Equations
- function.surjective.group f hf one mul inv = {mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, inv := has_inv.inv _inst_3, div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ has_inv.inv, div_eq_mul_inv := _, mul_left_inv := _}
A type endowed with 0
, +
, and unary -
is an additive group,
if it admits a surjective map that preserves 0
, +
, and -
from an additive group.
A type endowed with 1
, *
, ⁻¹
, and /
is a div_inv_monoid
,
if it admits a surjective map that preserves 1
, *
, ⁻¹
, and /
from a div_inv_monoid
Equations
- function.surjective.div_inv_monoid f hf one mul inv div = {mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, inv := has_inv.inv _inst_3, div := has_div.div _inst_4, div_eq_mul_inv := _}
A type endowed with 0
, +
, and -
(unary and binary) is an additive group,
if it admits a surjective map that preserves 0
, +
, and -
from a sub_neg_monoid
A type endowed with 0
, +
and -
is an additive group,
if it admits an surjective map from an additive group that preserves these operations.
This version of surjective.add_group
makes sure that the -
operation is defeq
to the specified subtraction operator.
A type endowed with 1
, *
, ⁻¹
and /
is a group,
if it admits an surjective map from a group that preserves these operations.
This version of surjective.group
makes sure that the /
operation is defeq
to the specified division operator.
Equations
- function.surjective.group_div f hf one mul inv div = {mul := div_inv_monoid.mul (function.surjective.div_inv_monoid f hf one mul inv div), mul_assoc := _, one := div_inv_monoid.one (function.surjective.div_inv_monoid f hf one mul inv div), one_mul := _, mul_one := _, inv := div_inv_monoid.inv (function.surjective.div_inv_monoid f hf one mul inv div), div := div_inv_monoid.div (function.surjective.div_inv_monoid f hf one mul inv div), div_eq_mul_inv := _, mul_left_inv := _}
A type endowed with 1
, *
and ⁻¹
is a commutative group,
if it admits a surjective map that preserves 1
, *
and ⁻¹
from a commutative group.
Equations
- function.surjective.comm_group f hf one mul inv = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul), one_mul := _, mul_one := _, inv := group.inv (function.surjective.group f hf one mul inv), div := group.div (function.surjective.group f hf one mul inv), div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}
A type endowed with 0
and +
is an additive commutative group,
if it admits a surjective map that preserves 0
and +
to an additive commutative group.
A type endowed with 1
, *
, ⁻¹
and /
is a commutative group,
if it admits an surjective map from a commutative group that preserves these operations.
This version of surjective.comm_group
makes sure that the /
operation is defeq
to the specified division operator.
Equations
- function.surjective.comm_group_div f hf one mul inv div = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul), one_mul := _, mul_one := _, inv := group.inv (function.surjective.group_div f hf one mul inv div), div := group.div (function.surjective.group_div f hf one mul inv div), div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}
A type endowed with 0
, +
and -
is an additive commutative group,
if it admits an surjective map from an additive commutative group that preserves these operations.
This version of surjective.add_comm_group
makes sure that the -
operation is defeq
to the specified subtraction operator.