Algebraic structure on locally constant functions #

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

source

instance LocallyConstant.instZeroLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] :

Zero (LocallyConstant X Y)

source

instance LocallyConstant.instOneLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] :

One (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.coe_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] :

↑0 = 0

source

@[simp]

theorem LocallyConstant.coe_one {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] :

↑1 = 1

source

theorem LocallyConstant.zero_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] (x : X) :

↑0 x = 0

source

theorem LocallyConstant.one_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] (x : X) :

↑1 x = 1

source

theorem LocallyConstant.instNegLocallyConstant.proof_1 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [Neg Y] (f : LocallyConstant X Y) :

IsLocallyConstant (-f.toFun)

source

instance LocallyConstant.instNegLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] :

Neg (LocallyConstant X Y)

source

instance LocallyConstant.instInvLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] :

Inv (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.coe_neg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] (f : LocallyConstant X Y) :

↑(-f) = -↑f

source

@[simp]

theorem LocallyConstant.coe_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] (f : LocallyConstant X Y) :

↑f⁻¹ = (↑f)⁻¹

source

theorem LocallyConstant.neg_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] (f : LocallyConstant X Y) (x : X) :

↑(-f) x = -↑f x

source

theorem LocallyConstant.inv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] (f : LocallyConstant X Y) (x : X) :

↑f⁻¹ x = (↑f x)⁻¹

source

theorem LocallyConstant.instAddLocallyConstant.proof_1 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [Add Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

IsLocallyConstant (f.toFun + ↑g)

source

instance LocallyConstant.instAddLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] :

Add (LocallyConstant X Y)

source

instance LocallyConstant.instMulLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] :

Mul (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.coe_add {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

↑(f + g) = ↑f + ↑g

source

@[simp]

theorem LocallyConstant.coe_mul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

↑(f * g) = ↑f * ↑g

source

theorem LocallyConstant.add_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :

↑(f + g) x = ↑f x + ↑g x

source

theorem LocallyConstant.mul_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :

↑(f * g) x = ↑f x * ↑g x

source

theorem LocallyConstant.instAddZeroClassLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddZeroClass Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

instance LocallyConstant.instAddZeroClassLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

AddZeroClass (LocallyConstant X Y)

source

theorem LocallyConstant.instAddZeroClassLocallyConstant.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

↑0 = ↑0

source

theorem LocallyConstant.instAddZeroClassLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

instance LocallyConstant.instMulOneClassLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] :

MulOneClass (LocallyConstant X Y)

source

theorem LocallyConstant.coeFnAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

↑0 = ↑0

source

def LocallyConstant.coeFnAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

LocallyConstant X Y →+ X → Y

FunLike.coe as an AddMonoidHom.

Instances For

source

theorem LocallyConstant.coeFnAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddZeroClass Y] :

∀ (x x_1 : LocallyConstant X Y), ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) = ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1)

source

@[simp]

theorem LocallyConstant.coeFnMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] :

∀ (a : LocallyConstant X Y) (a_1 : X), ↑LocallyConstant.coeFnMonoidHom a a_1 = ↑a a_1

source

@[simp]

theorem LocallyConstant.coeFnAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

∀ (a : LocallyConstant X Y) (a_1 : X), ↑LocallyConstant.coeFnAddMonoidHom a a_1 = ↑a a_1

source

def LocallyConstant.coeFnMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] :

LocallyConstant X Y →* X → Y

FunLike.coe as a MonoidHom.

Instances For

source

theorem LocallyConstant.constAddMonoidHom.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

∀ (x x_1 : Y), ZeroHom.toFun { toFun := LocallyConstant.const X, map_zero' := (_ : LocallyConstant.const X 0 = LocallyConstant.const X 0) } (x + x_1) = ZeroHom.toFun { toFun := LocallyConstant.const X, map_zero' := (_ : LocallyConstant.const X 0 = LocallyConstant.const X 0) } (x + x_1)

