mathlib documentation

topology.locally_constant.algebra

Algebraic structure on locally constant functions #

This file puts algebraic structure (add_group, etc) on the type of locally constant functions.

@[instance]
def locally_constant.has_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :
@[instance]
def locally_constant.has_one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
Equations
@[simp]
theorem locally_constant.coe_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :
0 = 0
@[simp]
theorem locally_constant.coe_one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
1 = 1
theorem locally_constant.one_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] (x : X) :
1 x = 1
theorem locally_constant.zero_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] (x : X) :
0 x = 0
@[instance]
def locally_constant.has_neg {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] :
@[instance]
def locally_constant.has_inv {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] :
Equations
@[simp]
theorem locally_constant.coe_neg {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] (f : locally_constant X Y) :
@[simp]
theorem locally_constant.coe_inv {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] (f : locally_constant X Y) :
theorem locally_constant.inv_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] (f : locally_constant X Y) (x : X) :
theorem locally_constant.neg_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] (f : locally_constant X Y) (x : X) :
(-f) x = -f x
@[instance]
def locally_constant.has_mul {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] :
Equations
@[instance]
def locally_constant.has_add {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] :
@[simp]
theorem locally_constant.coe_mul {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] (f g : locally_constant X Y) :
f * g = (f) * g
@[simp]
theorem locally_constant.coe_add {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] (f g : locally_constant X Y) :
(f + g) = f + g
theorem locally_constant.mul_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] (f g : locally_constant X Y) (x : X) :
(f * g) x = (f x) * g x
theorem locally_constant.add_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] (f g : locally_constant X Y) (x : X) :
(f + g) x = f x + g x
@[instance]
@[simp]
@[simp]
theorem locally_constant.coe_fn_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] (x : locally_constant X Y) (ᾰ : X) :

The constant-function embedding, as an additive monoid hom.

def locally_constant.const_monoid_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] :

The constant-function embedding, as a multiplicative monoid hom.

Equations
@[instance]
def locally_constant.has_div {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] :
Equations
@[instance]
def locally_constant.has_sub {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] :
theorem locally_constant.coe_sub {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] (f g : locally_constant X Y) :
(f - g) = f - g
theorem locally_constant.coe_div {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] (f g : locally_constant X Y) :
(f / g) = f / g
theorem locally_constant.sub_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] (f g : locally_constant X Y) (x : X) :
(f - g) x = f x - g x
theorem locally_constant.div_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] (f g : locally_constant X Y) (x : X) :
(f / g) x = f x / g x
@[instance]
@[instance]
def locally_constant.add_monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [add_monoid Y] :
@[instance]
@[instance]
def locally_constant.group {X : Type u_1} {Y : Type u_2} [topological_space X] [group Y] :
Equations
@[instance]
def locally_constant.add_group {X : Type u_1} {Y : Type u_2} [topological_space X] [add_group Y] :
@[instance]

The constant-function embedding, as a ring hom.

Equations
@[instance]
def locally_constant.has_scalar {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [has_scalar R Y] :
Equations
@[simp]
theorem locally_constant.coe_smul {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [has_scalar R Y] (r : R) (f : locally_constant X Y) :
(r f) = r f
theorem locally_constant.smul_apply {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [has_scalar R Y] (r : R) (f : locally_constant X Y) (x : X) :
(r f) x = r f x
@[instance]
def locally_constant.mul_action {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [monoid R] [mul_action R Y] :
Equations
@[instance]
def locally_constant.module {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [semiring R] [add_comm_monoid Y] [module R Y] :
Equations
@[simp]
theorem locally_constant.coe_algebra_map {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [comm_semiring R] [semiring Y] [algebra R Y] (r : R) :
((algebra_map R (locally_constant X Y)) r) = (algebra_map R (X → Y)) r