Algebraic structure on locally constant functions #

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

source

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

One (LocallyConstant X Y)

Equations

source

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

Zero (LocallyConstant X Y)

Equations

source

@[simp]

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

⇑1 = 1

source

@[simp]

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

⇑0 = 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.zero_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Zero Y] (x : X) :

0 x = 0

source

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

Inv (LocallyConstant X Y)

Equations

source

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

Neg (LocallyConstant X Y)

Equations

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

@[simp]

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

⇑(-f) = -⇑f

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

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

Mul (LocallyConstant X Y)

Equations

source

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

Add (LocallyConstant X Y)

Equations

source

@[simp]

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

⇑(f * g) = ⇑f * ⇑g

source

@[simp]

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

⇑(f + g) = ⇑f + ⇑g

source

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

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

source

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

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

source

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

MulOneClass (LocallyConstant X Y)

Equations

source

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

AddZeroClass (LocallyConstant X Y)

Equations

source

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

Instances For

source

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

Instances For

source

@[simp]

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

coeFnMonoidHom a✝ a = a✝ a

source

@[simp]

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

coeFnAddMonoidHom a✝ a = a✝ a

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.

Equations

Instances For

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.

Equations

Instances For

source

@[simp]

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

constAddMonoidHom y = const X y

source

@[simp]

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

constMonoidHom y = const X y

source

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

MulZeroClass (LocallyConstant X Y)

Equations

source

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

MulZeroOneClass (LocallyConstant X Y)

Equations

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.

Equations

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) :

⇑(charFn Y hU) = U.indicator 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) :

(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) :

(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 V : Set X} [Nontrivial Y] (hU : IsClopen U) (hV : IsClopen V) (h : charFn Y hU = charFn Y hV) :

U = V

source

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

Div (LocallyConstant X Y)

Equations

source

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

Sub (LocallyConstant X Y)

Equations

source

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

⇑(f / g) = ⇑f / ⇑g

source

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

⇑(f - g) = ⇑f - ⇑g

source

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

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

source

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

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

source

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

Semigroup (LocallyConstant X Y)

Equations

source

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

AddSemigroup (LocallyConstant X Y)

Equations

source

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

SemigroupWithZero (LocallyConstant X Y)

Equations

source

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

CommSemigroup (LocallyConstant X Y)

Equations

source

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

AddCommSemigroup (LocallyConstant X Y)

Equations

source

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

SMul α (LocallyConstant X Y)

Equations

source

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

VAdd α (LocallyConstant X Y)

Equations

source

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

source

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

source

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

source

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

source

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

Pow (LocallyConstant X Y) α

Equations

source

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

Monoid (LocallyConstant X Y)

Equations

source

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

AddMonoid (LocallyConstant X Y)

Equations

source

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

NatCast (LocallyConstant X Y)

Equations

source

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

IntCast (LocallyConstant X Y)

Equations

source

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

AddMonoidWithOne (LocallyConstant X Y)

Equations

source

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

CommMonoid (LocallyConstant X Y)

Equations

source

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

AddCommMonoid (LocallyConstant X Y)

Equations

source

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

Group (LocallyConstant X Y)

Equations

source

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

AddGroup (LocallyConstant X Y)

Equations

source

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

CommGroup (LocallyConstant X Y)

Equations

source

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

AddCommGroup (LocallyConstant X Y)

Equations

source

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

Distrib (LocallyConstant X Y)

Equations

source

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

NonUnitalNonAssocSemiring (LocallyConstant X Y)

Equations

source

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

NonUnitalSemiring (LocallyConstant X Y)

Equations

source

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

NonAssocSemiring (LocallyConstant X Y)

Equations

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.

Equations

Instances For

source

@[simp]

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

constRingHom y = const X y

source

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

Semiring (LocallyConstant X Y)

Equations

source

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

NonUnitalCommSemiring (LocallyConstant X Y)

Equations

source

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

CommSemiring (LocallyConstant X Y)

Equations

source

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

NonUnitalNonAssocRing (LocallyConstant X Y)

Equations

source

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

NonUnitalRing (LocallyConstant X Y)

Equations

source

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

NonAssocRing (LocallyConstant X Y)

Equations

source

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

Ring (LocallyConstant X Y)

Equations

source

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

NonUnitalCommRing (LocallyConstant X Y)

Equations

source

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

CommRing (LocallyConstant X Y)

Equations

source

