# Algebraic structure on locally constant functions #

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

instance LocallyConstant.instZero {X : Type u_1} {Y : Type u_2} [] [Zero Y] :
Zero ()
Equations
• LocallyConstant.instZero = { zero := }
instance LocallyConstant.instOne {X : Type u_1} {Y : Type u_2} [] [One Y] :
One ()
Equations
• LocallyConstant.instOne = { one := }
@[simp]
theorem LocallyConstant.coe_zero {X : Type u_1} {Y : Type u_2} [] [Zero Y] :
0 = 0
@[simp]
theorem LocallyConstant.coe_one {X : Type u_1} {Y : Type u_2} [] [One Y] :
1 = 1
theorem LocallyConstant.zero_apply {X : Type u_1} {Y : Type u_2} [] [Zero Y] (x : X) :
0 x = 0
theorem LocallyConstant.one_apply {X : Type u_1} {Y : Type u_2} [] [One Y] (x : X) :
1 x = 1
theorem LocallyConstant.instNeg.proof_1 {X : Type u_2} {Y : Type u_1} [] [Neg Y] (f : ) :
instance LocallyConstant.instNeg {X : Type u_1} {Y : Type u_2} [] [Neg Y] :
Neg ()
Equations
• LocallyConstant.instNeg = { neg := fun (f : ) => { toFun := -f, isLocallyConstant := } }
instance LocallyConstant.instInv {X : Type u_1} {Y : Type u_2} [] [Inv Y] :
Inv ()
Equations
• LocallyConstant.instInv = { inv := fun (f : ) => { toFun := (f)⁻¹, isLocallyConstant := } }
@[simp]
theorem LocallyConstant.coe_neg {X : Type u_1} {Y : Type u_2} [] [Neg Y] (f : ) :
(-f) = -f
@[simp]
theorem LocallyConstant.coe_inv {X : Type u_1} {Y : Type u_2} [] [Inv Y] (f : ) :
f⁻¹ = (f)⁻¹
theorem LocallyConstant.neg_apply {X : Type u_1} {Y : Type u_2} [] [Neg Y] (f : ) (x : X) :
(-f) x = -f x
theorem LocallyConstant.inv_apply {X : Type u_1} {Y : Type u_2} [] [Inv Y] (f : ) (x : X) :
f⁻¹ x = (f x)⁻¹
instance LocallyConstant.instAdd {X : Type u_1} {Y : Type u_2} [] [Add Y] :
Equations
• LocallyConstant.instAdd = { add := fun (f g : ) => { toFun := f + g, isLocallyConstant := } }
theorem LocallyConstant.instAdd.proof_1 {X : Type u_2} {Y : Type u_1} [] [Add Y] (f : ) (g : ) :
IsLocallyConstant (f.toFun + g)
instance LocallyConstant.instMul {X : Type u_1} {Y : Type u_2} [] [Mul Y] :
Mul ()
Equations
• LocallyConstant.instMul = { mul := fun (f g : ) => { toFun := f * g, isLocallyConstant := } }
@[simp]
theorem LocallyConstant.coe_add {X : Type u_1} {Y : Type u_2} [] [Add Y] (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem LocallyConstant.coe_mul {X : Type u_1} {Y : Type u_2} [] [Mul Y] (f : ) (g : ) :
(f * g) = f * g
theorem LocallyConstant.add_apply {X : Type u_1} {Y : Type u_2} [] [Add Y] (f : ) (g : ) (x : X) :
(f + g) x = f x + g x
theorem LocallyConstant.mul_apply {X : Type u_1} {Y : Type u_2} [] [Mul Y] (f : ) (g : ) (x : X) :
(f * g) x = f x * g x
theorem LocallyConstant.instAddZeroClass.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
theorem LocallyConstant.instAddZeroClass.proof_1 {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
theorem LocallyConstant.instAddZeroClass.proof_3 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
instance LocallyConstant.instAddZeroClass {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instMulOneClass {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.coeFnAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), { toFun := DFunLike.coe, map_zero' := }.toFun (x + x_1) = { toFun := DFunLike.coe, map_zero' := }.toFun (x + x_1)
theorem LocallyConstant.coeFnAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
def LocallyConstant.coeFnAddMonoidHom {X : Type u_1} {Y : Type u_2} [] [] :
→+ XY

DFunLike.coe as an AddMonoidHom.

Equations
• LocallyConstant.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
@[simp]
theorem LocallyConstant.coeFnAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] :
∀ (a : ) (a_1 : X), LocallyConstant.coeFnAddMonoidHom a a_1 = a a_1
@[simp]
theorem LocallyConstant.coeFnMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] :
∀ (a : ) (a_1 : X), LocallyConstant.coeFnMonoidHom a a_1 = a a_1
def LocallyConstant.coeFnMonoidHom {X : Type u_1} {Y : Type u_2} [] [] :
→* XY

DFunLike.coe as a MonoidHom.

Equations
• LocallyConstant.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := , map_mul' := }
Instances For
theorem LocallyConstant.constAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_2} [] [] :
def LocallyConstant.constAddMonoidHom {X : Type u_1} {Y : Type u_2} [] [] :
Y →+

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

