Algebraic structure on locally constant functions

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

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

Equations

• LocallyConstant.instZeroLocallyConstant = { zero := LocallyConstant.const X 0 }

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

Equations

• LocallyConstant.instOneLocallyConstant = { one := LocallyConstant.const X 1 }

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• LocallyConstant.instNegLocallyConstant = { neg := fun (f : LocallyConstant X Y) => { toFun := -⇑f, isLocallyConstant := ⋯ } }

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

Equations

• LocallyConstant.instInvLocallyConstant = { inv := fun (f : LocallyConstant X Y) => { toFun := (⇑f)⁻¹, isLocallyConstant := ⋯ } }

@[simp]

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

@[simp]

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

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

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)⁻¹

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)

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

Equations

• LocallyConstant.instAddLocallyConstant = { add := fun (f g : LocallyConstant X Y) => { toFun := ⇑f + ⇑g, isLocallyConstant := ⋯ } }

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

Equations

• LocallyConstant.instMulLocallyConstant = { mul := fun (f g : LocallyConstant X Y) => { toFun := ⇑f * ⇑g, isLocallyConstant := ⋯ } }

@[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

@[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

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

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

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)

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

Equations

• LocallyConstant.instAddZeroClassLocallyConstant = Function.Injective.addZeroClass DFunLike.coe ⋯ ⋯ ⋯

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

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

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

Equations

• LocallyConstant.instMulOneClassLocallyConstant = Function.Injective.mulOneClass DFunLike.coe ⋯ ⋯ ⋯

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

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

DFunLike.coe as an AddMonoidHom.

Equations

• LocallyConstant.coeFnAddMonoidHom = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }

theorem LocallyConstant.coeFnAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddZeroClass Y] : ∀ (x x_1 : LocallyConstant X Y), { toFun := DFunLike.coe, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := DFunLike.coe, map_zero' := ⋯ }.toFun (x + x_1)

@[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

@[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

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

DFunLike.coe as a MonoidHom.

Equations

• LocallyConstant.coeFnMonoidHom = { toOneHom := { toFun := DFunLike.coe, map_one' := ⋯ }, map_mul' := ⋯ }

theorem LocallyConstant.constAddMonoidHom.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddZeroClass Y] : ∀ (x x_1 : Y), { toFun := LocallyConstant.const X, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := LocallyConstant.const X, map_zero' := ⋯ }.toFun (x + x_1)

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.

Equations

• LocallyConstant.constAddMonoidHom = { toZeroHom := { toFun := LocallyConstant.const X, map_zero' := ⋯ }, map_add' := ⋯ }

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

@[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

@[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

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.

Equations

• LocallyConstant.constMonoidHom = { toOneHom := { toFun := LocallyConstant.const X, map_one' := ⋯ }, map_mul' := ⋯ }

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

Equations

• LocallyConstant.instMulZeroClassLocallyConstant = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instMulZeroOneClassLocallyConstant = Function.Injective.mulZeroOneClass DFunLike.coe ⋯ ⋯ ⋯ ⋯

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.

Equations

• LocallyConstant.charFn Y hU = LocallyConstant.indicator 1 hU

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

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

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

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

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)

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

Equations

• LocallyConstant.instSubLocallyConstant = { sub := fun (f g : LocallyConstant X Y) => { toFun := ⇑f - ⇑g, isLocallyConstant := ⋯ } }

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

Equations

• LocallyConstant.instDivLocallyConstant = { div := fun (f g : LocallyConstant X Y) => { toFun := ⇑f / ⇑g, isLocallyConstant := ⋯ } }

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

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

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

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

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

Equations

• LocallyConstant.instAddSemigroupLocallyConstant = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯

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

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)

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

Equations

• LocallyConstant.instSemigroupLocallyConstant = Function.Injective.semigroup DFunLike.coe ⋯ ⋯

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

Equations

• LocallyConstant.instSemigroupWithZeroLocallyConstant = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instAddCommSemigroupLocallyConstant = Function.Injective.addCommSemigroup DFunLike.coe ⋯ ⋯

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

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)

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

Equations

• LocallyConstant.instCommSemigroupLocallyConstant = Function.Injective.commSemigroup DFunLike.coe ⋯ ⋯

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

Equations

• LocallyConstant.vadd = { vadd := fun (n : α) (f : LocallyConstant X Y) => LocallyConstant.map (fun (x : Y) => n +ᵥ x) f }

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

Equations

• LocallyConstant.smul = { smul := fun (n : α) (f : LocallyConstant X Y) => LocallyConstant.map (fun (x : Y) => n • x) f }

@[simp]

theorem LocallyConstant.coe_vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_4} [VAdd R Y] (r : R) (f : LocallyConstant X Y) : ⇑(r +ᵥ f) = r +ᵥ ⇑f

@[simp]

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

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

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

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

Equations

• LocallyConstant.instPowLocallyConstant = { pow := fun (f : LocallyConstant X Y) (n : α) => LocallyConstant.map (fun (x : Y) => x ^ n) f }

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

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)

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

Equations

• LocallyConstant.instAddMonoidLocallyConstant = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

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)

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

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

Equations

• LocallyConstant.instMonoidLocallyConstant = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNatCastLocallyConstant = { natCast := fun (n : ℕ) => LocallyConstant.const X ↑n }

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

Equations

• LocallyConstant.instIntCastLocallyConstant = { intCast := fun (n : ℤ) => LocallyConstant.const X ↑n }

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

Equations

• LocallyConstant.instAddMonoidWithOneLocallyConstant = Function.Injective.addMonoidWithOne DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

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)

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

Equations

• LocallyConstant.instAddCommMonoidLocallyConstant = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

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

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

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

Equations

• LocallyConstant.instCommMonoidLocallyConstant = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

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)

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)

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

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