instance LocallyConstant.instMulAction {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

source

instance LocallyConstant.instDistribMulAction {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

source

instance LocallyConstant.instModule {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

source

instance LocallyConstant.instAlgebra {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

source

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

source

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

Instances For

source

@[simp]

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

coeFnRingHom a✝ a = a✝ a

source

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

Instances For

source

@[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✝¹ : X) :

(coeFnₗ R) a✝ a✝¹ = a✝ a✝¹

source

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

Instances For

source

@[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 : X) :

(coeFnAlgHom R) a✝ a = a✝ a

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

Equations

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

Equations

Instances For

source

@[simp]

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

(evalAddMonoidHom x) a✝ = a✝ x

source

@[simp]

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

(evalMonoidHom x) a✝ = a✝ x

source

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

Instances For

source

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

(evalₗ R 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

Equations

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) :

(evalRingHom x) a✝ = a✝ x

source

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

Instances For

source

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

(evalₐ R x) a✝ = a✝ x

source

def LocallyConstant.comapMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [MulOneClass Z] (f : C(X, Y)) :

LocallyConstant Y Z →* LocallyConstant X Z

LocallyConstant.comap as a MonoidHom.

Equations

Instances For

source

def LocallyConstant.comapAddMonoidHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [AddZeroClass Z] (f : C(X, Y)) :

LocallyConstant Y Z →+ LocallyConstant X Z

LocallyConstant.comap as an AddMonoidHom.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.comapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [AddZeroClass Z] (f : C(X, Y)) (g : LocallyConstant Y Z) :

(comapAddMonoidHom f) g = comap f g

source

@[simp]

theorem LocallyConstant.comapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [MulOneClass Z] (f : C(X, Y)) (g : LocallyConstant Y Z) :

(comapMonoidHom f) g = comap f g

source

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 : C(X, Y)) :

LocallyConstant Y Z →ₗ[R] LocallyConstant X Z

LocallyConstant.comap as a linear map.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.comapₗ_apply_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 : C(X, Y)) (g : LocallyConstant Y Z) (a✝ : X) :

((comapₗ R f) g) a✝ = g (f a✝)

source

def LocallyConstant.comapRingHom {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (f : C(X, Y)) :

LocallyConstant Y Z →+* LocallyConstant X Z

LocallyConstant.comap as a RingHom.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.comapRingHom_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (f : C(X, Y)) (g : LocallyConstant Y Z) (a✝ : X) :

((comapRingHom f) g) a✝ = g (f a✝)

source

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 : C(X, Y)) :

LocallyConstant Y Z →ₐ[R] LocallyConstant X Z

LocallyConstant.comap as an AlgHom

Equations

Instances For

source

@[simp]

theorem LocallyConstant.comapₐ_apply_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 : C(X, Y)) (g : LocallyConstant Y Z) (a✝ : X) :

((comapₐ R f) g) a✝ = g (f a✝)

source

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 : C(X, Y)) (hfs : Function.Surjective ⇑f) :

LinearMap.ker (comapₗ R f) = ⊥

source

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

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftₗ_symm_apply_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) (a✝¹ : X) :

((congrLeftₗ R e).symm a✝) a✝¹ = a✝ (e a✝¹)

source

@[simp]

theorem LocallyConstant.congrLeftₗ_apply_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) (g : LocallyConstant X Z) (a✝ : Y) :

((congrLeftₗ R e) g) a✝ = g (e.symm a✝)

source

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

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (e : X ≃ₜ Y) (g : LocallyConstant Y Z) (a✝ : X) :

((congrLeftRingEquiv e).symm g) a✝ = g (e a✝)

source

@[simp]

theorem LocallyConstant.congrLeftRingEquiv_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (e : X ≃ₜ Y) (g : LocallyConstant X Z) (a✝ : Y) :

((congrLeftRingEquiv e) g) a✝ = g (e.symm a✝)

source

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

Instances For

source

@[simp]

theorem LocallyConstant.congrLeftₐ_apply_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) (g : LocallyConstant X Z) (a✝ : Y) :

((congrLeftₐ R e) g) a✝ = g (e.symm a✝)

source

@[simp]

theorem LocallyConstant.congrLeftₐ_symm_apply_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) (g : LocallyConstant Y Z) (a✝ : X) :

((congrLeftₐ R e).symm g) a✝ = g (e a✝)

source

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

LocallyConstant X Y →* LocallyConstant X Z

LocallyConstant.map as a MonoidHom.

Equations

Instances For

source

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

LocallyConstant X Y →+ LocallyConstant X Z

LocallyConstant.map as an AddMonoidHom.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.mapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [AddZeroClass Y] [AddZeroClass Z] (f : Y →+ Z) (g : LocallyConstant X Y) :