source

def LocallyConstant.constAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

Y →+ LocallyConstant X Y

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

Instances For

source

theorem LocallyConstant.constAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] :

LocallyConstant.const X 0 = LocallyConstant.const X 0

source

@[simp]

theorem LocallyConstant.constMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (y : Y) :

↑LocallyConstant.constMonoidHom y = LocallyConstant.const X y

source

@[simp]

theorem LocallyConstant.constAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] (y : Y) :

↑LocallyConstant.constAddMonoidHom y = LocallyConstant.const X y

source

def LocallyConstant.constMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] :

Y →* LocallyConstant X Y

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

Instances For

source

instance LocallyConstant.instMulZeroClassLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulZeroClass Y] :

MulZeroClass (LocallyConstant X Y)

source

instance LocallyConstant.instMulZeroOneClassLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulZeroOneClass Y] :

MulZeroOneClass (LocallyConstant X Y)

source

noncomputable def LocallyConstant.charFn {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} (hU : IsClopen U) :

LocallyConstant 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.

Instances For

source

theorem LocallyConstant.coe_charFn {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} (hU : IsClopen U) :

↑(LocallyConstant.charFn Y hU) = Set.indicator U 1

source

theorem LocallyConstant.charFn_eq_one {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} [Nontrivial Y] (x : X) (hU : IsClopen U) :

↑(LocallyConstant.charFn Y hU) x = 1 ↔ x ∈ U

source

theorem LocallyConstant.charFn_eq_zero {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} [Nontrivial Y] (x : X) (hU : IsClopen U) :

↑(LocallyConstant.charFn Y hU) x = 0 ↔ ¬x ∈ U

source

theorem LocallyConstant.charFn_inj {X : Type u_1} (Y : Type u_2) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} {V : Set X} [Nontrivial Y] (hU : IsClopen U) (hV : IsClopen V) (h : LocallyConstant.charFn Y hU = LocallyConstant.charFn Y hV) :

U = V

source

theorem LocallyConstant.instSubLocallyConstant.proof_1 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [Sub Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

IsLocallyConstant (f.toFun - ↑g)

source

instance LocallyConstant.instSubLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] :

Sub (LocallyConstant X Y)

source

instance LocallyConstant.instDivLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] :

Div (LocallyConstant X Y)

source

theorem LocallyConstant.coe_sub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

↑(f - g) = ↑f - ↑g

source

theorem LocallyConstant.coe_div {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) :

↑(f / g) = ↑f / ↑g

source

theorem LocallyConstant.sub_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :

↑(f - g) x = ↑f x - ↑g x

source

theorem LocallyConstant.div_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] (f : LocallyConstant X Y) (g : LocallyConstant X Y) (x : X) :

↑(f / g) x = ↑f x / ↑g x

source

instance LocallyConstant.instAddSemigroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddSemigroup Y] :

AddSemigroup (LocallyConstant X Y)

source

theorem LocallyConstant.instAddSemigroupLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

theorem LocallyConstant.instAddSemigroupLocallyConstant.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddSemigroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

instance LocallyConstant.instSemigroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semigroup Y] :

Semigroup (LocallyConstant X Y)

source

instance LocallyConstant.instSemigroupWithZeroLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [SemigroupWithZero Y] :

SemigroupWithZero (LocallyConstant X Y)

source

instance LocallyConstant.instAddCommSemigroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddCommSemigroup Y] :

AddCommSemigroup (LocallyConstant X Y)

source

theorem LocallyConstant.instAddCommSemigroupLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

theorem LocallyConstant.instAddCommSemigroupLocallyConstant.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommSemigroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

instance LocallyConstant.instCommSemigroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CommSemigroup Y] :

CommSemigroup (LocallyConstant X Y)

source

instance LocallyConstant.vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [VAdd α Y] :

VAdd α (LocallyConstant X Y)

source

instance LocallyConstant.smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [SMul α Y] :

