Documentation

Orbifolds.Diffeology.Algebra.DSmoothMap

Algebraic structures on `DSmoothMap` #

In this file put algebraic structure instance on the type DSmoothMap X A of smooth maps from a diffeological space X to a diffeological algebraic structure A. For example, DSmoothMap X G is a group under pointwise multiplication whenever G is a diffeological group.

Adapted from Mathlib.Topology.ContinuousMap.Algebra.

`mul` and `add` #

instance DSmoothMap.instMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Mul A] [DSmoothMul A] :

Mul (DSmoothMap X A)

Equations

DSmoothMap.instMul = { mul := fun (f g : DSmoothMap X A) => { toFun := ⇑f * ⇑g, dsmooth := ⋯ } }

instance DSmoothMap.instAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Add A] [DSmoothAdd A] :

Add (DSmoothMap X A)

Equations

DSmoothMap.instAdd = { add := fun (f g : DSmoothMap X A) => { toFun := ⇑f + ⇑g, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_mul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Mul A] [DSmoothMul A] (f g : DSmoothMap X A) :

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

@[simp]

theorem DSmoothMap.coe_add {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Add A] [DSmoothAdd A] (f g : DSmoothMap X A) :

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

@[simp]

theorem DSmoothMap.mul_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Mul A] [DSmoothMul A] (f g : DSmoothMap X A) (x : X) :

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

@[simp]

theorem DSmoothMap.add_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Add A] [DSmoothAdd A] (f g : DSmoothMap X A) (x : X) :

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

@[simp]

theorem DSmoothMap.mul_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Mul A] [DSmoothMul A] (f₁ f₂ : DSmoothMap Y A) (g : DSmoothMap X Y) :

(f₁ * f₂).comp g = f₁.comp g * f₂.comp g

@[simp]

theorem DSmoothMap.add_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Add A] [DSmoothAdd A] (f₁ f₂ : DSmoothMap Y A) (g : DSmoothMap X Y) :

(f₁ + f₂).comp g = f₁.comp g + f₂.comp g

`one` and `zero` #

instance DSmoothMap.instOne {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [One A] :

One (DSmoothMap X A)

Equations

DSmoothMap.instOne = { one := DSmoothMap.const X 1 }

instance DSmoothMap.instZero {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Zero A] :

Zero (DSmoothMap X A)

Equations

DSmoothMap.instZero = { zero := DSmoothMap.const X 0 }

@[simp]

theorem DSmoothMap.coe_one {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [One A] :

⇑1 = 1

@[simp]

theorem DSmoothMap.coe_zero {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Zero A] :

⇑0 = 0

@[simp]

theorem DSmoothMap.one_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [One A] (x : X) :

1 x = 1

@[simp]

theorem DSmoothMap.zero_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Zero A] (x : X) :

0 x = 0

@[simp]

theorem DSmoothMap.one_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [One A] (g : DSmoothMap X Y) :

comp 1 g = 1

@[simp]

theorem DSmoothMap.zero_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Zero A] (g : DSmoothMap X Y) :

comp 0 g = 0

`Nat.cast` #

instance DSmoothMap.instNatCast {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NatCast A] :

NatCast (DSmoothMap X A)

Equations

DSmoothMap.instNatCast = { natCast := fun (n : ℕ) => DSmoothMap.const X ↑n }

@[simp]

theorem DSmoothMap.coe_natCast {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NatCast A] (n : ℕ) :

⇑↑n = ↑n

@[simp]

theorem DSmoothMap.natCast_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NatCast A] (n : ℕ) (x : X) :

↑n x = ↑n

