Lifting algebraic data classes along injective/surjective maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/707 Any changes to this file require a corresponding PR to mathlib4.
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 #
@[protected, reducible]
def
function.injective.semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
semigroup M₁
A type endowed with * is a semigroup,
if it admits an injective map that preserves * to a semigroup.
See note [reducible non-instances].
Equations
- function.injective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}
@[protected, reducible]
def
function.injective.add_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[add_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive semigroup,
if it admits an injective map that preserves + to an additive semigroup.
Equations
- function.injective.add_semigroup f hf mul = {add := has_add.add _inst_1, add_assoc := _}
@[protected, reducible]
def
function.injective.add_comm_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[add_comm_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive commutative semigroup,
if it admits an injective map that preserves + to an additive commutative semigroup.
Equations
- function.injective.add_comm_semigroup f hf mul = {add := add_semigroup.add (function.injective.add_semigroup f hf mul), add_assoc := _, add_comm := _}
@[protected, reducible]
def
function.injective.comm_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[comm_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with * is a commutative semigroup,
if it admits an injective map that preserves * to a commutative semigroup.
See note [reducible non-instances].
Equations
- function.injective.comm_semigroup f hf mul = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.injective.left_cancel_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[left_cancel_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with * is a left cancel semigroup,
if it admits an injective map that preserves * to a left cancel semigroup.
See note [reducible non-instances].
Equations
- function.injective.left_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_left_cancel := _}
@[protected, reducible]
def
function.injective.add_left_cancel_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[add_left_cancel_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive left cancel semigroup,
if it admits an injective map that preserves + to an additive left cancel semigroup.
Equations
- function.injective.add_left_cancel_semigroup f hf mul = {add := has_add.add _inst_1, add_assoc := _, add_left_cancel := _}
@[protected, reducible]
def
function.injective.right_cancel_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[right_cancel_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with * is a right cancel semigroup,
if it admits an injective map that preserves * to a right cancel semigroup.
See note [reducible non-instances].
Equations
- function.injective.right_cancel_semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _, mul_right_cancel := _}
@[protected, reducible]
def
function.injective.add_right_cancel_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[add_right_cancel_semigroup M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive right cancel semigroup,
if it admits an injective map that preserves + to an additive right cancel semigroup.
Equations
- function.injective.add_right_cancel_semigroup f hf mul = {add := has_add.add _inst_1, add_assoc := _, add_right_cancel := _}
@[protected, reducible]
def
function.injective.add_zero_class
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[add_zero_class M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with 0 and + is an add_zero_class,
if it admits an injective map that preserves 0 and + to an add_zero_class.
Equations
- function.injective.add_zero_class f hf one mul = {zero := 0, add := has_add.add _inst_1, zero_add := _, add_zero := _}
@[protected, reducible]
def
function.injective.mul_one_class
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[mul_one_class M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with 1 and * is a mul_one_class,
if it admits an injective map that preserves 1 and * to a mul_one_class.
See note [reducible non-instances].
Equations
- function.injective.mul_one_class f hf one mul = {one := 1, mul := has_mul.mul _inst_1, one_mul := _, mul_one := _}
@[protected, reducible]
def
function.injective.add_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
add_monoid M₁
A type endowed with 0 and + is an additive monoid,
if it admits an injective map that preserves 0 and + to an additive monoid.
This version takes a custom nsmul as a [has_smul ℕ M₁] argument.
Equations
- function.injective.add_monoid f hf one mul npow = {add := add_semigroup.add (function.injective.add_semigroup f hf mul), add_assoc := _, zero := add_zero_class.zero (function.injective.add_zero_class f hf one mul), zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : M₁), n • x, nsmul_zero' := _, nsmul_succ' := _}
@[protected, reducible]
def
function.injective.monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
monoid M₁
A type endowed with 1 and * is a monoid,
if it admits an injective map that preserves 1 and * to a monoid.
See note [reducible non-instances].
Equations
- function.injective.monoid f hf one mul npow = {mul := semigroup.mul (function.injective.semigroup f hf mul), mul_assoc := _, one := mul_one_class.one (function.injective.mul_one_class f hf one mul), one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : M₁), x ^ n, npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.injective.add_monoid_with_one
{M₂ : Type u_2}
{M₁ : Type u_1}
[has_zero M₁]
[has_one M₁]
[has_add M₁]
[has_smul ℕ M₁]
[has_nat_cast M₁]
[add_monoid_with_one M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : M₁), f (x + y) = f x + f y)
(nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :
A type endowed with 0, 1 and + is an additive monoid with one,
if it admits an injective map that preserves 0, 1 and + to an additive monoid with one.
See note [reducible non-instances].
Equations
- function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast = {nat_cast := coe coe_to_lift, add := add_monoid.add (function.injective.add_monoid f hf zero add nsmul), add_assoc := _, zero := add_monoid.zero (function.injective.add_monoid f hf zero add nsmul), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.injective.add_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}
@[protected, reducible]
def
function.injective.left_cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[left_cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
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.
See note [reducible non-instances].
Equations
- function.injective.left_cancel_monoid f hf one mul npow = {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 npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.injective.add_left_cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_left_cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
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.
Equations
- function.injective.add_left_cancel_monoid f hf one mul npow = {add := add_left_cancel_semigroup.add (function.injective.add_left_cancel_semigroup f hf mul), add_assoc := _, add_left_cancel := _, zero := add_monoid.zero (function.injective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.injective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _}
@[protected, reducible]
def
function.injective.right_cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[right_cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
A type endowed with 1 and * is a right cancel monoid,
if it admits an injective map that preserves 1 and * to a right cancel monoid.
See note [reducible non-instances].
Equations
- function.injective.right_cancel_monoid f hf one mul npow = {mul := right_cancel_semigroup.mul (function.injective.right_cancel_semigroup f hf mul), mul_assoc := _, mul_right_cancel := _, one := monoid.one (function.injective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.injective.add_right_cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_right_cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
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.
Equations
- function.injective.add_right_cancel_monoid f hf one mul npow = {add := add_right_cancel_semigroup.add (function.injective.add_right_cancel_semigroup f hf mul), add_assoc := _, add_right_cancel := _, zero := add_monoid.zero (function.injective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.injective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _}
@[protected, reducible]
def
function.injective.add_cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
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.
Equations
- function.injective.add_cancel_monoid f hf one mul npow = {add := add_left_cancel_monoid.add (function.injective.add_left_cancel_monoid f hf one mul npow), add_assoc := _, add_left_cancel := _, zero := add_left_cancel_monoid.zero (function.injective.add_left_cancel_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_left_cancel_monoid.nsmul (function.injective.add_left_cancel_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}
@[protected, reducible]
def
function.injective.cancel_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[cancel_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
A type endowed with 1 and * is a cancel monoid,
if it admits an injective map that preserves 1 and * to a cancel monoid.
See note [reducible non-instances].
Equations
- function.injective.cancel_monoid f hf one mul npow = {mul := left_cancel_monoid.mul (function.injective.left_cancel_monoid f hf one mul npow), mul_assoc := _, mul_left_cancel := _, one := left_cancel_monoid.one (function.injective.left_cancel_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := left_cancel_monoid.npow (function.injective.left_cancel_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_right_cancel := _}
@[protected, reducible]
def
function.injective.add_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
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.
Equations
- function.injective.add_comm_monoid f hf one mul npow = {add := add_comm_semigroup.add (function.injective.add_comm_semigroup f hf mul), add_assoc := _, zero := add_monoid.zero (function.injective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.injective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, reducible]
def
function.injective.comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_monoid M₁
A type endowed with 1 and * is a commutative monoid,
if it admits an injective map that preserves 1 and * to a commutative monoid.
See note [reducible non-instances].
Equations
- function.injective.comm_monoid f hf one mul npow = {mul := comm_semigroup.mul (function.injective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, reducible]
def
function.injective.add_cancel_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[add_cancel_comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
A type endowed with 0 and + is an additive cancel commutative monoid,
if it admits an injective map that preserves 0 and + to an additive cancel commutative monoid.
Equations
- function.injective.add_cancel_comm_monoid f hf one mul npow = {add := add_left_cancel_semigroup.add (function.injective.add_left_cancel_semigroup f hf mul), add_assoc := _, add_left_cancel := _, zero := add_comm_monoid.zero (function.injective.add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, reducible]
def
function.injective.cancel_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[cancel_comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
A type endowed with 1 and * is a cancel commutative monoid,
if it admits an injective map that preserves 1 and * to a cancel commutative monoid.
See note [reducible non-instances].
Equations
- function.injective.cancel_comm_monoid f hf one mul npow = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, reducible]
def
function.injective.has_involutive_inv
{M₂ : Type u_2}
{M₁ : Type u_1}
[has_inv M₁]
[has_involutive_inv M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) :
A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type
which has an involutive inversion.
Equations
- function.injective.has_involutive_inv f hf inv = {inv := has_inv.inv _inst_4, inv_inv := _}
@[protected, reducible]
def
function.injective.has_involutive_neg
{M₂ : Type u_2}
{M₁ : Type u_1}
[has_neg M₁]
[has_involutive_neg M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(inv : ∀ (x : M₁), f (-x) = -f x) :
A type has an involutive negation if it admits a surjective map that
preserves ⁻¹ to a type which has an involutive inversion.
Equations
- function.injective.has_involutive_neg f hf inv = {neg := has_neg.neg _inst_4, neg_neg := _}
@[protected, reducible]
def
function.injective.sub_neg_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[sub_neg_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
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.
This version takes custom nsmul and zsmul as [has_smul ℕ M₁] and
[has_smul ℤ M₁] arguments.
Equations
- function.injective.sub_neg_monoid f hf one mul inv div npow zpow = {add := add_monoid.add (function.injective.add_monoid f hf one mul npow), add_assoc := _, zero := add_monoid.zero (function.injective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.injective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg _inst_4, sub := has_sub.sub _inst_5, sub_eq_add_neg := _, zsmul := λ (n : ℤ) (x : M₁), n • x, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
@[protected, reducible]
def
function.injective.div_inv_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[has_inv M₁]
[has_div M₁]
[has_pow M₁ ℤ]
[div_inv_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
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.
See note [reducible non-instances].
Equations
- function.injective.div_inv_monoid f hf one mul inv div npow zpow = {mul := monoid.mul (function.injective.monoid f hf one mul npow), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, inv := has_inv.inv _inst_4, div := has_div.div _inst_5, div_eq_mul_inv := _, zpow := λ (n : ℤ) (x : M₁), x ^ n, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
@[protected, reducible]
def
function.injective.subtraction_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[subtraction_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
A type endowed with 0, +, unary -, and binary - is a subtraction_monoid
if it admits an injective map that preserves 0, +, unary -, and binary - to
a subtraction_monoid.
This version takes custom nsmul and zsmul as [has_smul ℕ M₁] and
[has_smul ℤ M₁] arguments.
Equations
- function.injective.subtraction_monoid f hf one mul inv div npow zpow = {add := sub_neg_monoid.add (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), add_assoc := _, zero := sub_neg_monoid.zero (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), sub := sub_neg_monoid.sub (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}
@[protected, reducible]
def
function.injective.division_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[has_inv M₁]
[has_div M₁]
[has_pow M₁ ℤ]
[division_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
A type endowed with 1, *, ⁻¹, and / is a division_monoid
if it admits an injective map that preserves 1, *, ⁻¹, and / to a division_monoid.
Equations
- function.injective.division_monoid f hf one mul inv div npow zpow = {mul := div_inv_monoid.mul (function.injective.div_inv_monoid f hf one mul inv div npow zpow), mul_assoc := _, one := div_inv_monoid.one (function.injective.div_inv_monoid f hf one mul inv div npow zpow), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (function.injective.div_inv_monoid f hf one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div := div_inv_monoid.div (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (function.injective.div_inv_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}
@[protected, reducible]
def
function.injective.division_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[has_inv M₁]
[has_div M₁]
[has_pow M₁ ℤ]
[division_comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
A type endowed with 1, *, ⁻¹, and / is a division_comm_monoid
if it admits an injective map that preserves 1, *, ⁻¹, and / to a division_comm_monoid.
See note [reducible non-instances].
Equations
- function.injective.division_comm_monoid f hf one mul inv div npow zpow = {mul := division_monoid.mul (function.injective.division_monoid f hf one mul inv div npow zpow), mul_assoc := _, one := division_monoid.one (function.injective.division_monoid f hf one mul inv div npow zpow), one_mul := _, mul_one := _, npow := division_monoid.npow (function.injective.division_monoid f hf one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := division_monoid.inv (function.injective.division_monoid f hf one mul inv div npow zpow), div := division_monoid.div (function.injective.division_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := division_monoid.zpow (function.injective.division_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}
@[protected, reducible]
def
function.injective.subtraction_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[subtraction_comm_monoid M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
A type endowed with 0, +, unary -, and binary - is a subtraction_comm_monoid
if it admits an injective map that preserves 0, +, unary -, and binary - to
a subtraction_comm_monoid.
This version takes custom nsmul and zsmul as [has_smul ℕ M₁] and
[has_smul ℤ M₁] arguments.
Equations
- function.injective.subtraction_comm_monoid f hf one mul inv div npow zpow = {add := subtraction_monoid.add (function.injective.subtraction_monoid f hf one mul inv div npow zpow), add_assoc := _, zero := subtraction_monoid.zero (function.injective.subtraction_monoid f hf one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := subtraction_monoid.nsmul (function.injective.subtraction_monoid f hf one mul inv div npow zpow), nsmul_zero' := _, nsmul_succ' := _, neg := subtraction_monoid.neg (function.injective.subtraction_monoid f hf one mul inv div npow zpow), sub := subtraction_monoid.sub (function.injective.subtraction_monoid f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul (function.injective.subtraction_monoid f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}
@[protected, reducible]
def
function.injective.group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[has_inv M₁]
[has_div M₁]
[has_pow M₁ ℤ]
[group M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
group M₁
A type endowed with 1, * and ⁻¹ is a group,
if it admits an injective map that preserves 1, * and ⁻¹ to a group.
See note [reducible non-instances].
Equations
- function.injective.group f hf one mul inv div npow zpow = {mul := div_inv_monoid.mul (function.injective.div_inv_monoid f hf one mul inv div npow zpow), mul_assoc := _, one := div_inv_monoid.one (function.injective.div_inv_monoid f hf one mul inv div npow zpow), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (function.injective.div_inv_monoid f hf one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div := div_inv_monoid.div (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (function.injective.div_inv_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[protected, reducible]
def
function.injective.add_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[add_group M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
add_group M₁
A type endowed with 0 and + is an additive group,
if it admits an injective map that preserves 0 and + to an additive group.
Equations
- function.injective.add_group f hf one mul inv div npow zpow = {add := sub_neg_monoid.add (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), add_assoc := _, zero := sub_neg_monoid.zero (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), sub := sub_neg_monoid.sub (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (function.injective.sub_neg_monoid f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[protected, reducible]
def
function.injective.add_group_with_one
{M₂ : Type u_2}
{M₁ : Type u_1}
[has_zero M₁]
[has_one M₁]
[has_add M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[has_nat_cast M₁]
[has_int_cast M₁]
[add_group_with_one M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : M₁), f (x + y) = f x + f y)
(neg : ∀ (x : M₁), f (-x) = -f x)
(sub : ∀ (x y : M₁), f (x - y) = f x - f y)
(nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
(int_cast : ∀ (n : ℤ), f ↑n = ↑n) :
A type endowed with 0, 1 and + is an additive group with one,
if it admits an injective map that preserves 0, 1 and + to an additive group with one.
See note [reducible non-instances].
Equations
- function.injective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast = {int_cast := coe coe_to_lift, add := add_group.add (function.injective.add_group f hf zero add neg sub nsmul zsmul), add_assoc := _, zero := add_group.zero (function.injective.add_group f hf zero add neg sub nsmul zsmul), zero_add := _, add_zero := _, nsmul := add_group.nsmul (function.injective.add_group f hf zero add neg sub nsmul zsmul), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (function.injective.add_group f hf zero add neg sub nsmul zsmul), sub := add_group.sub (function.injective.add_group f hf zero add neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := add_group.zsmul (function.injective.add_group f hf zero add neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := add_monoid_with_one.nat_cast (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), one := add_monoid_with_one.one (function.injective.add_monoid_with_one f hf zero one add nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, reducible]
def
function.injective.comm_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₁]
[has_one M₁]
[has_pow M₁ ℕ]
[has_inv M₁]
[has_div M₁]
[has_pow M₁ ℤ]
[comm_group M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
comm_group M₁
A type endowed with 1, * and ⁻¹ is a commutative group,
if it admits an injective map that preserves 1, * and ⁻¹ to a commutative group.
See note [reducible non-instances].
Equations
- function.injective.comm_group f hf one mul inv div npow zpow = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, inv := group.inv (function.injective.group f hf one mul inv div npow zpow), div := group.div (function.injective.group f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group.zpow (function.injective.group f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, reducible]
def
function.injective.add_comm_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₁]
[has_zero M₁]
[has_smul ℕ M₁]
[has_neg M₁]
[has_sub M₁]
[has_smul ℤ M₁]
[add_comm_group M₂]
(f : M₁ → M₂)
(hf : function.injective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
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.
Equations
- function.injective.add_comm_group f hf one mul inv div npow zpow = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf one mul npow), add_assoc := _, zero := add_comm_monoid.zero (function.injective.add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (function.injective.add_group f hf one mul inv div npow zpow), sub := add_group.sub (function.injective.add_group f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := add_group.zsmul (function.injective.add_group f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Surjective #
@[protected, reducible]
def
function.surjective.add_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[add_semigroup M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive semigroup,
if it admits a surjective map that preserves + from an additive semigroup.
Equations
- function.surjective.add_semigroup f hf mul = {add := has_add.add _inst_1, add_assoc := _}
@[protected, reducible]
def
function.surjective.semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[semigroup M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
semigroup M₂
A type endowed with * is a semigroup,
if it admits a surjective map that preserves * from a semigroup.
See note [reducible non-instances].
Equations
- function.surjective.semigroup f hf mul = {mul := has_mul.mul _inst_1, mul_assoc := _}
@[protected, reducible]
def
function.surjective.comm_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[comm_semigroup M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with * is a commutative semigroup,
if it admits a surjective map that preserves * from a commutative semigroup.
See note [reducible non-instances].
Equations
- function.surjective.comm_semigroup f hf mul = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.add_comm_semigroup
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[add_comm_semigroup M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with + is an additive commutative semigroup,
if it admits a surjective map that preserves + from an additive commutative semigroup.
Equations
- function.surjective.add_comm_semigroup f hf mul = {add := add_semigroup.add (function.surjective.add_semigroup f hf mul), add_assoc := _, add_comm := _}
@[protected, reducible]
def
function.surjective.mul_one_class
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[mul_one_class M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y) :
A type endowed with 1 and * is a mul_one_class,
if it admits a surjective map that preserves 1 and * from a mul_one_class.
See note [reducible non-instances].
Equations
- function.surjective.mul_one_class f hf one mul = {one := 1, mul := has_mul.mul _inst_1, one_mul := _, mul_one := _}
@[protected, reducible]
def
function.surjective.add_zero_class
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[add_zero_class M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y) :
A type endowed with 0 and + is an add_zero_class,
if it admits a surjective map that preserves 0 and + to an add_zero_class.
Equations
- function.surjective.add_zero_class f hf one mul = {zero := 0, add := has_add.add _inst_1, zero_add := _, add_zero := _}
@[protected, reducible]
def
function.surjective.monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[has_pow M₂ ℕ]
[monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
monoid M₂
A type endowed with 1 and * is a monoid,
if it admits a surjective map that preserves 1 and * to a monoid.
See note [reducible non-instances].
Equations
- function.surjective.monoid f hf one mul npow = {mul := semigroup.mul (function.surjective.semigroup f hf mul), mul_assoc := _, one := mul_one_class.one (function.surjective.mul_one_class f hf one mul), one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : M₂), x ^ n, npow_zero' := _, npow_succ' := _}
@[protected, reducible]
def
function.surjective.add_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[has_smul ℕ M₂]
[add_monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
add_monoid M₂
A type endowed with 0 and + is an additive monoid,
if it admits a surjective map that preserves 0 and + to an additive monoid.
This version takes a custom nsmul as a [has_smul ℕ M₂] argument.
Equations
- function.surjective.add_monoid f hf one mul npow = {add := add_semigroup.add (function.surjective.add_semigroup f hf mul), add_assoc := _, zero := add_zero_class.zero (function.surjective.add_zero_class f hf one mul), zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : M₂), n • x, nsmul_zero' := _, nsmul_succ' := _}
@[protected, reducible]
def
function.surjective.add_monoid_with_one
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_zero M₂]
[has_one M₂]
[has_add M₂]
[has_smul ℕ M₂]
[has_nat_cast M₂]
[add_monoid_with_one M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : M₁), f (x + y) = f x + f y)
(nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n) :
A type endowed with 0, 1 and + is an additive monoid with one,
if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one.
See note [reducible non-instances].
Equations
- function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast = {nat_cast := coe coe_to_lift, add := add_monoid.add (function.surjective.add_monoid f hf zero add nsmul), add_assoc := _, zero := add_monoid.zero (function.surjective.add_monoid f hf zero add nsmul), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.surjective.add_monoid f hf zero add nsmul), nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}
@[protected, reducible]
def
function.surjective.add_comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[has_smul ℕ M₂]
[add_comm_monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) :
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.
Equations
- function.surjective.add_comm_monoid f hf one mul npow = {add := add_comm_semigroup.add (function.surjective.add_comm_semigroup f hf mul), add_assoc := _, zero := add_monoid.zero (function.surjective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.surjective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, reducible]
def
function.surjective.comm_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[has_pow M₂ ℕ]
[comm_monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) :
comm_monoid M₂
A type endowed with 1 and * is a commutative monoid,
if it admits a surjective map that preserves 1 and * from a commutative monoid.
See note [reducible non-instances].
Equations
- function.surjective.comm_monoid f hf one mul npow = {mul := comm_semigroup.mul (function.surjective.comm_semigroup f hf mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.surjective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.has_involutive_inv
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_inv M₂]
[has_involutive_inv M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) :
A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type
which has an involutive inversion.
Equations
- function.surjective.has_involutive_inv f hf inv = {inv := has_inv.inv _inst_4, inv_inv := _}
@[protected, reducible]
def
function.surjective.has_involutive_neg
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_neg M₂]
[has_involutive_neg M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(inv : ∀ (x : M₁), f (-x) = -f x) :
A type has an involutive negation if it admits a surjective map that
preserves ⁻¹ to a type which has an involutive inversion.
Equations
- function.surjective.has_involutive_neg f hf inv = {neg := has_neg.neg _inst_4, neg_neg := _}
@[protected, reducible]
def
function.surjective.div_inv_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[has_pow M₂ ℕ]
[has_inv M₂]
[has_div M₂]
[has_pow M₂ ℤ]
[div_inv_monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
A type endowed with 1, *, ⁻¹, and / is a div_inv_monoid
if it admits a surjective map that preserves 1, *, ⁻¹, and / to a div_inv_monoid.
See note [reducible non-instances].
Equations
- function.surjective.div_inv_monoid f hf one mul inv div npow zpow = {mul := monoid.mul (function.surjective.monoid f hf one mul npow), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.surjective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, inv := has_inv.inv _inst_4, div := has_div.div _inst_5, div_eq_mul_inv := _, zpow := λ (n : ℤ) (x : M₂), x ^ n, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
@[protected, reducible]
def
function.surjective.sub_neg_monoid
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[has_smul ℕ M₂]
[has_neg M₂]
[has_sub M₂]
[has_smul ℤ M₂]
[sub_neg_monoid M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
A type endowed with 0, +, unary -, and binary - is a sub_neg_monoid
if it admits a surjective map that preserves 0, +, unary -, and binary - to
a sub_neg_monoid.
Equations
- function.surjective.sub_neg_monoid f hf one mul inv div npow zpow = {add := add_monoid.add (function.surjective.add_monoid f hf one mul npow), add_assoc := _, zero := add_monoid.zero (function.surjective.add_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (function.surjective.add_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg _inst_4, sub := has_sub.sub _inst_5, sub_eq_add_neg := _, zsmul := λ (n : ℤ) (x : M₂), n • x, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
@[protected, reducible]
def
function.surjective.group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[has_pow M₂ ℕ]
[has_inv M₂]
[has_div M₂]
[has_pow M₂ ℤ]
[group M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
group M₂
A type endowed with 1, * and ⁻¹ is a group,
if it admits a surjective map that preserves 1, * and ⁻¹ to a group.
See note [reducible non-instances].
Equations
- function.surjective.group f hf one mul inv div npow zpow = {mul := div_inv_monoid.mul (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), mul_assoc := _, one := div_inv_monoid.one (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), div := div_inv_monoid.div (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[protected, reducible]
def
function.surjective.add_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[has_smul ℕ M₂]
[has_neg M₂]
[has_sub M₂]
[has_smul ℤ M₂]
[add_group M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
add_group M₂
A type endowed with 0 and + is an additive group,
if it admits a surjective map that preserves 0 and + to an additive group.
Equations
- function.surjective.add_group f hf one mul inv div npow zpow = {add := sub_neg_monoid.add (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), add_assoc := _, zero := sub_neg_monoid.zero (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), sub := sub_neg_monoid.sub (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (function.surjective.sub_neg_monoid f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[protected]
def
function.surjective.add_group_with_one
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_zero M₂]
[has_one M₂]
[has_add M₂]
[has_neg M₂]
[has_sub M₂]
[has_smul ℕ M₂]
[has_smul ℤ M₂]
[has_nat_cast M₂]
[has_int_cast M₂]
[add_group_with_one M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : M₁), f (x + y) = f x + f y)
(neg : ∀ (x : M₁), f (-x) = -f x)
(sub : ∀ (x y : M₁), f (x - y) = f x - f y)
(nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zsmul : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x)
(nat_cast : ∀ (n : ℕ), f ↑n = ↑n)
(int_cast : ∀ (n : ℤ), f ↑n = ↑n) :
A type endowed with 0, 1, + is an additive group with one,
if it admits a surjective map that preserves 0, 1, and + to an additive group with one.
See note [reducible non-instances].
Equations
- function.surjective.add_group_with_one f hf zero one add neg sub nsmul zsmul nat_cast int_cast = {int_cast := coe coe_to_lift, add := add_monoid_with_one.add (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), add_assoc := _, zero := add_monoid_with_one.zero (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (function.surjective.add_group f hf zero add neg sub nsmul zsmul), sub := add_group.sub (function.surjective.add_group f hf zero add neg sub nsmul zsmul), sub_eq_add_neg := _, zsmul := add_group.zsmul (function.surjective.add_group f hf zero add neg sub nsmul zsmul), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := add_monoid_with_one.nat_cast (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), one := add_monoid_with_one.one (function.surjective.add_monoid_with_one f hf zero one add nsmul nat_cast), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, reducible]
def
function.surjective.comm_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_mul M₂]
[has_one M₂]
[has_pow M₂ ℕ]
[has_inv M₂]
[has_div M₂]
[has_pow M₂ ℤ]
[comm_group M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 1 = 1)
(mul : ∀ (x y : M₁), f (x * y) = f x * f y)
(inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : M₁), f (x / y) = f x / f y)
(npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) :
comm_group M₂
A type endowed with 1, *, ⁻¹, and / is a commutative group,
if it admits a surjective map that preserves 1, *, ⁻¹, and / from a commutative group.
See note [reducible non-instances].
Equations
- function.surjective.comm_group f hf one mul inv div npow zpow = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.surjective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, inv := group.inv (function.surjective.group f hf one mul inv div npow zpow), div := group.div (function.surjective.group f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group.zpow (function.surjective.group f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, reducible]
def
function.surjective.add_comm_group
{M₁ : Type u_1}
{M₂ : Type u_2}
[has_add M₂]
[has_zero M₂]
[has_smul ℕ M₂]
[has_neg M₂]
[has_sub M₂]
[has_smul ℤ M₂]
[add_comm_group M₁]
(f : M₁ → M₂)
(hf : function.surjective f)
(one : f 0 = 0)
(mul : ∀ (x y : M₁), f (x + y) = f x + f y)
(inv : ∀ (x : M₁), f (-x) = -f x)
(div : ∀ (x y : M₁), f (x - y) = f x - f y)
(npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
(zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) :
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.
Equations
- function.surjective.add_comm_group f hf one mul inv div npow zpow = {add := add_comm_monoid.add (function.surjective.add_comm_monoid f hf one mul npow), add_assoc := _, zero := add_comm_monoid.zero (function.surjective.add_comm_monoid f hf one mul npow), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.surjective.add_comm_monoid f hf one mul npow), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (function.surjective.add_group f hf one mul inv div npow zpow), sub := add_group.sub (function.surjective.add_group f hf one mul inv div npow zpow), sub_eq_add_neg := _, zsmul := add_group.zsmul (function.surjective.add_group f hf one mul inv div npow zpow), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}