Documentation

Mathlib.Topology.Instances.TrivSqZeroExt

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

TopologicalSpace (TrivSqZeroExt R 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) :

nhds x = nhds x.fst ×ˢ nhds x.snd

theorem TrivSqZeroExt.nhds_inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] (x : R) :

nhds (inl x) = nhds x ×ˢ nhds 0

theorem TrivSqZeroExt.nhds_inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] (m : M) :

nhds (inr m) = nhds 0 ×ˢ nhds m

theorem TrivSqZeroExt.continuous_fst {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] :

theorem TrivSqZeroExt.continuous_snd {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] :

theorem TrivSqZeroExt.continuous_inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] :

theorem TrivSqZeroExt.continuous_inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] :

theorem TrivSqZeroExt.IsEmbedding.inl {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero M] :

Topology.IsEmbedding TrivSqZeroExt.inl

theorem TrivSqZeroExt.IsEmbedding.inr {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Zero R] :

Topology.IsEmbedding TrivSqZeroExt.inr

def TrivSqZeroExt.fstCLM (R : Type u_3) (M : Type u_4) [TopologicalSpace R] [TopologicalSpace M] [CommSemiring R] [AddCommMonoid M] [Module R M] :

StrongDual R (TrivSqZeroExt R M)

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

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

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

(inlCLM R M) r = 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) :

(inrCLM R M) m = 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] [IsTopologicalSemiring R] [ContinuousAdd M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :

IsTopologicalSemiring (TrivSqZeroExt R M)

This is not an instance due to complaints by the fails_quickly linter. At any rate, we only really care about the IsTopologicalRing instance below.

instance TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite {R : Type u_3} {M : Type u_4} [TopologicalSpace R] [TopologicalSpace M] [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsTopologicalRing R] [IsTopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] :

IsTopologicalRing (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 : α) => inl (f x)) (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 : α) => inr (f x)) (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 = { toTopologicalSpace := TrivSqZeroExt.instTopologicalSpace, uniformity := UniformSpace.uniformity, symm := ⋯, comp := ⋯, nhds_eq_comap_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.instIsUniformAddGroup {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [AddGroup R] [AddGroup M] [IsUniformAddGroup R] [IsUniformAddGroup M] :

IsUniformAddGroup (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 fst

theorem TrivSqZeroExt.uniformContinuous_snd {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] :

UniformContinuous snd

theorem TrivSqZeroExt.uniformContinuous_inl {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [Zero M] :

UniformContinuous inl

theorem TrivSqZeroExt.uniformContinuous_inr {R : Type u_3} {M : Type u_4} [UniformSpace R] [UniformSpace M] [Zero R] :

UniformContinuous inr