SMul α (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.coe_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [VAdd R Y] (r : R) (f : LocallyConstant X Y) :

↑(r +ᵥ f) = r +ᵥ ↑f

source

@[simp]

theorem LocallyConstant.coe_smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [SMul R Y] (r : R) (f : LocallyConstant X Y) :

↑(r • f) = r • ↑f

source

theorem LocallyConstant.vadd_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [VAdd R Y] (r : R) (f : LocallyConstant X Y) (x : X) :

↑(r +ᵥ f) x = r +ᵥ ↑f x

source

theorem LocallyConstant.smul_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [SMul R Y] (r : R) (f : LocallyConstant X Y) (x : X) :

↑(r • f) x = r • ↑f x

source

instance LocallyConstant.instPowLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [Pow Y α] :

Pow (LocallyConstant X Y) α

source

theorem LocallyConstant.instAddMonoidLocallyConstant.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddMonoid Y] :

↑0 = ↑0

source

theorem LocallyConstant.instAddMonoidLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddMonoid Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

instance LocallyConstant.instAddMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddMonoid Y] :

AddMonoid (LocallyConstant X Y)

source

theorem LocallyConstant.instAddMonoidLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddMonoid Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem LocallyConstant.instAddMonoidLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

instance LocallyConstant.instMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Monoid Y] :

Monoid (LocallyConstant X Y)

source

instance LocallyConstant.instNatCastLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NatCast Y] :

NatCast (LocallyConstant X Y)

source

instance LocallyConstant.instIntCastLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [IntCast Y] :

IntCast (LocallyConstant X Y)

source

instance LocallyConstant.instAddMonoidWithOneLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddMonoidWithOne Y] :

AddMonoidWithOne (LocallyConstant X Y)

source

theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommMonoid Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommMonoid Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

instance LocallyConstant.instAddCommMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddCommMonoid Y] :

AddCommMonoid (LocallyConstant X Y)

source

theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddCommMonoid Y] :

↑0 = ↑0

source

theorem LocallyConstant.instAddCommMonoidLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

instance LocallyConstant.instCommMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CommMonoid Y] :

CommMonoid (LocallyConstant X Y)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_6 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_5 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x - x_1) = ↑(x - x_1)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddGroup Y] :

↑0 = ↑0

source

instance LocallyConstant.instAddGroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddGroup Y] :

AddGroup (LocallyConstant X Y)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_7 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

theorem LocallyConstant.instAddGroupLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :

∀ (x : LocallyConstant X Y), ↑(-x) = ↑(-x)

source

instance LocallyConstant.instGroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Group Y] :

Group (LocallyConstant X Y)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_7 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] :

Function.Injective FunLike.coe

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_6 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :

∀ (x : LocallyConstant X Y) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :

∀ (x : LocallyConstant X Y), ↑(-x) = ↑(-x)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddCommGroup Y] :

↑0 = ↑0

source

instance LocallyConstant.instAddCommGroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddCommGroup Y] :

AddCommGroup (LocallyConstant X Y)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_5 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x - x_1) = ↑(x - x_1)

source

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_3 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :

∀ (x x_1 : LocallyConstant X Y), ↑(x + x_1) = ↑(x + x_1)

source

instance LocallyConstant.instCommGroupLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CommGroup Y] :

CommGroup (LocallyConstant X Y)

source

instance LocallyConstant.instDistribLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Distrib Y] :

Distrib (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalNonAssocSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalNonAssocSemiring Y] :

NonUnitalNonAssocSemiring (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalSemiring Y] :

NonUnitalSemiring (LocallyConstant X Y)

source

instance LocallyConstant.instNonAssocSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonAssocSemiring Y] :

NonAssocSemiring (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.constRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonAssocSemiring Y] (y : Y) :

↑LocallyConstant.constRingHom y = LocallyConstant.const X y

source

def LocallyConstant.constRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonAssocSemiring Y] :