instance DSmoothMap.instIntCast {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [IntCast A] :

IntCast (DSmoothMap X A)

Equations

DSmoothMap.instIntCast = { intCast := fun (n : ℤ) => DSmoothMap.const X ↑n }

`Int.cast` #

@[simp]

theorem DSmoothMap.coe_intCast {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [IntCast A] (n : ℤ) :

⇑↑n = ↑n

@[simp]

theorem DSmoothMap.intCast_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [IntCast A] (n : ℤ) (x : X) :

↑n x = ↑n

`nsmul` and `pow` #

instance DSmoothMap.instNSMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] :

SMul ℕ (DSmoothMap X A)

Equations

DSmoothMap.instNSMul = { smul := fun (n : ℕ) (f : DSmoothMap X A) => { toFun := n • ⇑f, dsmooth := ⋯ } }

instance DSmoothMap.instPow {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] :

Pow (DSmoothMap X A) ℕ

Equations

DSmoothMap.instPow = { pow := fun (f : DSmoothMap X A) (n : ℕ) => { toFun := ⇑f ^ n, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_pow {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] (f : DSmoothMap X A) (n : ℕ) :

⇑(f ^ n) = ⇑f ^ n

theorem DSmoothMap.coe_nsmul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] (n : ℕ) (f : DSmoothMap X A) :

⇑(n • f) = n • ⇑f

@[simp]

theorem DSmoothMap.pow_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] (f : DSmoothMap X A) (n : ℕ) (x : X) :

(f ^ n) x = f x ^ n

theorem DSmoothMap.nsmul_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] (f : DSmoothMap X A) (n : ℕ) (x : X) :

(n • f) x = n • f x

@[simp]

theorem DSmoothMap.pow_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] (f : DSmoothMap Y A) (n : ℕ) (g : DSmoothMap X Y) :

(f ^ n).comp g = f.comp g ^ n

theorem DSmoothMap.nsmul_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] (f : DSmoothMap Y A) (n : ℕ) (g : DSmoothMap X Y) :

(n • f).comp g = n • f.comp g

`inv` and `neg` #

instance DSmoothMap.instInvOfDSmoothInv {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Inv A] [DSmoothInv A] :

Inv (DSmoothMap X A)

Equations

DSmoothMap.instInvOfDSmoothInv = { inv := fun (f : DSmoothMap X A) => { toFun := (⇑f)⁻¹, dsmooth := ⋯ } }

instance DSmoothMap.instNegOfDSmoothNeg {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Neg A] [DSmoothNeg A] :

Neg (DSmoothMap X A)

Equations

DSmoothMap.instNegOfDSmoothNeg = { neg := fun (f : DSmoothMap X A) => { toFun := -⇑f, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_inv {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Inv A] [DSmoothInv A] (f : DSmoothMap X A) :

⇑f⁻¹ = (⇑f)⁻¹

@[simp]

theorem DSmoothMap.coe_neg {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Neg A] [DSmoothNeg A] (f : DSmoothMap X A) :

⇑(-f) = -⇑f

@[simp]

theorem DSmoothMap.inv_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Inv A] [DSmoothInv A] (f : DSmoothMap X A) (x : X) :

f⁻¹ x = (f x)⁻¹

@[simp]

theorem DSmoothMap.neg_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Neg A] [DSmoothNeg A] (f : DSmoothMap X A) (x : X) :

(-f) x = -f x

@[simp]

theorem DSmoothMap.inv_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Inv A] [DSmoothInv A] (f : DSmoothMap Y A) (g : DSmoothMap X Y) :

f⁻¹.comp g = (f.comp g)⁻¹

@[simp]

theorem DSmoothMap.neg_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Neg A] [DSmoothNeg A] (f : DSmoothMap Y A) (g : DSmoothMap X Y) :

(-f).comp g = -f.comp g

`div` and `sub` #

instance DSmoothMap.instDivOfDSmoothDiv {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Div A] [DSmoothDiv A] :

Div (DSmoothMap X A)

Equations

DSmoothMap.instDivOfDSmoothDiv = { div := fun (f g : DSmoothMap X A) => { toFun := ⇑f / ⇑g, dsmooth := ⋯ } }

instance DSmoothMap.instSubOfDSmoothSub {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Sub A] [DSmoothSub A] :

Sub (DSmoothMap X A)

Equations

DSmoothMap.instSubOfDSmoothSub = { sub := fun (f g : DSmoothMap X A) => { toFun := ⇑f - ⇑g, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_div {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Div A] [DSmoothDiv A] (f g : DSmoothMap X A) :

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

@[simp]

theorem DSmoothMap.coe_sub {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Sub A] [DSmoothSub A] (f g : DSmoothMap X A) :

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

@[simp]

theorem DSmoothMap.div_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Div A] [DSmoothDiv A] (f g : DSmoothMap X A) (x : X) :

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

@[simp]

theorem DSmoothMap.sub_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Sub A] [DSmoothSub A] (f g : DSmoothMap X A) (x : X) :

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

@[simp]

theorem DSmoothMap.div_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Div A] [DSmoothDiv A] (f g : DSmoothMap Y A) (h : DSmoothMap X Y) :

(f / g).comp h = f.comp h / g.comp h

@[simp]

theorem DSmoothMap.sub_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Sub A] [DSmoothSub A] (f g : DSmoothMap Y A) (h : DSmoothMap X Y) :

(f - g).comp h = f.comp h - g.comp h

`zpow` and `zsmul` #

instance DSmoothMap.instZSMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] :

SMul ℤ (DSmoothMap X A)

Equations

DSmoothMap.instZSMul = { smul := fun (z : ℤ) (f : DSmoothMap X A) => { toFun := z • ⇑f, dsmooth := ⋯ } }

instance DSmoothMap.instZPow {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] :

Pow (DSmoothMap X A) ℤ

Equations

DSmoothMap.instZPow = { pow := fun (f : DSmoothMap X A) (z : ℤ) => { toFun := ⇑f ^ z, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_zpow {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] (f : DSmoothMap X A) (z : ℤ) :

⇑(f ^ z) = ⇑f ^ z

theorem DSmoothMap.coe_zsmul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] (z : ℤ) (f : DSmoothMap X A) :

⇑(z • f) = z • ⇑f

@[simp]

theorem DSmoothMap.zpow_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] (f : DSmoothMap X A) (z : ℤ) (x : X) :

(f ^ z) x = f x ^ z

theorem DSmoothMap.zsmul_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] (f : DSmoothMap X A) (z : ℤ) (x : X) :

(z • f) x = z • f x

@[simp]

theorem DSmoothMap.zpow_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] (f : DSmoothMap Y A) (z : ℤ) (g : DSmoothMap X Y) :

(f ^ z).comp g = f.comp g ^ z

theorem DSmoothMap.zsmul_comp {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] (f : DSmoothMap Y A) (z : ℤ) (g : DSmoothMap X Y) :

(z • f).comp g = z • f.comp g

Structure instances #

instance DSmoothMap.instSemigroupOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Semigroup A] [DSmoothMul A] :

Semigroup (DSmoothMap X A)

Equations

DSmoothMap.instSemigroupOfDSmoothMul = Function.Injective.semigroup DFunLike.coe ⋯ ⋯

instance DSmoothMap.instAddSemigroupOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddSemigroup A] [DSmoothAdd A] :

AddSemigroup (DSmoothMap X A)

Equations

DSmoothMap.instAddSemigroupOfDSmoothAdd = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯

instance DSmoothMap.instCommSemigroupOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommSemigroup A] [DSmoothMul A] :

CommSemigroup (DSmoothMap X A)

Equations

DSmoothMap.instCommSemigroupOfDSmoothMul = Function.Injective.commSemigroup DFunLike.coe ⋯ ⋯

instance DSmoothMap.instAddCommSemigroupOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddCommSemigroup A] [DSmoothAdd A] :

AddCommSemigroup (DSmoothMap X A)

Equations

DSmoothMap.instAddCommSemigroupOfDSmoothAdd = Function.Injective.addCommSemigroup DFunLike.coe ⋯ ⋯

instance DSmoothMap.instMulOneClassOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [MulOneClass A] [DSmoothMul A] :

MulOneClass (DSmoothMap X A)

Equations

DSmoothMap.instMulOneClassOfDSmoothMul = Function.Injective.mulOneClass DFunLike.coe ⋯ ⋯ ⋯

instance DSmoothMap.instAddZeroClassOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddZeroClass A] [DSmoothAdd A] :

AddZeroClass (DSmoothMap X A)

Equations

DSmoothMap.instAddZeroClassOfDSmoothAdd = Function.Injective.addZeroClass DFunLike.coe ⋯ ⋯ ⋯

instance DSmoothMap.instMulZeroClassOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [MulZeroClass A] [DSmoothMul A] :

MulZeroClass (DSmoothMap X A)

Equations

DSmoothMap.instMulZeroClassOfDSmoothMul = Function.Injective.mulZeroClass DFunLike.coe ⋯ ⋯ ⋯

instance DSmoothMap.instSemigroupWithZeroOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [SemigroupWithZero A] [DSmoothMul A] :

SemigroupWithZero (DSmoothMap X A)

Equations

DSmoothMap.instSemigroupWithZeroOfDSmoothMul = Function.Injective.semigroupWithZero DFunLike.coe ⋯ ⋯ ⋯

instance DSmoothMap.instMonoidOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] :

Monoid (DSmoothMap X A)

Equations

DSmoothMap.instMonoidOfDSmoothMul = Function.Injective.monoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instAddMonoidOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] :

AddMonoid (DSmoothMap X A)

Equations

DSmoothMap.instAddMonoidOfDSmoothAdd = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instMonoidWithZeroOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [MonoidWithZero A] [DSmoothMul A] :

MonoidWithZero (DSmoothMap X A)

Equations

DSmoothMap.instMonoidWithZeroOfDSmoothMul = Function.Injective.monoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instCommMonoidOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommMonoid A] [DSmoothMul A] :

CommMonoid (DSmoothMap X A)

Equations

DSmoothMap.instCommMonoidOfDSmoothMul = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instAddCommMonoidOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddCommMonoid A] [DSmoothAdd A] :

AddCommMonoid (DSmoothMap X A)

Equations

DSmoothMap.instAddCommMonoidOfDSmoothAdd = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instCommMonoidWithZeroOfDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommMonoidWithZero A] [DSmoothMul A] :

CommMonoidWithZero (DSmoothMap X A)

Equations

DSmoothMap.instCommMonoidWithZeroOfDSmoothMul = Function.Injective.commMonoidWithZero DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instGroupOfDiffeologicalGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] :

Group (DSmoothMap X A)

Equations

DSmoothMap.instGroupOfDiffeologicalGroup = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instAddGroupOfDiffeologicalAddGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] :

AddGroup (DSmoothMap X A)

Equations

DSmoothMap.instAddGroupOfDiffeologicalAddGroup = Function.Injective.addGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instCommGroupOfDiffeologicalGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommGroup A] [DiffeologicalGroup A] :

CommGroup (DSmoothMap X A)

Equations

DSmoothMap.instCommGroupOfDiffeologicalGroup = Function.Injective.commGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instAddCommGroupOfDiffeologicalAddGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddCommGroup A] [DiffeologicalAddGroup A] :

AddCommGroup (DSmoothMap X A)

Equations

DSmoothMap.instAddCommGroupOfDiffeologicalAddGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instAddMonoidWithOneOfDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoidWithOne A] [DSmoothAdd A] :

AddMonoidWithOne (DSmoothMap X A)

Equations

DSmoothMap.instAddMonoidWithOneOfDSmoothAdd = Function.Injective.addMonoidWithOne DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instNonUnitalNonAssocRingOfDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NonUnitalNonAssocRing A] [DiffeologicalRing A] :

NonUnitalNonAssocRing (DSmoothMap X A)

Equations

DSmoothMap.instNonUnitalNonAssocRingOfDiffeologicalRing = Function.Injective.nonUnitalNonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instNonUnitalRingOfDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NonUnitalRing A] [DiffeologicalRing A] :

NonUnitalRing (DSmoothMap X A)

Equations

DSmoothMap.instNonUnitalRingOfDiffeologicalRing = Function.Injective.nonUnitalRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instNonAssocRingOfDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NonAssocRing A] [DiffeologicalRing A] :

NonAssocRing (DSmoothMap X A)

Equations

DSmoothMap.instNonAssocRingOfDiffeologicalRing = Function.Injective.nonAssocRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Ring A] [DiffeologicalRing A] :

Ring (DSmoothMap X A)

Equations

DSmoothMap.instRing = Function.Injective.ring DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instNonUnitalCommRingOfDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NonUnitalCommRing A] [DiffeologicalRing A] :

NonUnitalCommRing (DSmoothMap X A)

Equations

DSmoothMap.instNonUnitalCommRingOfDiffeologicalRing = Function.Injective.nonUnitalCommRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DSmoothMap.instCommRingOfDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommRing A] [DiffeologicalRing A] :

CommRing (DSmoothMap X A)

Equations

DSmoothMap.instCommRingOfDiffeologicalRing = Function.Injective.commRing DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def DSmoothMap.coeFnMonoidHom {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] :

DSmoothMap X A →* X → A

Coercion to a function as a MonoidHom. Similar to MonoidHom.coeFn.

Equations

DSmoothMap.coeFnMonoidHom = { toFun := fun (f : DSmoothMap X A) => ⇑f, map_one' := ⋯, map_mul' := ⋯ }

Instances For

def DSmoothMap.coeFnAddMonoidHom {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] :

DSmoothMap X A →+ X → A

Coercion to a function as an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Equations

DSmoothMap.coeFnAddMonoidHom = { toFun := fun (f : DSmoothMap X A) => ⇑f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.coeFnMonoidHom_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Monoid A] [DSmoothMul A] (f : DSmoothMap X A) (a : X) :

coeFnMonoidHom f a = f a

@[simp]

theorem DSmoothMap.coeFnAddMonoidHom_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddMonoid A] [DSmoothAdd A] (f : DSmoothMap X A) (a : X) :

coeFnAddMonoidHom f a = f a

def DSmoothMap.coeFnRingHom {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Ring A] [DiffeologicalRing A] :

DSmoothMap X A →+* X → A

Coercion to a function as a RingHom.

Equations

DSmoothMap.coeFnRingHom = { toMonoidHom := DSmoothMap.coeFnMonoidHom, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.coeFnRingHom_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Ring A] [DiffeologicalRing A] (f : DSmoothMap X A) (a : X) :

coeFnRingHom f a = f a

def DSmoothMap.compRightRingHom {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] [NonAssocRing A] [DiffeologicalRing A] (f : DSmoothMap X Y) :

DSmoothMap Y A →+* DSmoothMap X A

Precomposition DSmoothMap Y A → DSmoothMap X A with f : DSmoothMap X Y as a ring homomorphism. TODO: add versions of this for monoids, groups etc. as needed.

Equations

f.compRightRingHom = { toFun := fun (g : DSmoothMap Y A) => g.comp f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.coe_prod {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommMonoid A] [DSmoothMul A] {ι : Type u_4} (s : Finset ι) (f : ι → DSmoothMap X A) :

⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)

@[simp]

theorem DSmoothMap.coe_sum {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddCommMonoid A] [DSmoothAdd A] {ι : Type u_4} (s : Finset ι) (f : ι → DSmoothMap X A) :

⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

theorem DSmoothMap.prod_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [CommMonoid A] [DSmoothMul A] {ι : Type u_4} (s : Finset ι) (f : ι → DSmoothMap X A) (x : X) :

(∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x

theorem DSmoothMap.sum_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddCommMonoid A] [DSmoothAdd A] {ι : Type u_4} (s : Finset ι) (f : ι → DSmoothMap X A) (x : X) :

(∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x

Diffeological structure instances #

instance DSmoothMap.instDSmoothMul {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Mul A] [DSmoothMul A] :

DSmoothMul (DSmoothMap X A)

instance DSmoothMap.instDSmoothAdd {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Add A] [DSmoothAdd A] :

DSmoothAdd (DSmoothMap X A)

instance DSmoothMap.instDSmoothInv {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Inv A] [DSmoothInv A] :

DSmoothInv (DSmoothMap X A)

instance DSmoothMap.instDSmoothNeg {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Neg A] [DSmoothNeg A] :

DSmoothNeg (DSmoothMap X A)

instance DSmoothMap.instDiffeologicalGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [Group A] [DiffeologicalGroup A] :

DiffeologicalGroup (DSmoothMap X A)

instance DSmoothMap.instDiffeologicalAddGroup {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [AddGroup A] [DiffeologicalAddGroup A] :

DiffeologicalAddGroup (DSmoothMap X A)

instance DSmoothMap.instDiffeologicalRing {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] [NonUnitalNonAssocRing A] [DiffeologicalRing A] :

DiffeologicalRing (DSmoothMap X A)

Modules and algebras #

instance DSmoothMap.instSMul {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] :

SMul R (DSmoothMap X M)

TODO: weaken this to DSmoothConstSMul once that is defined, with no diffeology required on R.

Equations

DSmoothMap.instSMul = { smul := fun (r : R) (f : DSmoothMap X M) => { toFun := r • ⇑f, dsmooth := ⋯ } }

instance DSmoothMap.instVAdd {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] :

VAdd R (DSmoothMap X M)

Equations

DSmoothMap.instVAdd = { vadd := fun (r : R) (f : DSmoothMap X M) => { toFun := r +ᵥ ⇑f, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_smul {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] (c : R) (f : DSmoothMap X M) :

⇑(c • f) = c • ⇑f

@[simp]

theorem DSmoothMap.coe_vadd {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] (c : R) (f : DSmoothMap X M) :

⇑(c +ᵥ f) = c +ᵥ ⇑f

theorem DSmoothMap.smul_apply {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] (c : R) (f : DSmoothMap X M) (x : X) :

(c • f) x = c • f x

theorem DSmoothMap.vadd_apply {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] (c : R) (f : DSmoothMap X M) (x : X) :

(c +ᵥ f) x = c +ᵥ f x

@[simp]

theorem DSmoothMap.smul_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] (r : R) (f : DSmoothMap Y M) (g : DSmoothMap X Y) :

(r • f).comp g = r • f.comp g

@[simp]

theorem DSmoothMap.vadd_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] (r : R) (f : DSmoothMap Y M) (g : DSmoothMap X Y) :

(r +ᵥ f).comp g = r +ᵥ f.comp g

instance DSmoothMap.instDSmoothSMul {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] :

DSmoothSMul R (DSmoothMap X M)

instance DSmoothMap.instDSmoothVAdd {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] :

DSmoothVAdd R (DSmoothMap X M)

instance DSmoothMap.instSMulCommClass {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {R' : Type u_5} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace R'] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] [SMul R' M] [DSmoothSMul R' M] [SMulCommClass R R' M] :

SMulCommClass R R' (DSmoothMap X M)

instance DSmoothMap.instVAddCommClass {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {R' : Type u_5} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace R'] [DiffeologicalSpace M] [VAdd R M] [DSmoothVAdd R M] [VAdd R' M] [DSmoothVAdd R' M] [VAddCommClass R R' M] :

VAddCommClass R R' (DSmoothMap X M)

instance DSmoothMap.instIsScalarTower {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {R' : Type u_5} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace R'] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] [SMul R' M] [DSmoothSMul R' M] [SMul R R'] [IsScalarTower R R' M] :

IsScalarTower R R' (DSmoothMap X M)

instance DSmoothMap.instIsCentralScalar {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [SMul Rᵐᵒᵖ M] [DSmoothSMul R M] [IsCentralScalar R M] :

IsCentralScalar R (DSmoothMap X M)

instance DSmoothMap.instIsScalarTower_1 {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] [Mul M] [DSmoothMul M] [IsScalarTower R M M] :

IsScalarTower R (DSmoothMap X M) (DSmoothMap X M)

instance DSmoothMap.instSMulCommClass_1 {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] [Mul M] [DSmoothMul M] [SMulCommClass R M M] :

SMulCommClass R (DSmoothMap X M) (DSmoothMap X M)

instance DSmoothMap.instSMulCommClass_2 {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [SMul R M] [DSmoothSMul R M] [Mul M] [DSmoothMul M] [SMulCommClass M R M] :

SMulCommClass (DSmoothMap X M) R (DSmoothMap X M)

instance DSmoothMap.instMulActionOfDSmoothSMul {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Monoid R] [MulAction R M] [DSmoothSMul R M] :

MulAction R (DSmoothMap X M)

Equations

DSmoothMap.instMulActionOfDSmoothSMul = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

instance DSmoothMap.instDistribMulActionOfDSmoothSMul {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Monoid R] [AddMonoid M] [DistribMulAction R M] [DSmoothAdd M] [DSmoothSMul R M] :

DistribMulAction R (DSmoothMap X M)

Equations

DSmoothMap.instDistribMulActionOfDSmoothSMul = Function.Injective.distribMulAction DSmoothMap.coeFnAddMonoidHom ⋯ ⋯

instance DSmoothMap.module {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothAdd M] [DSmoothSMul R M] :

Module R (DSmoothMap X M)

Equations

DSmoothMap.module = Function.Injective.module R DSmoothMap.coeFnAddMonoidHom ⋯ ⋯

def DSmoothMap.coeFnLinearMap {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothAdd M] [DSmoothSMul R M] :

DSmoothMap X M →ₗ[R] X → M

Coercion to a function as a LinearMap.

Equations

DSmoothMap.coeFnLinearMap = { toFun := (↑DSmoothMap.coeFnAddMonoidHom).toFun, map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.coeFnLinearMap_apply {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothAdd M] [DSmoothSMul R M] (a✝ : DSmoothMap X M) (a✝¹ : X) :

coeFnLinearMap a✝ a✝¹ = (↑coeFnAddMonoidHom).toFun a✝ a✝¹

def DSmoothMap.C {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] {R : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [DiffeologicalRing A] :

R →+* DSmoothMap X A

Smooth constant functions as a RingHom.

Equations

DSmoothMap.C = { toFun := fun (c : R) => { toFun := fun (x : X) => (algebraMap R A) c, dsmooth := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.C_apply {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] {R : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [DiffeologicalRing A] (r : R) (x : X) :

(C r) x = (algebraMap R A) r

instance DSmoothMap.algebra {X : Type u_1} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace A] {R : Type u_4} [DiffeologicalSpace R] [CommSemiring R] [Ring A] [Algebra R A] [DiffeologicalRing A] [DSmoothSMul R A] :

Algebra R (DSmoothMap X A)

Equations

DSmoothMap.algebra = { toSMul := DSmoothMap.instSMul, algebraMap := DSmoothMap.C, commutes' := ⋯, smul_def' := ⋯ }

def DSmoothMap.compRightAlgHom {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] {R : Type u_4} [DiffeologicalSpace R] [CommRing R] [Ring A] [Algebra R A] [DiffeologicalRing A] [DSmoothSMul R A] (f : DSmoothMap X Y) :

DSmoothMap Y A →ₐ[R] DSmoothMap X A

Precomposition DSmoothMap Y A → DSmoothMap X A with f : DSmoothMap X Y as an algebra homomorphism.

Equations

f.compRightAlgHom = { toRingHom := f.compRightRingHom, commutes' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.compRightAlgHom_apply_apply {X : Type u_1} {Y : Type u_2} {A : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace A] {R : Type u_4} [DiffeologicalSpace R] [CommRing R] [Ring A] [Algebra R A] [DiffeologicalRing A] [DSmoothSMul R A] (f : DSmoothMap X Y) (g : DSmoothMap Y A) (a✝ : X) :

(f.compRightAlgHom g) a✝ = g (f a✝)

instance DSmoothMap.instSMul' {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothSMul R M] :

SMul (DSmoothMap X R) (DSmoothMap X M)

Equations

DSmoothMap.instSMul' = { smul := fun (f : DSmoothMap X R) (g : DSmoothMap X M) => { toFun := fun (x : X) => f x • g x, dsmooth := ⋯ } }

@[simp]

theorem DSmoothMap.coe_smul' {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothSMul R M] (f : DSmoothMap X R) (g : DSmoothMap X M) :

⇑(f • g) = ⇑f • ⇑g

theorem DSmoothMap.smul_apply' {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DSmoothSMul R M] (f : DSmoothMap X R) (g : DSmoothMap X M) (x : X) :

(f • g) x = f x • g x

instance DSmoothMap.module' {X : Type u_1} [DiffeologicalSpace X] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DiffeologicalRing R] [DSmoothAdd M] [DSmoothSMul R M] :

Module (DSmoothMap X R) (DSmoothMap X M)

Equations

DSmoothMap.module' = { smul := fun (x1 : DSmoothMap X R) (x2 : DSmoothMap X M) => x1 • x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

def DSmoothMap.compRightLinearMap' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DiffeologicalRing R] [DSmoothAdd M] [DSmoothSMul R M] (f : DSmoothMap X Y) :

DSmoothMap Y M →ₛₗ[f.compRightRingHom] DSmoothMap X M

Precomposition DSmoothMap Y M → DSmoothMap X M with f : DSmoothMap X Y as a semilinear map over f.compRightRingHom : DSmoothMap Y R →+* DSmoothMap X R.

Equations

f.compRightLinearMap' = { toFun := fun (g : DSmoothMap Y M) => g.comp f, map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem DSmoothMap.compRightLinearMap'_apply_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {R : Type u_4} {M : Type u_6} [DiffeologicalSpace R] [DiffeologicalSpace M] [Ring R] [AddCommMonoid M] [Module R M] [DiffeologicalRing R] [DSmoothAdd M] [DSmoothSMul R M] (f : DSmoothMap X Y) (g : DSmoothMap Y M) (a✝ : X) :

(f.compRightLinearMap' g) a✝ = g (f a✝)