Equations
• LocallyConstant.constAddMonoidHom = { toFun := , map_zero' := , map_add' := }
Instances For
theorem LocallyConstant.constAddMonoidHom.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
∀ (x x_1 : Y), { toFun := , map_zero' := }.toFun (x + x_1) = { toFun := , map_zero' := }.toFun (x + x_1)
@[simp]
theorem LocallyConstant.constMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] (y : Y) :
LocallyConstant.constMonoidHom y =
@[simp]
theorem LocallyConstant.constAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] (y : Y) :
def LocallyConstant.constMonoidHom {X : Type u_1} {Y : Type u_2} [] [] :
Y →*

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

Equations
• LocallyConstant.constMonoidHom = { toFun := , map_one' := , map_mul' := }
Instances For
instance LocallyConstant.instMulZeroClass {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instMulZeroOneClass {X : Type u_1} {Y : Type u_2} [] [] :
Equations
noncomputable def LocallyConstant.charFn {X : Type u_1} (Y : Type u_2) [] [] {U : Set X} (hU : ) :

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
theorem LocallyConstant.coe_charFn {X : Type u_1} (Y : Type u_2) [] [] {U : Set X} (hU : ) :
() = U.indicator 1
theorem LocallyConstant.charFn_eq_one {X : Type u_1} (Y : Type u_2) [] [] {U : Set X} [] (x : X) (hU : ) :
() x = 1 x U
theorem LocallyConstant.charFn_eq_zero {X : Type u_1} (Y : Type u_2) [] [] {U : Set X} [] (x : X) (hU : ) :
() x = 0 xU
theorem LocallyConstant.charFn_inj {X : Type u_1} (Y : Type u_2) [] [] {U : Set X} {V : Set X} [] (hU : ) (hV : ) (h : ) :
U = V
theorem LocallyConstant.instSub.proof_1 {X : Type u_2} {Y : Type u_1} [] [Sub Y] (f : ) (g : ) :
IsLocallyConstant (f.toFun - g)
instance LocallyConstant.instSub {X : Type u_1} {Y : Type u_2} [] [Sub Y] :
Sub ()
Equations
• LocallyConstant.instSub = { sub := fun (f g : ) => { toFun := f - g, isLocallyConstant := } }
instance LocallyConstant.instDiv {X : Type u_1} {Y : Type u_2} [] [Div Y] :
Div ()
Equations
• LocallyConstant.instDiv = { div := fun (f g : ) => { toFun := f / g, isLocallyConstant := } }
theorem LocallyConstant.coe_sub {X : Type u_1} {Y : Type u_2} [] [Sub Y] (f : ) (g : ) :
(f - g) = f - g
theorem LocallyConstant.coe_div {X : Type u_1} {Y : Type u_2} [] [Div Y] (f : ) (g : ) :
(f / g) = f / g
theorem LocallyConstant.sub_apply {X : Type u_1} {Y : Type u_2} [] [Sub Y] (f : ) (g : ) (x : X) :
(f - g) x = f x - g x
theorem LocallyConstant.div_apply {X : Type u_1} {Y : Type u_2} [] [Div Y] (f : ) (g : ) (x : X) :
(f / g) x = f x / g x
instance LocallyConstant.instAddSemigroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddSemigroup.proof_2 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
theorem LocallyConstant.instAddSemigroup.proof_1 {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
instance LocallyConstant.instSemigroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instSemigroupWithZero {X : Type u_1} {Y : Type u_2} [] :
Equations
theorem LocallyConstant.instAddCommSemigroup.proof_2 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
instance LocallyConstant.instAddCommSemigroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instCommSemigroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.vadd {X : Type u_1} {Y : Type u_2} [] {α : Type u_3} [VAdd α Y] :
Equations
instance LocallyConstant.smul {X : Type u_1} {Y : Type u_2} [] {α : Type u_3} [SMul α Y] :
SMul α ()
Equations
@[simp]
theorem LocallyConstant.coe_vadd {X : Type u_1} {Y : Type u_2} [] {R : Type u_4} [VAdd R Y] (r : R) (f : ) :
(r +ᵥ f) = r +ᵥ f
@[simp]
theorem LocallyConstant.coe_smul {X : Type u_1} {Y : Type u_2} [] {R : Type u_4} [SMul R Y] (r : R) (f : ) :
(r f) = r f
theorem LocallyConstant.vadd_apply {X : Type u_1} {Y : Type u_2} [] {R : Type u_4} [VAdd R Y] (r : R) (f : ) (x : X) :
(r +ᵥ f) x = r +ᵥ f x
theorem LocallyConstant.smul_apply {X : Type u_1} {Y : Type u_2} [] {R : Type u_4} [SMul R Y] (r : R) (f : ) (x : X) :
(r f) x = r f x
instance LocallyConstant.instPow {X : Type u_1} {Y : Type u_2} [] {α : Type u_3} [Pow Y α] :
Pow () α
Equations
theorem LocallyConstant.instAddMonoid.proof_4 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddMonoid.proof_3 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
instance LocallyConstant.instAddMonoid {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddMonoid.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
theorem LocallyConstant.instAddMonoid.proof_1 {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
instance LocallyConstant.instMonoid {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instNatCast {X : Type u_1} {Y : Type u_2} [] [] :
Equations
• LocallyConstant.instNatCast = { natCast := fun (n : ) => }
instance LocallyConstant.instIntCast {X : Type u_1} {Y : Type u_2} [] [] :
Equations
• LocallyConstant.instIntCast = { intCast := fun (n : ) => }
instance LocallyConstant.instAddMonoidWithOne {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddCommMonoid.proof_4 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddCommMonoid.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
instance LocallyConstant.instAddCommMonoid {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddCommMonoid.proof_3 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
instance LocallyConstant.instCommMonoid {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instAddGroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddGroup.proof_6 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddGroup.proof_3 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
theorem LocallyConstant.instAddGroup.proof_7 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddGroup.proof_4 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ), (-x) = (-x)
theorem LocallyConstant.instAddGroup.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
theorem LocallyConstant.instAddGroup.proof_1 {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
theorem LocallyConstant.instAddGroup.proof_5 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x - x_1) = (x - x_1)
instance LocallyConstant.instGroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddCommGroup.proof_4 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ), (-x) = (-x)
theorem LocallyConstant.instAddCommGroup.proof_7 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddCommGroup.proof_5 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x - x_1) = (x - x_1)
instance LocallyConstant.instAddCommGroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
theorem LocallyConstant.instAddCommGroup.proof_3 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x x_1 : ), (x + x_1) = (x + x_1)
theorem LocallyConstant.instAddCommGroup.proof_6 {X : Type u_2} {Y : Type u_1} [] [] :
∀ (x : ) (x_1 : ), (x_1 x) = (x_1 x)
theorem LocallyConstant.instAddCommGroup.proof_2 {X : Type u_1} {Y : Type u_2} [] [] :
0 = 0
theorem LocallyConstant.instAddCommGroup.proof_1 {X : Type u_1} {Y : Type u_2} [] :
Function.Injective DFunLike.coe
instance LocallyConstant.instCommGroup {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instDistrib {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instNonUnitalNonAssocSemiring {X : Type u_1} {Y : Type u_2} [] :
Equations
instance LocallyConstant.instNonUnitalSemiring {X : Type u_1} {Y : Type u_2} [] :
Equations
instance LocallyConstant.instNonAssocSemiring {X : Type u_1} {Y : Type u_2} [] [] :
Equations
@[simp]
theorem LocallyConstant.constRingHom_apply {X : Type u_1} {Y : Type u_2} [] [] (y : Y) :
LocallyConstant.constRingHom y =
def LocallyConstant.constRingHom {X : Type u_1} {Y : Type u_2} [] [] :

The constant-function embedding, as a ring hom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance LocallyConstant.instSemiring {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instNonUnitalCommSemiring {X : Type u_1} {Y : Type u_2} [] :
Equations
instance LocallyConstant.instCommSemiring {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instNonUnitalNonAssocRing {X : Type u_1} {Y : Type u_2} [] :
Equations
instance LocallyConstant.instNonUnitalRing {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instNonAssocRing {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instRing {X : Type u_1} {Y : Type u_2} [] [Ring Y] :
Ring ()
Equations
instance LocallyConstant.instNonUnitalCommRing {X : Type u_1} {Y : Type u_2} [] :
Equations
instance LocallyConstant.instCommRing {X : Type u_1} {Y : Type u_2} [] [] :
Equations
instance LocallyConstant.instMulAction {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] [] :
Equations
instance LocallyConstant.instDistribMulAction {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] [] [] :
Equations
instance LocallyConstant.instModule {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] [] [Module R Y] :
Module R ()
Equations
instance LocallyConstant.instAlgebra {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] [] [Algebra R Y] :
Algebra R ()
Equations
• LocallyConstant.instAlgebra = Algebra.mk (LocallyConstant.constRingHom.comp ())
@[simp]
theorem LocallyConstant.coe_algebraMap {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] [] [Algebra R Y] (r : R) :
((algebraMap R ()) r) = (algebraMap R (XY)) r
@[simp]
theorem LocallyConstant.coeFnRingHom_apply {X : Type u_1} {Y : Type u_2} [] [] :
∀ (a : ) (a_1 : X), LocallyConstant.coeFnRingHom a a_1 = a a_1
def LocallyConstant.coeFnRingHom {X : Type u_1} {Y : Type u_2} [] [] :
→+* XY

DFunLike.coe as a RingHom.

Equations
• LocallyConstant.coeFnRingHom = let __spread.0 := LocallyConstant.coeFnAddMonoidHom; { toMonoidHom := LocallyConstant.coeFnMonoidHom, map_zero' := , map_add' := }
Instances For
@[simp]
theorem LocallyConstant.coeFnₗ_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] :
∀ (a : ) (a_1 : X), a a_1 = a a_1
def LocallyConstant.coeFnₗ {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] :
→ₗ[R] XY

DFunLike.coe as a linear map.

Equations
Instances For
@[simp]
theorem LocallyConstant.coeFnAlgHom_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] :
∀ (a : ) (a_1 : X), a a_1 = a a_1
def LocallyConstant.coeFnAlgHom {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] :
→ₐ[R] XY

DFunLike.coe as an AlgHom.

Equations
• = { toRingHom := LocallyConstant.coeFnRingHom, commutes' := }
Instances For
def LocallyConstant.evalAddMonoidHom {X : Type u_1} {Y : Type u_2} [] [] (x : X) :
→+ Y

Evaluation as an AddMonoidHom

Equations
Instances For
@[simp]
theorem LocallyConstant.evalAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] (x : X) :
∀ (a : ), = a x
@[simp]
theorem LocallyConstant.evalMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] (x : X) :
∀ (a : ), = a x
def LocallyConstant.evalMonoidHom {X : Type u_1} {Y : Type u_2} [] [] (x : X) :
→* Y

Evaluation as a MonoidHom

Equations
Instances For
@[simp]
theorem LocallyConstant.evalₗ_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] (x : X) :
∀ (a : ), () a = a x
def LocallyConstant.evalₗ {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] (x : X) :

Evaluation as a linear map

Equations
Instances For
@[simp]
theorem LocallyConstant.evalRingHom_apply {X : Type u_1} {Y : Type u_2} [] [] (x : X) :
∀ (a : ), = a x
def LocallyConstant.evalRingHom {X : Type u_1} {Y : Type u_2} [] [] (x : X) :

Evaluation as a RingHom

Equations
Instances For
@[simp]
theorem LocallyConstant.evalₐ_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] (x : X) :
∀ (a : ), () a = a x
def LocallyConstant.evalₐ {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] (x : X) :

Evaluation as an AlgHom

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

LocallyConstant.comap as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
theorem LocallyConstant.comapAddMonoidHom.proof_2 {X : Type u_3} {Y : Type u_2} [] [] {Z : Type u_1} [] (f : C(X, Y)) :
∀ (x x_1 : ), { toFun := , map_zero' := }.toFun (x + x_1) = { toFun := , map_zero' := }.toFun (x + x_1)
theorem LocallyConstant.comapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_3} [] [] {Z : Type u_2} [] (f : C(X, Y)) :
@[simp]
theorem LocallyConstant.comapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (f : C(X, Y)) (g : ) :
@[simp]
theorem LocallyConstant.comapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (f : C(X, Y)) (g : ) :
def LocallyConstant.comapMonoidHom {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (f : C(X, Y)) :

LocallyConstant.comap as a MonoidHom.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem LocallyConstant.comapₗ_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Z] (f : C(X, Y)) (g : ) :
∀ (a : X), (() g) a = g (f a)
def LocallyConstant.comapₗ {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Z] (f : C(X, Y)) :

LocallyConstant.comap as a linear map.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LocallyConstant.comapRingHom_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (f : C(X, Y)) (g : ) :
∀ (a : X), () a = g (f a)
def LocallyConstant.comapRingHom {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (f : C(X, Y)) :

LocallyConstant.comap as a RingHom.

Equations
• = let __spread.0 := ; { toMonoidHom := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem LocallyConstant.comapₐ_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Z] (f : C(X, Y)) (g : ) :
∀ (a : X), (() g) a = g (f a)
def LocallyConstant.comapₐ {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Z] (f : C(X, Y)) :

LocallyConstant.comap as an AlgHom

Equations
• = { toRingHom := , commutes' := }
Instances For
theorem LocallyConstant.ker_comapₗ {X : Type u_1} {Y : Type u_2} [] {R : Type u_5} [] {Z : Type u_6} [] [] [Module R Z] (f : C(X, Y)) (hfs : ) :
@[simp]
theorem LocallyConstant.congrLeftₗ_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Z] (e : X ≃ₜ Y) (g : ) :
∀ (a : Y), ( g) a = g (e.symm a)
@[simp]
theorem LocallyConstant.congrLeftₗ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Z] (e : X ≃ₜ Y) :
∀ (a : ) (a_1 : X), (.symm a) a_1 = a (e a_1)
def LocallyConstant.congrLeftₗ {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Z] (e : X ≃ₜ Y) :

LocallyConstant.congrLeft as a linear equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LocallyConstant.congrLeftRingEquiv_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (e : X ≃ₜ Y) (g : ) :
∀ (a : X), (.symm g) a = g (e a)
@[simp]
theorem LocallyConstant.congrLeftRingEquiv_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (e : X ≃ₜ Y) (g : ) :
∀ (a : Y), a = g (e.symm a)
def LocallyConstant.congrLeftRingEquiv {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} [] (e : X ≃ₜ Y) :

LocallyConstant.congrLeft as a RingEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LocallyConstant.congrLeftₐ_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Z] (e : X ≃ₜ Y) (g : ) :
∀ (a : Y), ( g) a = g (e.symm a)
@[simp]
theorem LocallyConstant.congrLeftₐ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Z] (e : X ≃ₜ Y) (g : ) :
∀ (a : X), (.symm g) a = g (e a)
def LocallyConstant.congrLeftₐ {X : Type u_1} {Y : Type u_2} [] [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Z] (e : X ≃ₜ Y) :

LocallyConstant.congrLeft as an AlgEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LocallyConstant.mapAddMonoidHom.proof_2 {X : Type u_2} {Y : Type u_1} [] {Z : Type u_3} [] [] (f : Y →+ Z) (x : ) (y : ) :
{ toFun := , map_zero' := }.toFun (x + y) = { toFun := , map_zero' := }.toFun x + { toFun := , map_zero' := }.toFun y
def LocallyConstant.mapAddMonoidHom {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →+ Z) :

LocallyConstant.map as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
theorem LocallyConstant.mapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_3} [] {Z : Type u_2} [] [] (f : Y →+ Z) :
@[simp]
theorem LocallyConstant.mapAddMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →+ Z) (g : ) :
@[simp]
theorem LocallyConstant.mapMonoidHom_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →* Z) (g : ) :
def LocallyConstant.mapMonoidHom {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →* Z) :