Y →+* LocallyConstant X Y

The constant-function embedding, as a ring hom.

Instances For

source

instance LocallyConstant.instSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] :

Semiring (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalCommSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalCommSemiring Y] :

NonUnitalCommSemiring (LocallyConstant X Y)

source

instance LocallyConstant.instCommSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CommSemiring Y] :

CommSemiring (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalNonAssocRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalNonAssocRing Y] :

NonUnitalNonAssocRing (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalRing Y] :

NonUnitalRing (LocallyConstant X Y)

source

instance LocallyConstant.instNonAssocRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonAssocRing Y] :

NonAssocRing (LocallyConstant X Y)

source

instance LocallyConstant.instRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Ring Y] :

Ring (LocallyConstant X Y)

source

instance LocallyConstant.instNonUnitalCommRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [NonUnitalCommRing Y] :

NonUnitalCommRing (LocallyConstant X Y)

source

instance LocallyConstant.instCommRingLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CommRing Y] :

CommRing (LocallyConstant X Y)

source

instance LocallyConstant.instMulActionLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [Monoid R] [MulAction R Y] :

MulAction R (LocallyConstant X Y)

source

instance LocallyConstant.instDistribMulActionLocallyConstantInstAddMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [Monoid R] [AddMonoid Y] [DistribMulAction R Y] :

DistribMulAction R (LocallyConstant X Y)

source

instance LocallyConstant.instModuleLocallyConstantInstAddCommMonoidLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [Semiring R] [AddCommMonoid Y] [Module R Y] :

Module R (LocallyConstant X Y)

source

instance LocallyConstant.instAlgebraLocallyConstantInstSemiringLocallyConstant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [CommSemiring R] [Semiring Y] [Algebra R Y] :

Algebra R (LocallyConstant X Y)

source

@[simp]

theorem LocallyConstant.coe_algebraMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [CommSemiring R] [Semiring Y] [Algebra R Y] (r : R) :

↑(↑(algebraMap R (LocallyConstant X Y)) r) = ↑(algebraMap R (X → Y)) r

source

@[simp]

theorem LocallyConstant.coeFnRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] :

∀ (a : LocallyConstant X Y) (a_1 : X), ↑LocallyConstant.coeFnRingHom a a_1 = ↑a a_1

source

def LocallyConstant.coeFnRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] :

LocallyConstant X Y →+* X → Y

FunLike.coe as a RingHom.

Instances For

source

@[simp]

theorem LocallyConstant.coeFnₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] :

∀ (a : LocallyConstant X Y) (a_1 : X), ↑(LocallyConstant.coeFnₗ R) a a_1 = ↑a a_1

source

def LocallyConstant.coeFnₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] :

LocallyConstant X Y →ₗ[R] X → Y

FunLike.coe as a linear map.

Instances For

source

@[simp]

theorem LocallyConstant.coeFnAlgHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] :

∀ (a : LocallyConstant X Y) (a_1 : X), ↑(LocallyConstant.coeFnAlgHom R) a a_1 = ↑a a_1

source

def LocallyConstant.coeFnAlgHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] :

LocallyConstant X Y →ₐ[R] X → Y

FunLike.coe as an AlgHom.

Instances For

source

def LocallyConstant.evalAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] (x : X) :

LocallyConstant X Y →+ Y

Evaluation as an AddMonoidHom

Instances For

source

@[simp]

theorem LocallyConstant.evalMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (x : X) :

∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalMonoidHom x) a = ↑a x

source

@[simp]

theorem LocallyConstant.evalAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] (x : X) :

∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalAddMonoidHom x) a = ↑a x

source

def LocallyConstant.evalMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (x : X) :

LocallyConstant X Y →* Y

Evaluation as a MonoidHom

Instances For

source

@[simp]

theorem LocallyConstant.evalₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] (x : X) :

∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalₗ R x) a = ↑a x

source