Equations

• LocallyConstant.instAddGroupLocallyConstant = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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)

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)

theorem LocallyConstant.instAddGroupLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] : ∀ (x : LocallyConstant X Y), ⇑(-x) = ⇑(-x)

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

Equations

• LocallyConstant.instGroupLocallyConstant = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

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

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)

theorem LocallyConstant.instAddCommGroupLocallyConstant.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] : ∀ (x : LocallyConstant X Y), ⇑(-x) = ⇑(-x)

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

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

Equations

• LocallyConstant.instAddCommGroupLocallyConstant = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

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)

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

Equations

• LocallyConstant.instCommGroupLocallyConstant = Function.Injective.commGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instDistribLocallyConstant = Function.Injective.distrib DFunLike.coe ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalNonAssocSemiringLocallyConstant = Function.Injective.nonUnitalNonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalSemiringLocallyConstant = Function.Injective.nonUnitalSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonAssocSemiringLocallyConstant = Function.Injective.nonAssocSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• LocallyConstant.instSemiringLocallyConstant = Function.Injective.semiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalCommSemiringLocallyConstant = Function.Injective.nonUnitalCommSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instCommSemiringLocallyConstant = Function.Injective.commSemiring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalNonAssocRingLocallyConstant = Function.Injective.nonUnitalNonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalRingLocallyConstant = Function.Injective.nonUnitalRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonAssocRingLocallyConstant = Function.Injective.nonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instRingLocallyConstant = Function.Injective.ring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instNonUnitalCommRingLocallyConstant = Function.Injective.nonUnitalCommRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instCommRingLocallyConstant = Function.Injective.commRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• LocallyConstant.instMulActionLocallyConstant = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

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

Equations

• LocallyConstant.instDistribMulActionLocallyConstantInstAddMonoidLocallyConstant = Function.Injective.distribMulAction LocallyConstant.coeFnAddMonoidHom ⋯ ⋯

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

Equations

• LocallyConstant.instModuleLocallyConstantInstAddCommMonoidLocallyConstant = Function.Injective.module R LocallyConstant.coeFnAddMonoidHom ⋯ ⋯

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

Equations

• LocallyConstant.instAlgebraLocallyConstantInstSemiringLocallyConstant = Algebra.mk (RingHom.comp LocallyConstant.constRingHom (algebraMap R Y)) ⋯ ⋯

