topology.locally_constant.algebra

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

locally_constant.has_zero = {zero := locally_constant.const X 0}

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

locally_constant.has_one = {one := locally_constant.const X 1}

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

locally_constant.has_neg = {neg := λ (f : locally_constant X Y), {to_fun := -⇑f, is_locally_constant := _}}

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

locally_constant.has_inv = {inv := λ (f : locally_constant X Y), {to_fun := (⇑f)⁻¹, is_locally_constant := _}}

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

locally_constant.has_mul = {mul := λ (f g : locally_constant X Y), {to_fun := ⇑f * ⇑g, is_locally_constant := _}}

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

locally_constant.has_add = {add := λ (f g : locally_constant X Y), {to_fun := ⇑f + ⇑g, is_locally_constant := _}}

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

locally_constant.add_zero_class = {zero := 0, add := has_add.add locally_constant.has_add, zero_add := _, add_zero := _}

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

locally_constant.mul_one_class = {one := 1, mul := has_mul.mul locally_constant.has_mul, one_mul := _, mul_one := _}

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

locally_constant.coe_fn_monoid_hom = {to_fun := coe_fn locally_constant.has_coe_to_fun, map_one' := _, map_mul' := _}

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

locally_constant.coe_fn_add_monoid_hom = {to_fun := coe_fn locally_constant.has_coe_to_fun, map_zero' := _, map_add' := _}

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

locally_constant.const_add_monoid_hom = {to_fun := locally_constant.const X _inst_1, map_zero' := _, map_add' := _}

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

locally_constant.const_monoid_hom = {to_fun := locally_constant.const X _inst_1, map_one' := _, map_mul' := _}

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

locally_constant.mul_zero_class = {mul := has_mul.mul locally_constant.has_mul, zero := 0, zero_mul := _, mul_zero := _}

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

locally_constant.mul_zero_one_class = {one := mul_one_class.one locally_constant.mul_one_class, mul := mul_zero_class.mul locally_constant.mul_zero_class, one_mul := _, mul_one := _, zero := mul_zero_class.zero locally_constant.mul_zero_class, zero_mul := _, mul_zero := _}

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

locally_constant.char_fn Y hU = 1.indicator hU

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

locally_constant.has_div = {div := λ (f g : locally_constant X Y), {to_fun := ⇑f / ⇑g, is_locally_constant := _}}

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

locally_constant.has_sub = {sub := λ (f g : locally_constant X Y), {to_fun := ⇑f - ⇑g, is_locally_constant := _}}

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

locally_constant.semigroup = {mul := has_mul.mul locally_constant.has_mul, mul_assoc := _}

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

locally_constant.add_semigroup = {add := has_add.add locally_constant.has_add, add_assoc := _}

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

locally_constant.semigroup_with_zero = {mul := mul_zero_class.mul locally_constant.mul_zero_class, mul_assoc := _, zero := mul_zero_class.zero locally_constant.mul_zero_class, zero_mul := _, mul_zero := _}

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

locally_constant.add_comm_semigroup = {add := add_semigroup.add locally_constant.add_semigroup, add_assoc := _, add_comm := _}

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

locally_constant.comm_semigroup = {mul := semigroup.mul locally_constant.semigroup, mul_assoc := _, mul_comm := _}

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

locally_constant.monoid = {mul := has_mul.mul locally_constant.has_mul, mul_assoc := _, one := mul_one_class.one locally_constant.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (locally_constant X Y)), npow_zero' := _, npow_succ' := _}

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

locally_constant.add_monoid = {add := has_add.add locally_constant.has_add, add_assoc := _, zero := add_zero_class.zero locally_constant.add_zero_class, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (locally_constant X Y)), nsmul_zero' := _, nsmul_succ' := _}

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

locally_constant.add_monoid_with_one = {nat_cast := λ (n : ℕ), locally_constant.const X ↑n, add := add_monoid.add locally_constant.add_monoid, add_assoc := _, zero := add_monoid.zero locally_constant.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul locally_constant.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}

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