LocallyConstant.map as a MonoidHom.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem LocallyConstant.mapₗ_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Y] [] [Module R Z] (f : Y →ₗ[R] Z) (g : ) :
∀ (a : X), (() g) a = f (g a)
def LocallyConstant.mapₗ {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Y] [] [Module R Z] (f : Y →ₗ[R] Z) :

LocallyConstant.map as a linear map.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LocallyConstant.mapRingHom_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →+* Z) (g : ) :
∀ (a : X), () a = f (g a)
def LocallyConstant.mapRingHom {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (f : Y →+* Z) :

LocallyConstant.map as a RingHom.

Equations
Instances For
@[simp]
theorem LocallyConstant.mapₐ_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Y] [] [Algebra R Z] (f : Y →ₐ[R] Z) (g : ) :
∀ (a : X), (() g) a = f (g a)
def LocallyConstant.mapₐ {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Y] [] [Algebra R Z] (f : Y →ₐ[R] Z) :

LocallyConstant.map as an AlgHom

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem LocallyConstant.congrRightₗ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Y] [] [Module R Z] (e : Y ≃ₗ[R] Z) :
∀ (a : ) (a_1 : X), (.symm a) a_1 = e.symm (a a_1)
@[simp]
theorem LocallyConstant.congrRightₗ_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Y] [] [Module R Z] (e : Y ≃ₗ[R] Z) (g : ) :
∀ (a : X), ( g) a = e (g a)
def LocallyConstant.congrRightₗ {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Module R Y] [] [Module R Z] (e : Y ≃ₗ[R] Z) :

