Topology on TrivSqZeroExt R M #
The type TrivSqZeroExt R M inherits the topology from R × M.
Note that this is not the topology induced by the seminorm on the dual numbers suggested by
this Math.SE answer, which instead induces
the topology pulled back through the projection map TrivSqZeroExt.fst : tsze R M → R.
Obviously, that topology is not Hausdorff and using it would result in exp converging to more than
one value.
Main results #
TrivSqZeroExt.topologicalRing: the ring operations are continuous
instance
TrivSqZeroExt.instTopologicalSpace
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
:
Equations
- TrivSqZeroExt.instTopologicalSpace = TopologicalSpace.induced TrivSqZeroExt.fst inst✝¹ ⊓ TopologicalSpace.induced TrivSqZeroExt.snd inst✝
instance
TrivSqZeroExt.instT2Space
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[T2Space R]
[T2Space M]
:
T2Space (TrivSqZeroExt R M)
theorem
TrivSqZeroExt.nhds_def
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
(x : TrivSqZeroExt R M)
:
theorem
TrivSqZeroExt.nhds_inl
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero M]
(x : R)
:
theorem
TrivSqZeroExt.nhds_inr
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero R]
(m : M)
:
theorem
TrivSqZeroExt.continuous_fst
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
:
Continuous TrivSqZeroExt.fst
theorem
TrivSqZeroExt.continuous_snd
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
:
Continuous TrivSqZeroExt.snd
theorem
TrivSqZeroExt.continuous_inl
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero M]
:
Continuous TrivSqZeroExt.inl
theorem
TrivSqZeroExt.continuous_inr
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero R]
:
Continuous TrivSqZeroExt.inr
theorem
TrivSqZeroExt.IsEmbedding.inl
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero M]
:
Topology.IsEmbedding TrivSqZeroExt.inl
@[deprecated TrivSqZeroExt.IsEmbedding.inl]
theorem
TrivSqZeroExt.embedding_inl
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero M]
:
Topology.IsEmbedding TrivSqZeroExt.inl
Alias of TrivSqZeroExt.IsEmbedding.inl.
theorem
TrivSqZeroExt.IsEmbedding.inr
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero R]
:
Topology.IsEmbedding TrivSqZeroExt.inr
@[deprecated TrivSqZeroExt.IsEmbedding.inr]
theorem
TrivSqZeroExt.embedding_inr
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Zero R]
:
Topology.IsEmbedding TrivSqZeroExt.inr
Alias of TrivSqZeroExt.IsEmbedding.inr.
def
TrivSqZeroExt.fstCLM
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
TrivSqZeroExt R M →L[R] R
TrivSqZeroExt.fst as a continuous linear map.
Equations
- TrivSqZeroExt.fstCLM R M = { toFun := TrivSqZeroExt.fst, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
TrivSqZeroExt.fstCLM_apply
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(x : TrivSqZeroExt R M)
:
(TrivSqZeroExt.fstCLM R M) x = x.fst
def
TrivSqZeroExt.sndCLM
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
TrivSqZeroExt R M →L[R] M
TrivSqZeroExt.snd as a continuous linear map.
Equations
- TrivSqZeroExt.sndCLM R M = { toFun := TrivSqZeroExt.snd, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
TrivSqZeroExt.sndCLM_apply
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(x : TrivSqZeroExt R M)
:
(TrivSqZeroExt.sndCLM R M) x = x.snd
def
TrivSqZeroExt.inlCLM
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
R →L[R] TrivSqZeroExt R M
TrivSqZeroExt.inl as a continuous linear map.
Equations
- TrivSqZeroExt.inlCLM R M = { toFun := TrivSqZeroExt.inl, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
TrivSqZeroExt.inlCLM_apply
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(r : R)
:
(TrivSqZeroExt.inlCLM R M) r = TrivSqZeroExt.inl r
def
TrivSqZeroExt.inrCLM
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
M →L[R] TrivSqZeroExt R M
TrivSqZeroExt.inr as a continuous linear map.
Equations
- TrivSqZeroExt.inrCLM R M = { toFun := TrivSqZeroExt.inr, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
@[simp]
theorem
TrivSqZeroExt.inrCLM_apply
(R : Type u_3)
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(m : M)
:
(TrivSqZeroExt.inrCLM R M) m = TrivSqZeroExt.inr m
instance
TrivSqZeroExt.instContinuousAdd
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Add R]
[Add M]
[ContinuousAdd R]
[ContinuousAdd M]
:
ContinuousAdd (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Mul R]
[Add M]
[SMul R M]
[SMul Rᵐᵒᵖ M]
[ContinuousMul R]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[ContinuousAdd M]
:
ContinuousMul (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instContinuousNeg
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Neg R]
[Neg M]
[ContinuousNeg R]
[ContinuousNeg M]
:
ContinuousNeg (TrivSqZeroExt R M)
theorem
TrivSqZeroExt.topologicalSemiring
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module Rᵐᵒᵖ M]
[TopologicalSemiring R]
[ContinuousAdd M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
:
This is not an instance due to complaints by the fails_quickly linter. At any rate, we only
really care about the TopologicalRing instance below.
instance
TrivSqZeroExt.instTopologicalRingOfTopologicalAddGroupOfContinuousSMulMulOpposite
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[Ring R]
[AddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[TopologicalRing R]
[TopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
:
TopologicalRing (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instContinuousConstSMul
{S : Type u_2}
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[SMul S R]
[SMul S M]
[ContinuousConstSMul S R]
[ContinuousConstSMul S M]
:
ContinuousConstSMul S (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instContinuousSMul
{S : Type u_2}
{R : Type u_3}
{M : Type u_4}
[TopologicalSpace R]
[TopologicalSpace M]
[TopologicalSpace S]
[SMul S R]
[SMul S M]
[ContinuousSMul S R]
[ContinuousSMul S M]
:
ContinuousSMul S (TrivSqZeroExt R M)
theorem
TrivSqZeroExt.hasSum_inl
{α : Type u_1}
{R : Type u_3}
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid R]
[AddCommMonoid M]
{f : α → R}
{a : R}
(h : HasSum f a)
:
HasSum (fun (x : α) => TrivSqZeroExt.inl (f x)) (TrivSqZeroExt.inl a)
theorem
TrivSqZeroExt.hasSum_inr
{α : Type u_1}
{R : Type u_3}
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid R]
[AddCommMonoid M]
{f : α → M}
{a : M}
(h : HasSum f a)
:
HasSum (fun (x : α) => TrivSqZeroExt.inr (f x)) (TrivSqZeroExt.inr a)
theorem
TrivSqZeroExt.hasSum_fst
{α : Type u_1}
{R : Type u_3}
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid R]
[AddCommMonoid M]
{f : α → TrivSqZeroExt R M}
{a : TrivSqZeroExt R M}
(h : HasSum f a)
:
HasSum (fun (x : α) => (f x).fst) a.fst
theorem
TrivSqZeroExt.hasSum_snd
{α : Type u_1}
{R : Type u_3}
(M : Type u_4)
[TopologicalSpace R]
[TopologicalSpace M]
[AddCommMonoid R]
[AddCommMonoid M]
{f : α → TrivSqZeroExt R M}
{a : TrivSqZeroExt R M}
(h : HasSum f a)
:
HasSum (fun (x : α) => (f x).snd) a.snd
instance
TrivSqZeroExt.instUniformSpace
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
:
UniformSpace (TrivSqZeroExt R M)
Equations
- TrivSqZeroExt.instUniformSpace = UniformSpace.mk UniformSpace.uniformity ⋯ ⋯ ⋯
instance
TrivSqZeroExt.instCompleteSpace
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
[CompleteSpace R]
[CompleteSpace M]
:
CompleteSpace (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instUniformAddGroup
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
[AddGroup R]
[AddGroup M]
[UniformAddGroup R]
[UniformAddGroup M]
:
UniformAddGroup (TrivSqZeroExt R M)
theorem
TrivSqZeroExt.uniformity_def
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
:
uniformity (TrivSqZeroExt R M) = Filter.comap (fun (p : TrivSqZeroExt R M × TrivSqZeroExt R M) => (p.1.fst, p.2.fst)) (uniformity R) ⊓ Filter.comap (fun (p : TrivSqZeroExt R M × TrivSqZeroExt R M) => (p.1.snd, p.2.snd)) (uniformity M)
theorem
TrivSqZeroExt.uniformContinuous_fst
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
:
UniformContinuous TrivSqZeroExt.fst
theorem
TrivSqZeroExt.uniformContinuous_snd
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
:
UniformContinuous TrivSqZeroExt.snd
theorem
TrivSqZeroExt.uniformContinuous_inl
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
[Zero M]
:
UniformContinuous TrivSqZeroExt.inl
theorem
TrivSqZeroExt.uniformContinuous_inr
{R : Type u_3}
{M : Type u_4}
[UniformSpace R]
[UniformSpace M]
[Zero R]
:
UniformContinuous TrivSqZeroExt.inr