locally_constant.comm_monoid = {mul := comm_semigroup.mul locally_constant.comm_semigroup, mul_assoc := _, one := monoid.one locally_constant.monoid, one_mul := _, mul_one := _, npow := monoid.npow locally_constant.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

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

locally_constant.add_comm_monoid = {add := add_comm_semigroup.add locally_constant.add_comm_semigroup, add_assoc := _, zero := add_monoid.zero locally_constant.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul locally_constant.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

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

locally_constant.group = {mul := monoid.mul locally_constant.monoid, mul_assoc := _, one := monoid.one locally_constant.monoid, one_mul := _, mul_one := _, npow := monoid.npow locally_constant.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv locally_constant.has_inv, div := has_div.div locally_constant.has_div, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul locally_constant.group._proof_7 monoid.one locally_constant.group._proof_8 locally_constant.group._proof_9 monoid.npow locally_constant.group._proof_10 locally_constant.group._proof_11 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

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

locally_constant.add_group = {add := add_monoid.add locally_constant.add_monoid, add_assoc := _, zero := add_monoid.zero locally_constant.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul locally_constant.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg locally_constant.has_neg, sub := has_sub.sub locally_constant.has_sub, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add locally_constant.add_group._proof_7 add_monoid.zero locally_constant.add_group._proof_8 locally_constant.add_group._proof_9 add_monoid.nsmul locally_constant.add_group._proof_10 locally_constant.add_group._proof_11 has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}

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

locally_constant.add_comm_group = {add := add_comm_monoid.add locally_constant.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero locally_constant.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul locally_constant.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg locally_constant.add_group, sub := add_group.sub locally_constant.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul locally_constant.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

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

locally_constant.comm_group = {mul := comm_monoid.mul locally_constant.comm_monoid, mul_assoc := _, one := comm_monoid.one locally_constant.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow locally_constant.comm_monoid, npow_zero' := _, npow_succ' := _, inv := group.inv locally_constant.group, div := group.div locally_constant.group, div_eq_mul_inv := _, zpow := group.zpow locally_constant.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

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

locally_constant.distrib = {mul := has_mul.mul locally_constant.has_mul, add := has_add.add locally_constant.has_add, left_distrib := _, right_distrib := _}

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

locally_constant.non_unital_non_assoc_semiring = {add := add_comm_monoid.add locally_constant.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero locally_constant.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul locally_constant.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul locally_constant.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

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

locally_constant.non_assoc_semiring = {add := add_monoid_with_one.add locally_constant.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero locally_constant.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul locally_constant.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_one_class.mul locally_constant.mul_one_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one locally_constant.mul_one_class, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast locally_constant.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _}

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

locally_constant.const_ring_hom = {to_fun := locally_constant.const X _inst_1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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

locally_constant.semiring = {add := non_assoc_semiring.add locally_constant.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero locally_constant.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul locally_constant.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_assoc_semiring.mul locally_constant.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one locally_constant.non_assoc_semiring, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast locally_constant.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow locally_constant.monoid, npow_zero' := _, npow_succ' := _}

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

locally_constant.non_unital_comm_semiring = {add := non_unital_semiring.add locally_constant.non_unital_semiring, add_assoc := _, zero := non_unital_semiring.zero locally_constant.non_unital_semiring, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul locally_constant.non_unital_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul locally_constant.non_unital_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

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

locally_constant.comm_semiring = {add := semiring.add locally_constant.semiring, add_assoc := _, zero := semiring.zero locally_constant.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul locally_constant.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul locally_constant.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one locally_constant.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast locally_constant.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow locally_constant.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}

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

locally_constant.non_unital_non_assoc_ring = {add := add_comm_group.add locally_constant.add_comm_group, add_assoc := _, zero := add_comm_group.zero locally_constant.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul locally_constant.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg locally_constant.add_comm_group, sub := add_comm_group.sub locally_constant.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul locally_constant.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul locally_constant.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

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

locally_constant.non_unital_ring = {add := non_unital_non_assoc_ring.add locally_constant.non_unital_non_assoc_ring, add_assoc := _, zero := non_unital_non_assoc_ring.zero locally_constant.non_unital_non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_ring.nsmul locally_constant.non_unital_non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_non_assoc_ring.neg locally_constant.non_unital_non_assoc_ring, sub := non_unital_non_assoc_ring.sub locally_constant.non_unital_non_assoc_ring, sub_eq_add_neg := _, zsmul := non_unital_non_assoc_ring.zsmul locally_constant.non_unital_non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semigroup.mul locally_constant.semigroup, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

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

locally_constant.non_assoc_ring = {add := non_unital_non_assoc_ring.add locally_constant.non_unital_non_assoc_ring, add_assoc := _, zero := non_unital_non_assoc_ring.zero locally_constant.non_unital_non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_ring.nsmul locally_constant.non_unital_non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_non_assoc_ring.neg locally_constant.non_unital_non_assoc_ring, sub := non_unital_non_assoc_ring.sub locally_constant.non_unital_non_assoc_ring, sub_eq_add_neg := _, zsmul := non_unital_non_assoc_ring.zsmul locally_constant.non_unital_non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := mul_one_class.mul locally_constant.mul_one_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one locally_constant.mul_one_class, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast._default mul_one_class.one non_unital_non_assoc_ring.add locally_constant.non_assoc_ring._proof_18 non_unital_non_assoc_ring.zero locally_constant.non_assoc_ring._proof_19 locally_constant.non_assoc_ring._proof_20 non_unital_non_assoc_ring.nsmul locally_constant.non_assoc_ring._proof_21 locally_constant.non_assoc_ring._proof_22, nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast._default (non_assoc_semiring.nat_cast._default mul_one_class.one non_unital_non_assoc_ring.add locally_constant.non_assoc_ring._proof_18 non_unital_non_assoc_ring.zero locally_constant.non_assoc_ring._proof_19 locally_constant.non_assoc_ring._proof_20 non_unital_non_assoc_ring.nsmul locally_constant.non_assoc_ring._proof_21 locally_constant.non_assoc_ring._proof_22) non_unital_non_assoc_ring.add locally_constant.non_assoc_ring._proof_25 non_unital_non_assoc_ring.zero locally_constant.non_assoc_ring._proof_26 locally_constant.non_assoc_ring._proof_27 non_unital_non_assoc_ring.nsmul locally_constant.non_assoc_ring._proof_28 locally_constant.non_assoc_ring._proof_29 mul_one_class.one locally_constant.non_assoc_ring._proof_30 locally_constant.non_assoc_ring._proof_31 non_unital_non_assoc_ring.neg non_unital_non_assoc_ring.sub locally_constant.non_assoc_ring._proof_32 non_unital_non_assoc_ring.zsmul locally_constant.non_assoc_ring._proof_33 locally_constant.non_assoc_ring._proof_34 locally_constant.non_assoc_ring._proof_35 locally_constant.non_assoc_ring._proof_36, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

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

locally_constant.ring = {add := semiring.add locally_constant.semiring, add_assoc := _, zero := semiring.zero locally_constant.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul locally_constant.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg locally_constant.add_comm_group, sub := add_comm_group.sub locally_constant.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul locally_constant.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add locally_constant.ring._proof_12 semiring.zero locally_constant.ring._proof_13 locally_constant.ring._proof_14 semiring.nsmul locally_constant.ring._proof_15 locally_constant.ring._proof_16 semiring.one locally_constant.ring._proof_17 locally_constant.ring._proof_18 add_comm_group.neg add_comm_group.sub locally_constant.ring._proof_19 add_comm_group.zsmul locally_constant.ring._proof_20 locally_constant.ring._proof_21 locally_constant.ring._proof_22 locally_constant.ring._proof_23, nat_cast := semiring.nat_cast locally_constant.semiring, one := semiring.one locally_constant.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul locally_constant.semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow locally_constant.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

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

locally_constant.non_unital_comm_ring = {add := non_unital_comm_semiring.add locally_constant.non_unital_comm_semiring, add_assoc := _, zero := non_unital_comm_semiring.zero locally_constant.non_unital_comm_semiring, zero_add := _, add_zero := _, nsmul := non_unital_comm_semiring.nsmul locally_constant.non_unital_comm_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg locally_constant.non_unital_ring, sub := non_unital_ring.sub locally_constant.non_unital_ring, sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul locally_constant.non_unital_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_comm_semiring.mul locally_constant.non_unital_comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

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

locally_constant.comm_ring = {add := comm_semiring.add locally_constant.comm_semiring, add_assoc := _, zero := comm_semiring.zero locally_constant.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul locally_constant.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg locally_constant.ring, sub := ring.sub locally_constant.ring, sub_eq_add_neg := _, zsmul := ring.zsmul locally_constant.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast locally_constant.ring, nat_cast := comm_semiring.nat_cast locally_constant.comm_semiring, one := comm_semiring.one locally_constant.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semiring.mul locally_constant.comm_semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow locally_constant.comm_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

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

locally_constant.has_smul = {smul := λ (r : R) (f : locally_constant X Y), {to_fun := r • ⇑f, is_locally_constant := _}}

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

locally_constant.mul_action = function.injective.mul_action coe_fn locally_constant.coe_injective locally_constant.mul_action._proof_1

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

locally_constant.distrib_mul_action = function.injective.distrib_mul_action locally_constant.coe_fn_add_monoid_hom locally_constant.coe_injective locally_constant.distrib_mul_action._proof_1

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

locally_constant.module = function.injective.module R locally_constant.coe_fn_add_monoid_hom locally_constant.coe_injective locally_constant.module._proof_1

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

locally_constant.algebra = {to_has_smul := locally_constant.has_smul smul_with_zero.to_has_smul, to_ring_hom := locally_constant.const_ring_hom.comp (algebra_map R Y), commutes' := _, smul_def' := _}

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

mathlib documentation

Algebraic structure on locally constant functions #