mathlib3 documentation

algebra.group_with_zero.inj_surj

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) :

Pullback a mul_zero_class instance along an injective function. See note [reducible non-instances].

Equations
@[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) :

Pushforward a mul_zero_class instance along an surjective function. See note [reducible non-instances].

Equations
@[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
@[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
@[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
@[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
@[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) :

Pullback a monoid_with_zero class along an injective function. See note [reducible non-instances].

Equations
@[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) :

Pushforward a monoid_with_zero class along a surjective function. See note [reducible non-instances].

Equations
@[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
@[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
@[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
@[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
@[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) :

Pullback a group_with_zero class along an injective function. See note [reducible non-instances].

Equations
@[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) :

Pushforward a group_with_zero class along an surjective function. See note [reducible non-instances].

Equations
@[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
@[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