@[simp]

theorem LocallyConstant.coe_algebraMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_5} [CommSemiring R] [Semiring Y] [Algebra R Y] (r : R) : ⇑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R (X → Y)) r

@[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

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

DFunLike.coe as a RingHom.

Equations

• LocallyConstant.coeFnRingHom = let __spread.0 := LocallyConstant.coeFnAddMonoidHom; { toMonoidHom := LocallyConstant.coeFnMonoidHom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LocallyConstant.coeFnₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [Semiring R] [AddCommMonoid Y] [Module R Y] : ∀ (a : LocallyConstant X Y) (a_1 : X), (LocallyConstant.coeFnₗ R) a a_1 = a a_1

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

DFunLike.coe as a linear map.

Equations

• LocallyConstant.coeFnₗ R = { toAddHom := ↑LocallyConstant.coeFnAddMonoidHom, map_smul' := ⋯ }

@[simp]

theorem LocallyConstant.coeFnAlgHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [CommSemiring R] [Semiring Y] [Algebra R Y] : ∀ (a : LocallyConstant X Y) (a_1 : X), (LocallyConstant.coeFnAlgHom R) a a_1 = a a_1

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

DFunLike.coe as an AlgHom.

Equations

• LocallyConstant.coeFnAlgHom R = { toRingHom := LocallyConstant.coeFnRingHom, commutes' := ⋯ }

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

Equations

• LocallyConstant.evalAddMonoidHom x = AddMonoidHom.comp (Pi.evalAddMonoidHom (fun (a : X) => Y) x) LocallyConstant.coeFnAddMonoidHom

@[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

@[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

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

Equations

• LocallyConstant.evalMonoidHom x = MonoidHom.comp (Pi.evalMonoidHom (fun (a : X) => Y) x) LocallyConstant.coeFnMonoidHom

@[simp]

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

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

Evaluation as a linear map

Equations

• LocallyConstant.evalₗ R x = LinearMap.comp (LinearMap.proj x) (LocallyConstant.coeFnₗ R)

@[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

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

Equations

• LocallyConstant.evalRingHom x = RingHom.comp (Pi.evalRingHom (fun (a : X) => Y) x) LocallyConstant.coeFnRingHom

@[simp]

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

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

Evaluation as an AlgHom

Equations

• LocallyConstant.evalₐ R x = AlgHom.comp (Pi.evalAlgHom R (fun (a : X) => Y) x) (LocallyConstant.coeFnAlgHom R)

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

LocallyConstant.comap as an AddHom.

Equations

• LocallyConstant.comapAddHom f hf = { toFun := LocallyConstant.comap f, map_add' := ⋯ }

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

@[simp]

theorem LocallyConstant.comapAddHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Add Z] (f : X → Y) (hf : Continuous f) : ∀ (a : LocallyConstant Y Z), (LocallyConstant.comapAddHom f hf) a = LocallyConstant.comap f a

@[simp]

theorem LocallyConstant.comapMulHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Mul Z] (f : X → Y) (hf : Continuous f) : ∀ (a : LocallyConstant Y Z), (LocallyConstant.comapMulHom f hf) a = LocallyConstant.comap f a

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

LocallyConstant.comap as a MulHom.

Equations

• LocallyConstant.comapMulHom f hf = { toFun := LocallyConstant.comap f, map_mul' := ⋯ }

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

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

LocallyConstant.comap as an AddMonoidHom.

Equations

• LocallyConstant.comapAddMonoidHom f hf = { toZeroHom := { toFun := LocallyConstant.comap f, map_zero' := ⋯ }, map_add' := ⋯ }

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

@[simp]

theorem LocallyConstant.comapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [AddZeroClass Z] (f : X → Y) (hf : Continuous f) : ∀ (a : LocallyConstant Y Z), (LocallyConstant.comapAddMonoidHom f hf) a = LocallyConstant.comap f a

@[simp]

theorem LocallyConstant.comapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [MulOneClass Z] (f : X → Y) (hf : Continuous f) : ∀ (a : LocallyConstant Y Z), (LocallyConstant.comapMonoidHom f hf) a = LocallyConstant.comap f a

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

LocallyConstant.comap as a MonoidHom.

Equations

• LocallyConstant.comapMonoidHom f hf = { toOneHom := { toFun := LocallyConstant.comap f, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem LocallyConstant.comapₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

noncomputable def LocallyConstant.comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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.

Equations

• LocallyConstant.comapₗ R f hf = { toAddHom := { toFun := LocallyConstant.comap f, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem LocallyConstant.comapRingHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (f : X → Y) (hf : Continuous f) : ∀ (a : LocallyConstant Y Z), (LocallyConstant.comapRingHom f hf) a = LocallyConstant.comap f a

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

LocallyConstant.comap as a RingHom.

Equations

• LocallyConstant.comapRingHom f hf = let __spread.0 := LocallyConstant.comapAddMonoidHom f hf; { toMonoidHom := LocallyConstant.comapMonoidHom f hf, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LocallyConstant.comapₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

noncomputable def LocallyConstant.comapₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

Equations

• LocallyConstant.comapₐ R f hf = { toRingHom := LocallyConstant.comapRingHom f hf, commutes' := ⋯ }

theorem LocallyConstant.ker_comapₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_5} [TopologicalSpace Y] {Z : Type u_6} [Semiring R] [AddCommMonoid Z] [Module R Z] (f : X → Y) (hf : Continuous f) (hfs : Function.Surjective f) : LinearMap.ker (LocallyConstant.comapₗ R f hf) = ⊥

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) ⋯) (x + y) = (LocallyConstant.comapAddHom ⇑(Homeomorph.symm e) ⋯) x + (LocallyConstant.comapAddHom ⇑(Homeomorph.symm e) ⋯) y

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

LocallyConstant.congrLeft as an AddEquiv.

Equations

• LocallyConstant.congrLeftAddEquiv e = { toEquiv := LocallyConstant.congrLeft e, map_add' := ⋯ }

@[simp]

theorem LocallyConstant.congrLeftMulEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Mul Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant X Z), (LocallyConstant.congrLeftMulEquiv e) a = LocallyConstant.comap (⇑(Homeomorph.symm e)) a

@[simp]

theorem LocallyConstant.congrLeftAddEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Add Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant Y Z), (AddEquiv.symm (LocallyConstant.congrLeftAddEquiv e)) a = LocallyConstant.comap (⇑e) a

@[simp]

theorem LocallyConstant.congrLeftAddEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Add Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant X Z), (LocallyConstant.congrLeftAddEquiv e) a = LocallyConstant.comap (⇑(Homeomorph.symm e)) a

@[simp]

theorem LocallyConstant.congrLeftMulEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Mul Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant Y Z), (MulEquiv.symm (LocallyConstant.congrLeftMulEquiv e)) a = LocallyConstant.comap (⇑e) a

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

LocallyConstant.congrLeft as a MulEquiv.

Equations

• LocallyConstant.congrLeftMulEquiv e = { toEquiv := LocallyConstant.congrLeft e, map_mul' := ⋯ }

@[simp]

theorem LocallyConstant.congrLeftₗ_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

@[simp]

theorem LocallyConstant.congrLeftₗ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

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

LocallyConstant.congrLeft as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant X Z), (LocallyConstant.congrLeftRingEquiv e) a = LocallyConstant.comap (⇑(Homeomorph.symm e)) a

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (e : X ≃ₜ Y) : ∀ (a : LocallyConstant Y Z), (RingEquiv.symm (LocallyConstant.congrLeftRingEquiv e)) a = LocallyConstant.comap (⇑e) a

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

LocallyConstant.congrLeft as a RingEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocallyConstant.congrLeftₐ_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

@[simp]

theorem LocallyConstant.congrLeftₐ_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [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

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

LocallyConstant.congrLeft as an AlgEquiv.

Equations

• LocallyConstant.congrLeftₐ R e = let __spread.0 := LocallyConstant.comapₐ R ⇑(Homeomorph.symm e) ⋯; { toEquiv := LocallyConstant.congrLeft e, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }