Documentation

Mathlib.Topology.LocallyConstant.Algebra

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} [TopologicalSpace X] [Zero Y] :
Equations
instance LocallyConstant.instOne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [One Y] :
Equations
@[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
instance LocallyConstant.instNeg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Neg Y] :
Equations
  • LocallyConstant.instNeg = { neg := fun (f : LocallyConstant X Y) => { toFun := -f, isLocallyConstant := } }
instance LocallyConstant.instInv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Inv Y] :
Equations
  • LocallyConstant.instInv = { 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)⁻¹
instance LocallyConstant.instAdd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Add Y] :
Equations
  • LocallyConstant.instAdd = { add := fun (f g : LocallyConstant X Y) => { toFun := f + g, isLocallyConstant := } }
theorem LocallyConstant.instAdd.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.instMul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Mul Y] :
Equations
  • LocallyConstant.instMul = { 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.instAddZeroClass.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)
Equations
Equations
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)

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} [TopologicalSpace X] [AddZeroClass Y] :
    ∀ (a : LocallyConstant X Y) (a_1 : X), LocallyConstant.coeFnAddMonoidHom a a_1 = a a_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

    DFunLike.coe as a MonoidHom.

    Equations
    • LocallyConstant.coeFnMonoidHom = { toFun := DFunLike.coe, map_one' := , map_mul' := }
    Instances For

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

      Equations
      Instances For
        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)
        @[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

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

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

          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) [TopologicalSpace X] [MulZeroOneClass Y] {U : Set X} (hU : IsClopen U) :
            (LocallyConstant.charFn Y hU) = U.indicator 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) :
            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 xU
            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.instSub.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.instSub {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Sub Y] :
            Equations
            • LocallyConstant.instSub = { sub := fun (f g : LocallyConstant X Y) => { toFun := f - g, isLocallyConstant := } }
            instance LocallyConstant.instDiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Div Y] :
            Equations
            • LocallyConstant.instDiv = { 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
            Equations
            theorem LocallyConstant.instAddSemigroup.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)
            Equations
            Equations
            theorem LocallyConstant.instAddCommSemigroup.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)
            Equations
            Equations
            instance LocallyConstant.vadd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [VAdd α Y] :
            Equations
            instance LocallyConstant.smul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [SMul α Y] :
            Equations
            @[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.instPow {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [Pow Y α] :
            Equations
            theorem LocallyConstant.instAddMonoid.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.instAddMonoid.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)
            Equations
            theorem LocallyConstant.instAddMonoid.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddMonoid Y] :
            0 = 0
            Equations
            Equations
            Equations
            Equations
            theorem LocallyConstant.instAddCommMonoid.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)
            Equations
            theorem LocallyConstant.instAddCommMonoid.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)
            Equations
            Equations
            theorem LocallyConstant.instAddGroup.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.instAddGroup.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.instAddGroup.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.instAddGroup.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddGroup Y] :
            ∀ (x : LocallyConstant X Y), (-x) = (-x)
            theorem LocallyConstant.instAddGroup.proof_2 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [AddGroup Y] :
            0 = 0
            theorem LocallyConstant.instAddGroup.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)
            instance LocallyConstant.instGroup {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Group Y] :
            Equations
            theorem LocallyConstant.instAddCommGroup.proof_4 {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [AddCommGroup Y] :
            ∀ (x : LocallyConstant X Y), (-x) = (-x)
            theorem LocallyConstant.instAddCommGroup.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.instAddCommGroup.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)
            Equations
            theorem LocallyConstant.instAddCommGroup.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)
            theorem LocallyConstant.instAddCommGroup.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)
            Equations
            Equations
            Equations
            Equations
            Equations
            @[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

            The constant-function embedding, as a ring hom.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              Equations
              Equations
              Equations
              Equations
              Equations
              instance LocallyConstant.instRing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [Ring Y] :
              Equations
              Equations
              Equations
              instance LocallyConstant.instMulAction {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_5} [Monoid R] [MulAction R Y] :
              Equations
              Equations
              instance LocallyConstant.instModule {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_5} [Semiring R] [AddCommMonoid Y] [Module R Y] :
              Equations
              instance LocallyConstant.instAlgebra {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {R : Type u_5} [CommSemiring R] [Semiring Y] [Algebra R Y] :
              Equations
              @[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 (XY)) 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

              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} [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] :

                DFunLike.coe as a linear map.

                Equations
                Instances For
                  @[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] :

                  DFunLike.coe as an AlgHom.

                  Equations
                  Instances For

                    Evaluation as an AddMonoidHom

                    Equations
                    Instances For
                      @[simp]
                      theorem LocallyConstant.evalMonoidHom_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MulOneClass Y] (x : X) :

                      Evaluation as a MonoidHom

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

                        Evaluation as a linear map

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

                          Evaluation as a RingHom

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

                            Evaluation as an AlgHom

                            Equations
                            Instances For

                              LocallyConstant.comap as an AddMonoidHom.

                              Equations
                              Instances For
                                theorem LocallyConstant.comapAddMonoidHom.proof_2 {X : Type u_3} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_1} [AddZeroClass Z] (f : C(X, Y)) :
                                ∀ (x x_1 : LocallyConstant Y Z), { toFun := LocallyConstant.comap f, map_zero' := }.toFun (x + x_1) = { toFun := LocallyConstant.comap f, map_zero' := }.toFun (x + x_1)

                                LocallyConstant.comap as a MonoidHom.

                                Equations
                                Instances For
                                  @[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), ((LocallyConstant.comapₗ R f) g) a = g (f a)
                                  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.comap as a linear map.

                                  Equations
                                  Instances For
                                    @[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), ((LocallyConstant.comapRingHom f) g) a = g (f a)

                                    LocallyConstant.comap as a RingHom.

                                    Equations
                                    Instances For
                                      @[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), ((LocallyConstant.comapₐ R f) g) a = g (f a)
                                      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.comap as an AlgHom

                                      Equations
                                      Instances For
                                        @[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), ((LocallyConstant.congrLeftₗ R e) g) a = g (e.symm a)
                                        @[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_1 : X), ((LocallyConstant.congrLeftₗ R e).symm a) a_1 = a (e a_1)
                                        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.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} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (e : X ≃ₜ Y) (g : LocallyConstant Y Z) :
                                          ∀ (a : X), ((LocallyConstant.congrLeftRingEquiv e).symm g) a = g (e a)
                                          @[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), ((LocallyConstant.congrLeftRingEquiv e) g) a = g (e.symm a)

                                          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} [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), ((LocallyConstant.congrLeftₐ R e) g) a = g (e.symm a)
                                            @[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), ((LocallyConstant.congrLeftₐ R e).symm g) a = g (e a)
                                            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.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} [TopologicalSpace X] {Z : Type u_3} [AddZeroClass Y] [AddZeroClass Z] (f : Y →+ Z) (x : LocallyConstant X Y) (y : LocallyConstant X Y) :
                                              { toFun := LocallyConstant.map f, map_zero' := }.toFun (x + y) = { toFun := LocallyConstant.map f, map_zero' := }.toFun x + { toFun := LocallyConstant.map f, map_zero' := }.toFun y

                                              LocallyConstant.map as an AddMonoidHom.

                                              Equations
                                              Instances For
                                                theorem LocallyConstant.mapAddMonoidHom.proof_1 {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] {Z : Type u_2} [AddZeroClass Y] [AddZeroClass Z] (f : Y →+ Z) :
                                                @[simp]

                                                LocallyConstant.map as a MonoidHom.

                                                Equations
                                                Instances For
                                                  @[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), ((LocallyConstant.mapₗ R f) g) a = f (g a)
                                                  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.map as a linear map.

                                                  Equations
                                                  Instances For
                                                    @[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), ((LocallyConstant.mapRingHom f) g) a = f (g a)
                                                    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.map as a RingHom.

                                                    Equations
                                                    Instances For
                                                      @[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), ((LocallyConstant.mapₐ R f) g) a = f (g a)
                                                      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.map as an AlgHom

                                                      Equations
                                                      Instances For
                                                        @[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_1 : X), ((LocallyConstant.congrRightₗ R e).symm a) a_1 = e.symm (a a_1)
                                                        @[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), ((LocallyConstant.congrRightₗ R e) g) a = e (g a)
                                                        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.congrRight as a linear equivalence.

                                                        Equations
                                                        Instances For
                                                          @[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), ((LocallyConstant.congrRightRingEquiv e) g) a = e (g a)
                                                          @[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), ((LocallyConstant.congrRightRingEquiv e).symm g) a = (e).symm (g a)

                                                          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} [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), ((LocallyConstant.congrRightₐ R e).symm g) a = e.symm (g a)
                                                            @[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), ((LocallyConstant.congrRightₐ R e) g) a = e (g a)
                                                            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.congrRight as an AlgEquiv.

                                                            Equations
                                                            Instances For
                                                              @[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), ((LocallyConstant.constₗ R) y) a = y
                                                              def LocallyConstant.constₗ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [Semiring R] [AddCommMonoid Y] [Module R Y] :

                                                              LocallyConstant.const as a linear map.

                                                              Equations
                                                              Instances For
                                                                @[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), ((LocallyConstant.constₐ R) y) a = y
                                                                def LocallyConstant.constₐ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (R : Type u_6) [CommSemiring R] [Semiring Y] [Algebra R Y] :

                                                                LocallyConstant.const as an AlgHom

                                                                Equations
                                                                Instances For