(mapAddMonoidHom f) g = map (⇑f) g

source

@[simp]

theorem LocallyConstant.mapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [MulOneClass Y] [MulOneClass Z] (f : Y →* Z) (g : LocallyConstant X Y) :

(mapMonoidHom f) g = map (⇑f) g

source

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

LocallyConstant X Y →ₗ[R] LocallyConstant X Z

LocallyConstant.map as a linear map.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.mapₗ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid Y] [Module R Y] [AddCommMonoid Z] [Module R Z] (f : Y →ₗ[R] Z) (g : LocallyConstant X Y) (a✝ : X) :

((mapₗ R f) g) a✝ = f (g a✝)

source

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

LocallyConstant X Y →+* LocallyConstant X Z

LocallyConstant.map as a RingHom.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.mapRingHom_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [Semiring Y] [Semiring Z] (f : Y →+* Z) (g : LocallyConstant X Y) (a✝ : X) :

((mapRingHom f) g) a✝ = f (g a✝)

source

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

LocallyConstant X Y →ₐ[R] LocallyConstant X Z

LocallyConstant.map as an AlgHom

Equations

Instances For

source

@[simp]

theorem LocallyConstant.mapₐ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [CommSemiring R] [Semiring Y] [Algebra R Y] [Semiring Z] [Algebra R Z] (f : Y →ₐ[R] Z) (g : LocallyConstant X Y) (a✝ : X) :

((mapₐ R f) g) a✝ = f (g a✝)

source

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

LocallyConstant X Y ≃ₗ[R] LocallyConstant X Z

LocallyConstant.congrRight as a linear equivalence.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.congrRightₗ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid Y] [Module R Y] [AddCommMonoid Z] [Module R Z] (e : Y ≃ₗ[R] Z) (a✝ : LocallyConstant X Z) (a✝¹ : X) :

((congrRightₗ R e).symm a✝) a✝¹ = e.symm (a✝ a✝¹)

source

@[simp]

theorem LocallyConstant.congrRightₗ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid Y] [Module R Y] [AddCommMonoid Z] [Module R Z] (e : Y ≃ₗ[R] Z) (g : LocallyConstant X Y) (a✝ : X) :

((congrRightₗ R e) g) a✝ = e (g a✝)

source

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

LocallyConstant X Y ≃+* LocallyConstant X Z

LocallyConstant.congrRight as a RingEquiv.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.congrRightRingEquiv_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [Semiring Y] [Semiring Z] (e : Y ≃+* Z) (g : LocallyConstant X Y) (a✝ : X) :

((congrRightRingEquiv e) g) a✝ = e (g a✝)

source

@[simp]

theorem LocallyConstant.congrRightRingEquiv_symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [Semiring Y] [Semiring Z] (e : Y ≃+* Z) (g : LocallyConstant X Z) (a✝ : X) :

((congrRightRingEquiv e).symm g) a✝ = (↑e).symm (g a✝)

source

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

LocallyConstant X Y ≃ₐ[R] LocallyConstant X Z

LocallyConstant.congrRight as an AlgEquiv.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.congrRightₐ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [CommSemiring R] [Semiring Y] [Algebra R Y] [Semiring Z] [Algebra R Z] (e : Y ≃ₐ[R] Z) (g : LocallyConstant X Y) (a✝ : X) :

((congrRightₐ R e) g) a✝ = e (g a✝)

source

@[simp]

theorem LocallyConstant.congrRightₐ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [CommSemiring R] [Semiring Y] [Algebra R Y] [Semiring Z] [Algebra R Z] (e : Y ≃ₐ[R] Z) (g : LocallyConstant X Z) (a✝ : X) :

((congrRightₐ R e).symm g) a✝ = e.symm (g a✝)

source

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

Y →ₗ[R] LocallyConstant X Y

LocallyConstant.const as a linear map.

Equations

Instances For

source

@[simp]

theorem LocallyConstant.constₗ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [Semiring R] [AddCommMonoid Y] [Module R Y] (y : Y) (a✝ : X) :

((constₗ R) y) a✝ = y

source

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

Y →ₐ[R] LocallyConstant X Y

LocallyConstant.const as an AlgHom

Equations

Instances For

source

@[simp]

theorem LocallyConstant.constₐ_apply_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [CommSemiring R] [Semiring Y] [Algebra R Y] (y : Y) (a✝ : X) :

((constₐ R) y) a✝ = y

Documentation

Mathlib.Topology.LocallyConstant.Algebra

Algebraic structure on locally constant functions #