def LocallyConstant.evalₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [Semiring R] [AddCommMonoid Y] [Module R Y] (x : X) :

LocallyConstant X Y →ₗ[R] Y

Evaluation as a linear map

Instances For

source

@[simp]

theorem LocallyConstant.evalRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] (x : X) :

∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalRingHom x) a = ↑a x

source

def LocallyConstant.evalRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Semiring Y] (x : X) :

LocallyConstant X Y →+* Y

Evaluation as a RingHom

Instances For

source

@[simp]

theorem LocallyConstant.evalₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] (x : X) :

∀ (a : LocallyConstant X Y), ↑(LocallyConstant.evalₐ R x) a = ↑a x

source

def LocallyConstant.evalₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_4) [CommSemiring R] [Semiring Y] [Algebra R Y] (x : X) :

LocallyConstant X Y →ₐ[R] Y

Evaluation as an AlgHom

Instances For

source

noncomputable def LocallyConstant.comapAddHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (f : X → Y) (hf : Continuous f) :

AddHom (LocallyConstant Y Z) (LocallyConstant X Z)

LocallyConstant.comap as an AddHom.

Instances For

source

theorem LocallyConstant.comapAddHom.proof_1 {X : Type u_3} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_1} [Add Z] (f : X → Y) (hf : Continuous f) (r : LocallyConstant Y Z) (s : LocallyConstant Y Z) :

LocallyConstant.comap f (r + s) = LocallyConstant.comap f r + LocallyConstant.comap f s

source

@[simp]

theorem LocallyConstant.comapAddHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapAddHom f hf) a = LocallyConstant.comap f a

source

@[simp]

theorem LocallyConstant.comapMulHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapMulHom f hf) a = LocallyConstant.comap f a

source

noncomputable def LocallyConstant.comapMulHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →ₙ* LocallyConstant X Z

LocallyConstant.comap as a MulHom.

Instances For

source

theorem LocallyConstant.comapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_2} [AddZeroClass Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant.comap f 0 = 0

source

noncomputable def LocallyConstant.comapAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [AddZeroClass Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →+ LocallyConstant X Z

LocallyConstant.comap as an AddMonoidHom.

Instances For

source

theorem LocallyConstant.comapAddMonoidHom.proof_2 {X : Type u_3} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_1} [AddZeroClass Z] (f : X → Y) (hf : Continuous f) (x : LocallyConstant Y Z) (y : LocallyConstant Y Z) :

↑(LocallyConstant.comapAddHom f hf) (x + y) = ↑(LocallyConstant.comapAddHom f hf) x + ↑(LocallyConstant.comapAddHom f hf) y

source

@[simp]

theorem LocallyConstant.comapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [AddZeroClass Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapAddMonoidHom f hf) a = LocallyConstant.comap f a

source

@[simp]

theorem LocallyConstant.comapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [MulOneClass Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapMonoidHom f hf) a = LocallyConstant.comap f a

source

noncomputable def LocallyConstant.comapMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [MulOneClass Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →* LocallyConstant X Z

LocallyConstant.comap as a MonoidHom.

Instances For

source

@[simp]

theorem LocallyConstant.comapₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapₗ R f hf) a = LocallyConstant.comap f a

source

noncomputable def LocallyConstant.comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →ₗ[R] LocallyConstant X Z

LocallyConstant.comap as a linear map.

Instances For

source

@[simp]

theorem LocallyConstant.comapRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapRingHom f hf) a = LocallyConstant.comap f a

source

noncomputable def LocallyConstant.comapRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →+* LocallyConstant X Z

LocallyConstant.comap as a RingHom.

Instances For

source

@[simp]

theorem LocallyConstant.comapₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : X → Y) (hf : Continuous f) :

∀ (a : LocallyConstant Y Z), ↑(LocallyConstant.comapₐ R f hf) a = LocallyConstant.comap f a

source

noncomputable def LocallyConstant.comapₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : X → Y) (hf : Continuous f) :

