mathlib3 documentation

topology.instances.triv_sq_zero_ext

Topology on `triv_sq_zero_ext R M` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The type triv_sq_zero_ext 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 triv_sq_zero_ext.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 #

triv_sq_zero_ext.topological_ring: the ring operations are continuous

@[protected, instance]

def triv_sq_zero_ext.topological_space {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] :

topological_space (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.topological_space = topological_space.induced triv_sq_zero_ext.fst _inst_1 ⊓ topological_space.induced triv_sq_zero_ext.snd _inst_2

@[protected, instance]

def triv_sq_zero_ext.t2_space {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [t2_space R] [t2_space M] :

t2_space (triv_sq_zero_ext R M)

theorem triv_sq_zero_ext.nhds_def {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] (x : triv_sq_zero_ext R M) :

nhds x = (nhds x.fst).prod (nhds x.snd)

theorem triv_sq_zero_ext.nhds_inl {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero M] (x : R) :

nhds (triv_sq_zero_ext.inl x) = (nhds x).prod (nhds 0)

theorem triv_sq_zero_ext.nhds_inr {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero R] (m : M) :

nhds (triv_sq_zero_ext.inr m) = (nhds 0).prod (nhds m)

theorem triv_sq_zero_ext.continuous_fst {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] :

continuous triv_sq_zero_ext.fst

theorem triv_sq_zero_ext.continuous_snd {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] :

continuous triv_sq_zero_ext.snd

theorem triv_sq_zero_ext.continuous_inl {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero M] :

continuous triv_sq_zero_ext.inl

theorem triv_sq_zero_ext.continuous_inr {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero R] :

continuous triv_sq_zero_ext.inr

theorem triv_sq_zero_ext.embedding_inl {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero M] :

embedding triv_sq_zero_ext.inl

theorem triv_sq_zero_ext.embedding_inr {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_zero R] :

embedding triv_sq_zero_ext.inr

@[simp]

theorem triv_sq_zero_ext.fst_clm_coe_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :

⇑↑(triv_sq_zero_ext.fst_clm R M) x = x.fst

def triv_sq_zero_ext.fst_clm (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] :

triv_sq_zero_ext R M →L[R] R

triv_sq_zero_ext.fst as a continuous linear map.

Equations

triv_sq_zero_ext.fst_clm R M = {to_linear_map := {to_fun := triv_sq_zero_ext.fst M, map_add' := _, map_smul' := _}, cont := _}

@[simp]

theorem triv_sq_zero_ext.fst_clm_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :

⇑(triv_sq_zero_ext.fst_clm R M) x = x.fst

@[simp]

theorem triv_sq_zero_ext.snd_clm_coe_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :

⇑↑(triv_sq_zero_ext.snd_clm R M) x = x.snd

@[simp]

theorem triv_sq_zero_ext.snd_clm_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :

⇑(triv_sq_zero_ext.snd_clm R M) x = x.snd

def triv_sq_zero_ext.snd_clm (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] :

triv_sq_zero_ext R M →L[R] M

triv_sq_zero_ext.snd as a continuous linear map.

Equations

triv_sq_zero_ext.snd_clm R M = {to_linear_map := {to_fun := triv_sq_zero_ext.snd M, map_add' := _, map_smul' := _}, cont := _}

@[simp]

theorem triv_sq_zero_ext.inl_clm_coe_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) :

⇑↑(triv_sq_zero_ext.inl_clm R M) r = triv_sq_zero_ext.inl r

def triv_sq_zero_ext.inl_clm (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] :

R →L[R] triv_sq_zero_ext R M

triv_sq_zero_ext.inl as a continuous linear map.

Equations

triv_sq_zero_ext.inl_clm R M = {to_linear_map := {to_fun := triv_sq_zero_ext.inl (add_zero_class.to_has_zero M), map_add' := _, map_smul' := _}, cont := _}

@[simp]

theorem triv_sq_zero_ext.inl_clm_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) :

⇑(triv_sq_zero_ext.inl_clm R M) r = triv_sq_zero_ext.inl r

