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.

source
@[protected, instance]
def locally_constant.has_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :
has_zero (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.has_one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
has_one (locally_constant X Y)
Equations
source
@[simp]
theorem locally_constant.coe_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] :
⇑0 = 0
source
@[simp]
theorem locally_constant.coe_one {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] :
⇑1 = 1
source
theorem locally_constant.one_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_one Y] (x : X) :
⇑1 x = 1
source
theorem locally_constant.zero_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [has_zero Y] (x : X) :
⇑0 x = 0
source
@[protected, instance]
def locally_constant.has_neg {X : Type u_1} {Y : Type u_2} [topological_space X] [has_neg Y] :
has_neg (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.has_inv {X : Type u_1} {Y : Type u_2} [topological_space X] [has_inv Y] :
has_inv (locally_constant X Y)
Equations
source
@[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) :
⇑-f = -⇑f
source
@[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) :
⇑f⁻¹ = (⇑f)⁻¹
source
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) :
⇑f⁻¹ x = (⇑f x)⁻¹
source
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
source
@[protected, instance]
def locally_constant.has_mul {X : Type u_1} {Y : Type u_2} [topological_space X] [has_mul Y] :
has_mul (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.has_add {X : Type u_1} {Y : Type u_2} [topological_space X] [has_add Y] :
has_add (locally_constant X Y)
Equations
source
@[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
source
@[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
source
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
source
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
source
@[protected, instance]
def locally_constant.add_zero_class {X : Type u_1} {Y : Type u_2} [topological_space X] [add_zero_class Y] :
add_zero_class (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.mul_one_class {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] :
mul_one_class (locally_constant X Y)
Equations
source
def locally_constant.coe_fn_monoid_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] :
locally_constant X Y →* X → Y

coe_fn is a monoid_hom.

Equations
source
@[simp]
theorem locally_constant.coe_fn_add_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [add_zero_class Y] (x : locally_constant X Y) (ᾰ : X) :
⇑locally_constant.coe_fn_add_monoid_hom x ᾰ = ⇑x ᾰ
source
def locally_constant.coe_fn_add_monoid_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [add_zero_class Y] :
locally_constant X Y →+ X → Y

coe_fn is an add_monoid_hom.

Equations
source
@[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) :
⇑locally_constant.coe_fn_monoid_hom x ᾰ = ⇑x ᾰ
source
def locally_constant.const_add_monoid_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [add_zero_class Y] :
Y →+ locally_constant X Y

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

Equations
source
@[simp]
theorem locally_constant.const_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] (y : Y) :
⇑locally_constant.const_monoid_hom y = locally_constant.const X y
source
@[simp]
theorem locally_constant.const_add_monoid_hom_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [add_zero_class Y] (y : Y) :
⇑locally_constant.const_add_monoid_hom y = locally_constant.const X y
source
def locally_constant.const_monoid_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_one_class Y] :
Y →* locally_constant X Y

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

Equations
source
@[protected, instance]
def locally_constant.mul_zero_class {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_zero_class Y] :
mul_zero_class (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.mul_zero_one_class {X : Type u_1} {Y : Type u_2} [topological_space X] [mul_zero_one_class Y] :
mul_zero_one_class (locally_constant X Y)
Equations
source
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) :
locally_constant X Y

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

Equations
source
theorem locally_constant.coe_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) :
⇑(locally_constant.char_fn Y hU) = U.indicator 1
source
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) :
⇑(locally_constant.char_fn Y hU) x = 1 ↔ x ∈ U
source
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) :
⇑(locally_constant.char_fn Y hU) x = 0 ↔ x ∉ U
source
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
source
@[protected, instance]
def locally_constant.has_div {X : Type u_1} {Y : Type u_2} [topological_space X] [has_div Y] :
has_div (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.has_sub {X : Type u_1} {Y : Type u_2} [topological_space X] [has_sub Y] :
has_sub (locally_constant X Y)
Equations
source
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
source
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
source
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
source
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
source
@[protected, instance]
def locally_constant.semigroup {X : Type u_1} {Y : Type u_2} [topological_space X] [semigroup Y] :
semigroup (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_semigroup {X : Type u_1} {Y : Type u_2} [topological_space X] [add_semigroup Y] :
add_semigroup (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.semigroup_with_zero {X : Type u_1} {Y : Type u_2} [topological_space X] [semigroup_with_zero Y] :
semigroup_with_zero (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_comm_semigroup {X : Type u_1} {Y : Type u_2} [topological_space X] [add_comm_semigroup Y] :
add_comm_semigroup (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.comm_semigroup {X : Type u_1} {Y : Type u_2} [topological_space X] [comm_semigroup Y] :
comm_semigroup (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [monoid Y] :
monoid (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [add_monoid Y] :
add_monoid (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_monoid_with_one {X : Type u_1} {Y : Type u_2} [topological_space X] [add_monoid_with_one Y] :
add_monoid_with_one (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.comm_monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [comm_monoid Y] :
comm_monoid (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_comm_monoid {X : Type u_1} {Y : Type u_2} [topological_space X] [add_comm_monoid Y] :
add_comm_monoid (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.group {X : Type u_1} {Y : Type u_2} [topological_space X] [group Y] :
group (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_group {X : Type u_1} {Y : Type u_2} [topological_space X] [add_group Y] :
add_group (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.add_comm_group {X : Type u_1} {Y : Type u_2} [topological_space X] [add_comm_group Y] :
add_comm_group (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.comm_group {X : Type u_1} {Y : Type u_2} [topological_space X] [comm_group Y] :
comm_group (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.distrib {X : Type u_1} {Y : Type u_2} [topological_space X] [distrib Y] :
distrib (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_non_assoc_semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_non_assoc_semiring Y] :
non_unital_non_assoc_semiring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_semiring Y] :
non_unital_semiring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_assoc_semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_assoc_semiring Y] :
non_assoc_semiring (locally_constant X Y)
Equations
source
@[simp]
theorem locally_constant.const_ring_hom_apply {X : Type u_1} {Y : Type u_2} [topological_space X] [non_assoc_semiring Y] (y : Y) :
⇑locally_constant.const_ring_hom y = locally_constant.const X y
source
def locally_constant.const_ring_hom {X : Type u_1} {Y : Type u_2} [topological_space X] [non_assoc_semiring Y] :
Y →+* locally_constant X Y

The constant-function embedding, as a ring hom.

Equations
source
@[protected, instance]
def locally_constant.semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [semiring Y] :
semiring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_comm_semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_comm_semiring Y] :
non_unital_comm_semiring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.comm_semiring {X : Type u_1} {Y : Type u_2} [topological_space X] [comm_semiring Y] :
comm_semiring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_non_assoc_ring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_non_assoc_ring Y] :
non_unital_non_assoc_ring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_ring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_ring Y] :
non_unital_ring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_assoc_ring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_assoc_ring Y] :
non_assoc_ring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.ring {X : Type u_1} {Y : Type u_2} [topological_space X] [ring Y] :
ring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.non_unital_comm_ring {X : Type u_1} {Y : Type u_2} [topological_space X] [non_unital_comm_ring Y] :
non_unital_comm_ring (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.comm_ring {X : Type u_1} {Y : Type u_2} [topological_space X] [comm_ring Y] :
comm_ring (locally_constant X Y)
Equations
source
@[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] :
has_smul R (locally_constant X Y)
Equations
source
@[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
source
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
source
@[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] :
mul_action R (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.distrib_mul_action {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [monoid R] [add_monoid Y] [distrib_mul_action R Y] :
distrib_mul_action R (locally_constant X Y)
Equations
source
@[protected, 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] :
module R (locally_constant X Y)
Equations
source
@[protected, instance]
def locally_constant.algebra {X : Type u_1} {Y : Type u_2} [topological_space X] {R : Type u_3} [comm_semiring R] [semiring Y] [algebra R Y] :
algebra R (locally_constant X Y)
Equations
source
@[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