LocallyConstant Y Z →ₐ[R] LocallyConstant X Z

LocallyConstant.comap as an AlgHom

Instances For

source

theorem LocallyConstant.ker_comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_3} [TopologicalSpace Y] {Z : Type u_4} [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y) (hf : Continuous f) (hfs : Function.Surjective f) :

LinearMap.ker (LocallyConstant.comapₗ R f hf) = ⊥

source

theorem LocallyConstant.congrLeftAddEquiv.proof_1 {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_1} [Add Z] (e : X ≃ₜ Y) (x : LocallyConstant X Z) (y : LocallyConstant X Z) :

↑(LocallyConstant.comapAddHom ↑(Homeomorph.symm e) (_ : Continuous ↑(Homeomorph.symm e))) (x + y) = ↑(LocallyConstant.comapAddHom ↑(Homeomorph.symm e) (_ : Continuous ↑(Homeomorph.symm e))) x + ↑(LocallyConstant.comapAddHom ↑(Homeomorph.symm e) (_ : Continuous ↑(Homeomorph.symm e))) y

source

noncomputable def LocallyConstant.congrLeftAddEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (e : X ≃ₜ Y) :

LocallyConstant X Z ≃+ LocallyConstant Y Z

LocallyConstant.congrLeft as an AddEquiv.

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftMulEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeftMulEquiv e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

source

@[simp]

theorem LocallyConstant.congrLeftAddEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant Y Z), ↑(AddEquiv.symm (LocallyConstant.congrLeftAddEquiv e)) a = LocallyConstant.comap (↑e) a

source

@[simp]

theorem LocallyConstant.congrLeftAddEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Add Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeftAddEquiv e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

source

@[simp]

theorem LocallyConstant.congrLeftMulEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant Y Z), ↑(MulEquiv.symm (LocallyConstant.congrLeftMulEquiv e)) a = LocallyConstant.comap (↑e) a

source

noncomputable def LocallyConstant.congrLeftMulEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Mul Z] (e : X ≃ₜ Y) :

LocallyConstant X Z ≃* LocallyConstant Y Z

LocallyConstant.congrLeft as a MulEquiv.

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftₗ_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant Y Z), ↑(LinearEquiv.symm (LocallyConstant.congrLeftₗ R e)) a = LocallyConstant.comap (↑e) a

source

@[simp]

theorem LocallyConstant.congrLeftₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeftₗ R e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

source

noncomputable def LocallyConstant.congrLeftₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [Semiring R] [AddCommMonoid Z] [Module R Z] (e : X ≃ₜ Y) :

LocallyConstant X Z ≃ₗ[R] LocallyConstant Y Z

LocallyConstant.congrLeft as a linear equivalence.

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeftRingEquiv e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

source

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant Y Z), ↑(RingEquiv.symm (LocallyConstant.congrLeftRingEquiv e)) a = LocallyConstant.comap (↑e) a

source

noncomputable def LocallyConstant.congrLeftRingEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_4} [Semiring Z] (e : X ≃ₜ Y) :

LocallyConstant X Z ≃+* LocallyConstant Y Z

LocallyConstant.congrLeft as a RingEquiv.

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftₐ_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant Y Z), ↑(AlgEquiv.symm (LocallyConstant.congrLeftₐ R e)) a = LocallyConstant.comap (↑e) a

source

@[simp]

theorem LocallyConstant.congrLeftₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :

∀ (a : LocallyConstant X Z), ↑(LocallyConstant.congrLeftₐ R e) a = LocallyConstant.comap (↑(Homeomorph.symm e)) a

source

noncomputable def LocallyConstant.congrLeftₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_5} (R : Type u_4) [CommSemiring R] [Semiring Z] [Algebra R Z] (e : X ≃ₜ Y) :

LocallyConstant X Z ≃ₐ[R] LocallyConstant Y Z

LocallyConstant.congrLeft as an AlgEquiv.

Instances For