def triv_sq_zero_ext.inr_clm (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] :

M →L[R] triv_sq_zero_ext R M

triv_sq_zero_ext.inr as a continuous linear map.

Equations

triv_sq_zero_ext.inr_clm R M = {to_linear_map := {to_fun := triv_sq_zero_ext.inr (mul_zero_class.to_has_zero R), map_add' := _, map_smul' := _}, cont := _}

@[simp]

theorem triv_sq_zero_ext.inr_clm_coe_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (m : M) :

⇑↑(triv_sq_zero_ext.inr_clm R M) m = triv_sq_zero_ext.inr m

@[simp]

theorem triv_sq_zero_ext.inr_clm_apply (R : Type u_3) (M : Type u_4) [topological_space R] [topological_space M] [comm_semiring R] [add_comm_monoid M] [module R M] (m : M) :

⇑(triv_sq_zero_ext.inr_clm R M) m = triv_sq_zero_ext.inr m

@[protected, instance]

def triv_sq_zero_ext.has_continuous_add {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_add R] [has_add M] [has_continuous_add R] [has_continuous_add M] :

has_continuous_add (triv_sq_zero_ext R M)

@[protected, instance]

def triv_sq_zero_ext.has_continuous_mul {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_mul R] [has_add M] [has_smul R M] [has_smul Rᵐᵒᵖ M] [has_continuous_mul R] [has_continuous_smul R M] [has_continuous_smul Rᵐᵒᵖ M] [has_continuous_add M] :

has_continuous_mul (triv_sq_zero_ext R M)

@[protected, instance]

def triv_sq_zero_ext.has_continuous_neg {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_neg R] [has_neg M] [has_continuous_neg R] [has_continuous_neg M] :

has_continuous_neg (triv_sq_zero_ext R M)

theorem triv_sq_zero_ext.topological_semiring {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] [topological_semiring R] [has_continuous_add M] [has_continuous_smul R M] [has_continuous_smul Rᵐᵒᵖ M] :

topological_semiring (triv_sq_zero_ext R M)

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

@[protected, instance]

def triv_sq_zero_ext.topological_ring {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [ring R] [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [has_continuous_smul Rᵐᵒᵖ M] :

topological_ring (triv_sq_zero_ext R M)

@[protected, instance]

def triv_sq_zero_ext.has_continuous_const_smul {S : Type u_2} {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [has_smul S R] [has_smul S M] [has_continuous_const_smul S R] [has_continuous_const_smul S M] :

has_continuous_const_smul S (triv_sq_zero_ext R M)

@[protected, instance]

def triv_sq_zero_ext.has_continuous_smul {S : Type u_2} {R : Type u_3} {M : Type u_4} [topological_space R] [topological_space M] [topological_space S] [has_smul S R] [has_smul S M] [has_continuous_smul S R] [has_continuous_smul S M] :

has_continuous_smul S (triv_sq_zero_ext R M)

theorem triv_sq_zero_ext.has_sum_inl {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α → R} {a : R} (h : has_sum f a) :

has_sum (λ (x : α), triv_sq_zero_ext.inl (f x)) (triv_sq_zero_ext.inl a)

theorem triv_sq_zero_ext.has_sum_inr {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α → M} {a : M} (h : has_sum f a) :

has_sum (λ (x : α), triv_sq_zero_ext.inr (f x)) (triv_sq_zero_ext.inr a)

theorem triv_sq_zero_ext.has_sum_fst {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α → triv_sq_zero_ext R M} {a : triv_sq_zero_ext R M} (h : has_sum f a) :

has_sum (λ (x : α), (f x).fst) a.fst

theorem triv_sq_zero_ext.has_sum_snd {α : Type u_1} {R : Type u_3} (M : Type u_4) [topological_space R] [topological_space M] [add_comm_monoid R] [add_comm_monoid M] {f : α → triv_sq_zero_ext R M} {a : triv_sq_zero_ext R M} (h : has_sum f a) :

has_sum (λ (x : α), (f x).snd) a.snd