Lifting groups with zero along injective/surjective maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, reducible]
def
function.injective.mul_zero_class
{M₀ : Type u_1}
{M₀' : Type u_3}
[mul_zero_class M₀]
[has_mul M₀']
[has_zero M₀']
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :
mul_zero_class M₀'
Pullback a mul_zero_class instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.mul_zero_class
{M₀ : Type u_1}
{M₀' : Type u_3}
[mul_zero_class M₀]
[has_mul M₀']
[has_zero M₀']
(f : M₀ → M₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(mul : ∀ (a b : M₀), f (a * b) = f a * f b) :
mul_zero_class M₀'
Pushforward a mul_zero_class instance along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}
@[protected]
theorem
function.injective.no_zero_divisors
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_mul M₀]
[has_zero M₀]
[has_mul M₀']
[has_zero M₀']
[no_zero_divisors M₀']
(f : M₀ → M₀')
(hf : function.injective f)
(zero : f 0 = 0)
(mul : ∀ (x y : M₀), f (x * y) = f x * f y) :
Pushforward a no_zero_divisors instance along an injective function.
@[protected, reducible]
def
function.injective.mul_zero_one_class
{M₀ : Type u_1}
{M₀' : Type u_3}
[mul_zero_one_class M₀]
[has_mul M₀']
[has_zero M₀']
[has_one M₀']
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :
Pullback a mul_zero_one_class instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.mul_zero_one_class f hf zero one mul = {one := mul_one_class.one (function.injective.mul_one_class f hf one mul), mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.mul_zero_one_class
{M₀ : Type u_1}
{M₀' : Type u_3}
[mul_zero_one_class M₀]
[has_mul M₀']
[has_zero M₀']
[has_one M₀']
(f : M₀ → M₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (a b : M₀), f (a * b) = f a * f b) :
Pushforward a mul_zero_one_class instance along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.mul_zero_one_class f hf zero one mul = {one := mul_one_class.one (function.surjective.mul_one_class f hf one mul), mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.semigroup_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_zero M₀']
[has_mul M₀']
[semigroup_with_zero M₀]
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(mul : ∀ (x y : M₀'), f (x * y) = f x * f y) :
Pullback a semigroup_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.semigroup_with_zero f hf zero mul = {mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), mul_assoc := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.semigroup_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[semigroup_with_zero M₀]
[has_zero M₀']
[has_mul M₀']
(f : M₀ → M₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(mul : ∀ (x y : M₀), f (x * y) = f x * f y) :
Pushforward a semigroup_with_zero class along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.semigroup_with_zero f hf zero mul = {mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), mul_assoc := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
[monoid_with_zero M₀]
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(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_with_zero M₀'
Pullback a monoid_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.monoid_with_zero f hf zero one mul npow = {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' := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
[monoid_with_zero M₀]
(f : M₀ → M₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(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_with_zero M₀'
Pushforward a monoid_with_zero class along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.monoid_with_zero f hf zero one mul npow = {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' := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.comm_monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
[comm_monoid_with_zero M₀]
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(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) :
Pullback a monoid_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.comm_monoid_with_zero f hf zero one mul npow = {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' := _, mul_comm := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.surjective.comm_monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
[comm_monoid_with_zero M₀]
(f : M₀ → M₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(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) :
Pushforward a monoid_with_zero class along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.comm_monoid_with_zero f hf zero one mul npow = {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' := _, mul_comm := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected, reducible]
def
function.injective.cancel_monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[cancel_monoid_with_zero M₀]
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(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) :
Pullback a monoid_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.cancel_monoid_with_zero f hf zero one mul npow = {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' := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
@[protected, reducible]
def
function.injective.cancel_comm_monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[cancel_comm_monoid_with_zero M₀]
[has_zero M₀']
[has_mul M₀']
[has_one M₀']
[has_pow M₀' ℕ]
(f : M₀' → M₀)
(hf : function.injective f)
(zero : f 0 = 0)
(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) :
Pullback a cancel_comm_monoid_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.cancel_comm_monoid_with_zero f hf zero one mul npow = {mul := comm_monoid_with_zero.mul (function.injective.comm_monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := comm_monoid_with_zero.one (function.injective.comm_monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := comm_monoid_with_zero.npow (function.injective.comm_monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_monoid_with_zero.zero (function.injective.comm_monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _}
@[protected, reducible]
def
function.injective.group_with_zero
{G₀ : Type u_2}
{G₀' : Type u_4}
[group_with_zero G₀]
[has_zero G₀']
[has_mul G₀']
[has_one G₀']
[has_inv G₀']
[has_div G₀']
[has_pow G₀' ℕ]
[has_pow G₀' ℤ]
(f : G₀' → G₀)
(hf : function.injective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (x y : G₀'), f (x * y) = f x * f y)
(inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : G₀'), f (x / y) = f x / f y)
(npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) :
group_with_zero G₀'
Pullback a group_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.group_with_zero f hf zero one mul inv div npow zpow = {mul := monoid_with_zero.mul (function.injective.monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := monoid_with_zero.one (function.injective.monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.injective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (function.injective.monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, 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' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, reducible]
def
function.surjective.group_with_zero
{G₀ : Type u_2}
{G₀' : Type u_4}
[group_with_zero G₀]
[has_zero G₀']
[has_mul G₀']
[has_one G₀']
[has_inv G₀']
[has_div G₀']
[has_pow G₀' ℕ]
[has_pow G₀' ℤ]
(h01 : 0 ≠ 1)
(f : G₀ → G₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (x y : G₀), f (x * y) = f x * f y)
(inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : G₀), f (x / y) = f x / f y)
(npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) :
group_with_zero G₀'
Pushforward a group_with_zero class along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow = {mul := monoid_with_zero.mul (function.surjective.monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := monoid_with_zero.one (function.surjective.monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.surjective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (function.surjective.monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, 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' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, reducible]
def
function.injective.comm_group_with_zero
{G₀ : Type u_2}
{G₀' : Type u_4}
[comm_group_with_zero G₀]
[has_zero G₀']
[has_mul G₀']
[has_one G₀']
[has_inv G₀']
[has_div G₀']
[has_pow G₀' ℕ]
[has_pow G₀' ℤ]
(f : G₀' → G₀)
(hf : function.injective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (x y : G₀'), f (x * y) = f x * f y)
(inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : G₀'), f (x / y) = f x / f y)
(npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) :
Pullback a comm_group_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.comm_group_with_zero f hf zero one mul inv div npow zpow = {mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv div npow zpow), mul_assoc := _, one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv div npow zpow), one_mul := _, mul_one := _, npow := group_with_zero.npow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected]
def
function.surjective.comm_group_with_zero
{G₀ : Type u_2}
{G₀' : Type u_4}
[comm_group_with_zero G₀]
[has_zero G₀']
[has_mul G₀']
[has_one G₀']
[has_inv G₀']
[has_div G₀']
[has_pow G₀' ℕ]
[has_pow G₀' ℤ]
(h01 : 0 ≠ 1)
(f : G₀ → G₀')
(hf : function.surjective f)
(zero : f 0 = 0)
(one : f 1 = 1)
(mul : ∀ (x y : G₀), f (x * y) = f x * f y)
(inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : G₀), f (x / y) = f x / f y)
(npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) :
Pushforward a comm_group_with_zero class along a surjective function.
Equations
- function.surjective.comm_group_with_zero h01 f hf zero one mul inv div npow zpow = {mul := group_with_zero.mul (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), mul_assoc := _, one := group_with_zero.one (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), one_mul := _, mul_one := _, npow := group_with_zero.npow (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}