mathlib3 documentation

topology.locally_constant.algebra

Algebraic structure on locally constant functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
Equations
@[protected, instance]
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
@[protected, instance]
Equations
@[protected, instance]
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
@[protected, instance]
Equations
@[protected, instance]
Equations
@[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

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

Equations

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

Equations
noncomputable def locally_constant.char_fn {X : Type u_1} (Y : Type u_2) [topological_space X] [mul_zero_one_class Y] {U : set X} (hU : is_clopen U) :

Characteristic functions are locally constant functions taking x : X to 1 if x ∈ U, where U is a clopen set, and 0 otherwise.

Equations
theorem locally_constant.char_fn_eq_one {X : Type u_1} (Y : Type u_2) [topological_space X] [mul_zero_one_class Y] {U : set X} [nontrivial Y] (x : X) (hU : is_clopen U) :
theorem locally_constant.char_fn_eq_zero {X : Type u_1} (Y : Type u_2) [topological_space X] [mul_zero_one_class Y] {U : set X} [nontrivial Y] (x : X) (hU : is_clopen U) :
theorem locally_constant.char_fn_inj {X : Type u_1} (Y : Type u_2) [topological_space X] [mul_zero_one_class Y] {U V : set X} [nontrivial Y] (hU : is_clopen U) (hV : is_clopen V) (h : locally_constant.char_fn Y hU = locally_constant.char_fn Y hV) :
U = V
@[protected, instance]
Equations
@[protected, instance]
Equations
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
@[protected, instance]
def locally_constant.group {X : Type u_1} {Y : Type u_2} [topological_space X] [group Y] :
Equations
@[protected, instance]
Equations

The constant-function embedding, as a ring hom.

Equations
@[protected, instance]
Equations
@[protected, instance]
def locally_constant.ring {X : Type u_1} {Y : Type u_2} [topological_space X] [ring Y] :
Equations
@[protected, instance]
def locally_constant.has_smul {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [has_smul 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_smul 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_smul R Y] (r : R) (f : locally_constant X Y) (x : X) :
(r f) x = r f x
@[protected, 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
@[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) :