LocallyConstant.congrRight as a linear equivalence.

Equations
• = let __spread.0 := LocallyConstant.congrRight e.toEquiv; { toLinearMap := , invFun := __spread.0.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LocallyConstant.congrRightRingEquiv_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (e : Y ≃+* Z) (g : ) :
∀ (a : X), a = e (g a)
@[simp]
theorem LocallyConstant.congrRightRingEquiv_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (e : Y ≃+* Z) (g : ) :
∀ (a : X), (.symm g) a = (e).symm (g a)
def LocallyConstant.congrRightRingEquiv {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} [] [] (e : Y ≃+* Z) :

LocallyConstant.congrRight as a RingEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LocallyConstant.congrRightₐ_symm_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Y] [] [Algebra R Z] (e : Y ≃ₐ[R] Z) (g : ) :
∀ (a : X), (.symm g) a = e.symm (g a)
@[simp]
theorem LocallyConstant.congrRightₐ_apply_apply {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Y] [] [Algebra R Z] (e : Y ≃ₐ[R] Z) (g : ) :
∀ (a : X), ( g) a = e (g a)
def LocallyConstant.congrRightₐ {X : Type u_1} {Y : Type u_2} [] {Z : Type u_6} (R : Type u_7) [] [] [Algebra R Y] [] [Algebra R Z] (e : Y ≃ₐ[R] Z) :

LocallyConstant.congrRight as an AlgEquiv.

Equations
• = let __spread.0 := ; { toEquiv := , map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem LocallyConstant.constₗ_apply_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] (y : Y) :
∀ (a : X), () a = y
def LocallyConstant.constₗ {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Module R Y] :

LocallyConstant.const as a linear map.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LocallyConstant.constₐ_apply_apply {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] (y : Y) :
∀ (a : X), () a = y
def LocallyConstant.constₐ {X : Type u_1} {Y : Type u_2} [] (R : Type u_6) [] [] [Algebra R Y] :

LocallyConstant.const as an AlgHom

Equations
• = { toRingHom := LocallyConstant.constRingHom, commutes' := }
Instances For