Theory of topological modules and continuous linear maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We use the class has_continuous_smul for topological (semi) modules and topological vector spaces.
In this file we define continuous (semi-)linear maps, as semilinear maps between topological
modules which are continuous. The set of continuous semilinear maps between the topological
R₁-module M and R₂-module M₂ with respect to the ring_hom σ is denoted by M →SL[σ] M₂.
Plain linear maps are denoted by M →L[R] M₂ and star-linear maps by M →L⋆[R] M₂.
The corresponding notation for equivalences is M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.
theorem
has_continuous_smul.of_nhds_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[module R M]
[topological_ring R]
[topological_add_group M]
(hmul : filter.tendsto (λ (p : R × M), p.fst • p.snd) ((nhds 0).prod (nhds 0)) (nhds 0))
(hmulleft : ∀ (m : M), filter.tendsto (λ (a : R), a • m) (nhds 0) (nhds 0))
(hmulright : ∀ (a : R), filter.tendsto (λ (m : M), a • m) (nhds 0) (nhds 0)) :
theorem
submodule.eq_top_of_nonempty_interior'
{R : Type u_1}
{M : Type u_2}
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M]
[(nhds_within 0 {x : R | is_unit x}).ne_bot]
(s : submodule R M)
(hs : (interior ↑s).nonempty) :
If M is a topological module over R and 0 is a limit of invertible elements of R, then
⊤ is the only submodule of M with a nonempty interior.
This is the case, e.g., if R is a nontrivially normed field.
theorem
module.punctured_nhds_ne_bot
(R : Type u_1)
(M : Type u_2)
[ring R]
[topological_space R]
[topological_space M]
[add_comm_group M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M]
[nontrivial M]
[(nhds_within 0 {0}ᶜ).ne_bot]
[no_zero_smul_divisors R M]
(x : M) :
(nhds_within x {x}ᶜ).ne_bot
Let R be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see normed_field.punctured_nhds_ne_bot). Let M be a nontrivial module over R
such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this
using ne_bot (𝓝[≠] x).
This lemma is not an instance because Lean would need to find [has_continuous_smul ?m_1 M] with
unknown ?m_1. We register this as an instance for R = ℝ in real.punctured_nhds_module_ne_bot.
One can also use haveI := module.punctured_nhds_ne_bot R M in a proof.
theorem
has_continuous_smul_induced
{R : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
[u : topological_space R]
{t : topological_space M₂}
[has_continuous_smul R M₂]
(f : M₁ →ₗ[R] M₂) :
has_continuous_smul R M₁
@[protected, instance]
def
submodule.has_continuous_smul
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[topological_space α]
[semiring α]
[add_comm_monoid β]
[module α β]
[has_continuous_smul α β]
(S : submodule α β) :
@[protected, instance]
def
submodule.topological_add_group
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[ring α]
[add_comm_group β]
[module α β]
[topological_add_group β]
(S : submodule α β) :
theorem
submodule.closure_smul_self_subset
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
(s : submodule R M) :
theorem
submodule.closure_smul_self_eq
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
(s : submodule R M) :
def
submodule.topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
submodule R M
The (topological-space) closure of a submodule of a topological R-module M is itself
a submodule.
Equations
Instances for ↥submodule.topological_closure
@[simp]
theorem
submodule.topological_closure_coe
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
↑(s.topological_closure) = closure ↑s
theorem
submodule.le_topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
s ≤ s.topological_closure
theorem
submodule.is_closed_topological_closure
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M) :
theorem
submodule.topological_closure_minimal
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M)
{t : submodule R M}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
theorem
submodule.topological_closure_mono
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
{s t : submodule R M}
(h : s ≤ t) :
theorem
is_closed.submodule_topological_closure_eq
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
{s : submodule R M}
(hs : is_closed ↑s) :
s.topological_closure = s
The topological closure of a closed submodule s is equal to s.
theorem
submodule.dense_iff_topological_closure_eq_top
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
{s : submodule R M} :
A subspace is dense iff its topological closure is the entire space.
@[protected, instance]
def
submodule.topological_closure.complete_space
{R : Type u}
[semiring R]
[topological_space R]
{M' : Type u_1}
[add_comm_monoid M']
[module R M']
[uniform_space M']
[has_continuous_add M']
[has_continuous_smul R M']
[complete_space M']
(U : submodule R M') :
theorem
submodule.is_closed_or_dense_of_is_coatom
{R : Type u}
{M : Type v}
[semiring R]
[topological_space R]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M]
[has_continuous_add M]
(s : submodule R M)
(hs : is_coatom s) :
A maximal proper subspace of a topological module (i.e a submodule satisfying is_coatom)
is either closed or dense.
theorem
linear_map.continuous_on_pi
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[finite ι]
[semiring R]
[topological_space R]
[add_comm_monoid M]
[module R M]
[topological_space M]
[has_continuous_add M]
[has_continuous_smul R M]
(f : (ι → R) →ₗ[R] M) :
structure
continuous_linear_map
{R : Type u_1}
{S : Type u_2}
[semiring R]
[semiring S]
(σ : R →+* S)
(M : Type u_3)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_4)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_3 u_4)
- to_linear_map : M →ₛₗ[σ] M₂
- cont : continuous self.to_linear_map.to_fun . "continuity'"
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M and M₂ will be topological modules over the topological
ring R.
Instances for continuous_linear_map
- continuous_linear_map.has_sizeof_inst
- continuous_linear_map.linear_map.has_coe
- continuous_linear_map.continuous_semilinear_map_class
- continuous_linear_map.to_fun
- continuous_linear_map.mul_action
- continuous_linear_map.is_scalar_tower
- continuous_linear_map.smul_comm_class
- continuous_linear_map.has_zero
- continuous_linear_map.inhabited
- continuous_linear_map.unique_of_left
- continuous_linear_map.unique_of_right
- continuous_linear_map.has_one
- continuous_linear_map.has_add
- continuous_linear_map.add_comm_monoid
- continuous_linear_map.has_mul
- continuous_linear_map.monoid_with_zero
- continuous_linear_map.semiring
- continuous_linear_map.apply_module
- continuous_linear_map.apply_has_faithful_smul
- continuous_linear_map.apply_smul_comm_class
- continuous_linear_map.apply_smul_comm_class'
- continuous_linear_map.has_continuous_const_smul
- continuous_linear_map.has_neg
- continuous_linear_map.has_sub
- continuous_linear_map.add_comm_group
- continuous_linear_map.ring
- continuous_linear_map.distrib_mul_action
- continuous_linear_map.module
- continuous_linear_map.is_central_scalar
- continuous_linear_map.algebra
- continuous_linear_equiv.continuous_linear_map.has_coe
- linear_isometry_equiv.continuous_linear_map.has_coe_t
- continuous_linear_map.topological_space
- continuous_linear_map.topological_add_group
- continuous_linear_map.has_continuous_smul
- continuous_linear_map.uniform_space
- continuous_linear_map.uniform_add_group
- continuous_linear_map.t2_space
- continuous_linear_map.has_op_norm
- continuous_linear_map.to_pseudo_metric_space
- continuous_linear_map.to_seminormed_add_comm_group
- continuous_linear_map.to_normed_space
- continuous_linear_map.to_semi_normed_ring
- continuous_linear_map.to_normed_algebra
- continuous_linear_map.norm_one_class
- continuous_linear_map.to_normed_add_comm_group
- continuous_linear_map.to_normed_ring
- continuous_linear_map.complete_space
- continuous_linear_map.finite_dimensional
- linear_map.can_lift_continuous_linear_map
- continuous_linear_map.topological_space.second_countable_topology
- continuous_linear_map.has_star
- continuous_linear_map.has_involutive_star
- continuous_linear_map.star_semigroup
- continuous_linear_map.star_ring
- continuous_linear_map.star_module
- continuous_linear_map.cstar_ring
- continuous_linear_map.has_le
- von_neumann_algebra.continuous_linear_map.set_like
- von_neumann_algebra.continuous_linear_map.star_mem_class
- von_neumann_algebra.continuous_linear_map.subring_class
@[class]
structure
continuous_semilinear_map_class
(F : Type u_1)
{R : out_param (Type u_2)}
{S : out_param (Type u_3)}
[semiring R]
[semiring S]
(σ : out_param (R →+* S))
(M : out_param (Type u_4))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_5))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_1 u_4 u_5)
- coe : F → Π (a : M), (λ (_x : M), M₂) a
- coe_injective' : function.injective continuous_semilinear_map_class.coe
- map_add : ∀ (f : F) (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y
- map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x
- map_continuous : ∀ (f : F), continuous ⇑f
continuous_semilinear_map_class F σ M M₂ asserts F is a type of bundled continuous
σ-semilinear maps M → M₂. See also continuous_linear_map_class F R M M₂ for the case where
σ is the identity map on R. A map f between an R-module and an S-module over a ring
homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x.
Instances of this typeclass
- continuous_semilinear_equiv_class.continuous_semilinear_map_class
- semilinear_isometry_class.continuous_semilinear_map_class
- continuous_linear_map.continuous_semilinear_map_class
- linear_map.continuous_linear_map_class_of_finite_dimensional
- weak_dual.weak_dual.continuous_linear_map_class
- normed_space.continuous_linear_map_class
Instances of other typeclasses for continuous_semilinear_map_class
- continuous_semilinear_map_class.has_sizeof_inst
@[instance]
def
continuous_semilinear_map_class.to_semilinear_map_class
(F : Type u_1)
{R : out_param (Type u_2)}
{S : out_param (Type u_3)}
[semiring R]
[semiring S]
(σ : out_param (R →+* S))
(M : out_param (Type u_4))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_5))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂]
[self : continuous_semilinear_map_class F σ M M₂] :
semilinear_map_class F σ M M₂
@[nolint, instance]
def
continuous_semilinear_map_class.to_continuous_map_class
(F : Type u_1)
{R : out_param (Type u_2)}
{S : out_param (Type u_3)}
[semiring R]
[semiring S]
(σ : out_param (R →+* S))
(M : out_param (Type u_4))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_5))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂]
[self : continuous_semilinear_map_class F σ M M₂] :
continuous_map_class F M M₂
@[reducible]
def
continuous_linear_map_class
(F : Type u_1)
(R : out_param (Type u_2))
[semiring R]
(M : out_param (Type u_3))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_4))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Type (max u_1 u_3 u_4)
continuous_linear_map_class F R M M₂ asserts F is a type of bundled continuous
R-linear maps M → M₂. This is an abbreviation for
continuous_semilinear_map_class F (ring_hom.id R) M M₂.
@[nolint]
structure
continuous_linear_equiv
{R : Type u_1}
{S : Type u_2}
[semiring R]
[semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
(M : Type u_3)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_4)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_3 u_4)
- to_linear_equiv : M ≃ₛₗ[σ] M₂
- continuous_to_fun : continuous self.to_linear_equiv.to_fun . "continuity'"
- continuous_inv_fun : continuous self.to_linear_equiv.inv_fun . "continuity'"
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M and M₂ will be topological modules over the
topological semiring R.
Instances for continuous_linear_equiv
- continuous_linear_equiv.has_sizeof_inst
- continuous_linear_equiv.continuous_linear_map.has_coe
- continuous_linear_equiv.continuous_semilinear_equiv_class
- continuous_linear_equiv.has_coe_to_fun
- continuous_linear_equiv.automorphism_group
- linear_isometry_equiv.continuous_linear_equiv.has_coe_t
- linear_equiv.can_lift_continuous_linear_equiv
@[class]
structure
continuous_semilinear_equiv_class
(F : Type u_1)
{R : out_param (Type u_2)}
{S : out_param (Type u_3)}
[semiring R]
[semiring S]
(σ : out_param (R →+* S))
{σ' : out_param (S →+* R)}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
(M : out_param (Type u_4))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_5))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_1 u_4 u_5)
- coe : F → M → M₂
- inv : F → M₂ → M
- left_inv : ∀ (e : F), function.left_inverse (continuous_semilinear_equiv_class.inv e) (continuous_semilinear_equiv_class.coe e)
- right_inv : ∀ (e : F), function.right_inverse (continuous_semilinear_equiv_class.inv e) (continuous_semilinear_equiv_class.coe e)
- coe_injective' : ∀ (e g : F), continuous_semilinear_equiv_class.coe e = continuous_semilinear_equiv_class.coe g → continuous_semilinear_equiv_class.inv e = continuous_semilinear_equiv_class.inv g → e = g
- map_add : ∀ (f : F) (a b : M), ⇑f (a + b) = ⇑f a + ⇑f b
- map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x
- map_continuous : (∀ (f : F), continuous ⇑f) . "continuity'"
- inv_continuous : (∀ (f : F), continuous (continuous_semilinear_equiv_class.inv f)) . "continuity'"
continuous_semilinear_equiv_class F σ M M₂ asserts F is a type of bundled continuous
σ-semilinear equivs M → M₂. See also continuous_linear_equiv_class F R M M₂ for the case
where σ is the identity map on R. A map f between an R-module and an S-module over a ring
homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x.
Instances of this typeclass
Instances of other typeclasses for continuous_semilinear_equiv_class
- continuous_semilinear_equiv_class.has_sizeof_inst
@[instance]
def
continuous_semilinear_equiv_class.to_semilinear_equiv_class
(F : Type u_1)
{R : out_param (Type u_2)}
{S : out_param (Type u_3)}
[semiring R]
[semiring S]
(σ : out_param (R →+* S))
{σ' : out_param (S →+* R)}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
(M : out_param (Type u_4))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_5))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂]
[self : continuous_semilinear_equiv_class F σ M M₂] :
semilinear_equiv_class F σ M M₂
@[reducible]
def
continuous_linear_equiv_class
(F : Type u_1)
(R : out_param (Type u_2))
[semiring R]
(M : out_param (Type u_3))
[topological_space M]
[add_comm_monoid M]
(M₂ : out_param (Type u_4))
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Type (max u_1 u_3 u_4)
continuous_linear_equiv_class F σ M M₂ asserts F is a type of bundled continuous
R-linear equivs M → M₂. This is an abbreviation for
continuous_semilinear_equiv_class F (ring_hom.id) M M₂.
@[protected, nolint, instance]
def
continuous_semilinear_equiv_class.continuous_semilinear_map_class
(F : Type u_1)
{R : Type u_2}
{S : Type u_3}
[semiring R]
[semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[ring_hom_inv_pair σ σ']
[ring_hom_inv_pair σ' σ]
(M : Type u_4)
[topological_space M]
[add_comm_monoid M]
(M₂ : Type u_5)
[topological_space M₂]
[add_comm_monoid M₂]
[module R M]
[module S M₂]
[s : continuous_semilinear_equiv_class F σ M M₂] :
continuous_semilinear_map_class F σ M M₂
Equations
- continuous_semilinear_equiv_class.continuous_semilinear_map_class F σ M M₂ = {coe := continuous_semilinear_equiv_class.coe s, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
theorem
is_closed_set_of_map_smul
(M₁ : Type u_1)
(M₂ : Type u_2)
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
(σ : R →+* S) :
@[simp]
theorem
linear_map_of_mem_closure_range_coe_apply
{M₁ : Type u_1}
{M₂ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
(f : M₁ → M₂)
(hf : f ∈ closure (set.range coe_fn)) :
⇑(linear_map_of_mem_closure_range_coe f hf) = f
def
linear_map_of_mem_closure_range_coe
{M₁ : Type u_1}
{M₂ : Type u_2}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
(f : M₁ → M₂)
(hf : f ∈ closure (set.range coe_fn)) :
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
def
linear_map_of_tendsto
{M₁ : Type u_1}
{M₂ : Type u_2}
{α : Type u_3}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
{l : filter α}
(f : M₁ → M₂)
(g : α → (M₁ →ₛₗ[σ] M₂))
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (nhds f)) :
Construct a bundled linear map from a pointwise limit of linear maps
Equations
@[simp]
theorem
linear_map_of_tendsto_apply
{M₁ : Type u_1}
{M₂ : Type u_2}
{α : Type u_3}
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
{σ : R →+* S}
{l : filter α}
(f : M₁ → M₂)
(g : α → (M₁ →ₛₗ[σ] M₂))
[l.ne_bot]
(h : filter.tendsto (λ (a : α) (x : M₁), ⇑(g a) x) l (nhds f)) :
⇑(linear_map_of_tendsto f g h) = f
theorem
linear_map.is_closed_range_coe
(M₁ : Type u_1)
(M₂ : Type u_2)
{R : Type u_4}
{S : Type u_5}
[topological_space M₂]
[t2_space M₂]
[semiring R]
[semiring S]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module S M₂]
[has_continuous_const_smul S M₂]
[has_continuous_add M₂]
(σ : R →+* S) :
Properties that hold for non-necessarily commutative semirings. #
@[protected, instance]
def
continuous_linear_map.linear_map.has_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear maps to linear maps.
Equations
@[simp]
theorem
continuous_linear_map.to_linear_map_eq_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
f.to_linear_map = ↑f
theorem
continuous_linear_map.coe_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[protected, instance]
def
continuous_linear_map.continuous_semilinear_map_class
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
continuous_semilinear_map_class (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂
Equations
- continuous_linear_map.continuous_semilinear_map_class = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
@[protected, instance]
def
continuous_linear_map.to_fun
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear maps to functions.
Equations
- continuous_linear_map.to_fun = {coe := λ (f : M₁ →SL[σ₁₂] M₂), f.to_linear_map.to_fun}
@[simp]
theorem
continuous_linear_map.coe_mk
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
(h : continuous f.to_fun . "continuity'") :
↑{to_linear_map := f, cont := h} = f
@[simp]
theorem
continuous_linear_map.coe_mk'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
(h : continuous f.to_fun . "continuity'") :
@[protected, continuity]
theorem
continuous_linear_map.continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_map.uniform_continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{E₁ : Type u_3}
{E₂ : Type u_4}
[uniform_space E₁]
[uniform_space E₂]
[add_comm_group E₁]
[add_comm_group E₂]
[module R₁ E₁]
[module R₂ E₂]
[uniform_add_group E₁]
[uniform_add_group E₂]
(f : E₁ →SL[σ₁₂] E₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inj
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂} :
theorem
continuous_linear_map.coe_fn_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
def
continuous_linear_map.simps.apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ →SL[σ₁₂] M₂) :
M₁ → M₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
continuous_linear_map.simps.coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ →SL[σ₁₂] M₂) :
See Note [custom simps projection].
Equations
@[ext]
theorem
continuous_linear_map.ext
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂}
(h : ∀ (x : M₁), ⇑f x = ⇑g x) :
f = g
theorem
continuous_linear_map.ext_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂} :
@[protected]
def
continuous_linear_map.copy
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(f' : M₁ → M₂)
(h : f' = ⇑f) :
Copy of a continuous_linear_map with a new to_fun equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_linear_map := f.to_linear_map.copy f' h, cont := _}
@[simp]
theorem
continuous_linear_map.coe_copy
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(f' : M₁ → M₂)
(h : f' = ⇑f) :
theorem
continuous_linear_map.copy_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(f' : M₁ → M₂)
(h : f' = ⇑f) :
@[protected]
theorem
continuous_linear_map.map_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_map.map_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(x y : M₁) :
@[protected, simp]
theorem
continuous_linear_map.map_smulₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(c : R₁)
(x : M₁) :
@[protected, simp]
theorem
continuous_linear_map.map_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(f : M₁ →L[R₁] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_map.map_smul_of_tower
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_1}
{S : Type u_2}
[semiring S]
[has_smul R M₁]
[module S M₁]
[has_smul R M₂]
[module S M₂]
[linear_map.compatible_smul M₁ M₂ R S]
(f : M₁ →L[S] M₂)
(c : R)
(x : M₁) :
@[protected]
theorem
continuous_linear_map.map_sum
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{ι : Type u_3}
(f : M₁ →SL[σ₁₂] M₂)
(s : finset ι)
(g : ι → M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
@[ext]
theorem
continuous_linear_map.ext_ring
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ →L[R₁] M₁}
(h : ⇑f 1 = ⇑g 1) :
f = g
theorem
continuous_linear_map.ext_ring_iff
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ →L[R₁] M₁} :
theorem
continuous_linear_map.eq_on_closure_span
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[t2_space M₂]
{s : set M₁}
{f g : M₁ →SL[σ₁₂] M₂}
(h : set.eq_on ⇑f ⇑g s) :
If two continuous linear maps are equal on a set s, then they are equal on the closure
of the submodule.span of this set.
theorem
continuous_linear_map.ext_on
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[t2_space M₂]
{s : set M₁}
(hs : dense ↑(submodule.span R₁ s))
{f g : M₁ →SL[σ₁₂] M₂}
(h : set.eq_on ⇑f ⇑g s) :
f = g
If the submodule generated by a set s is dense in the ambient module, then two continuous
linear maps equal on s are equal.
theorem
submodule.topological_closure_map
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
[topological_space R₁]
[topological_space R₂]
[has_continuous_smul R₁ M₁]
[has_continuous_add M₁]
[has_continuous_smul R₂ M₂]
[has_continuous_add M₂]
(f : M₁ →SL[σ₁₂] M₂)
(s : submodule R₁ M₁) :
Under a continuous linear map, the image of the topological_closure of a submodule is
contained in the topological_closure of its image.
theorem
dense_range.topological_closure_map_submodule
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[ring_hom_surjective σ₁₂]
[topological_space R₁]
[topological_space R₂]
[has_continuous_smul R₁ M₁]
[has_continuous_add M₁]
[has_continuous_smul R₂ M₂]
[has_continuous_add M₂]
{f : M₁ →SL[σ₁₂] M₂}
(hf' : dense_range ⇑f)
{s : submodule R₁ M₁}
(hs : s.topological_closure = ⊤) :
(submodule.map ↑f s).topological_closure = ⊤
Under a dense continuous linear map, a submodule whose topological_closure is ⊤ is sent to
another such submodule. That is, the image of a dense set under a map with dense range is dense.
@[protected, instance]
def
continuous_linear_map.mul_action
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂] :
mul_action S₂ (M₁ →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.mul_action = {to_has_smul := {smul := λ (c : S₂) (f : M₁ →SL[σ₁₂] M₂), {to_linear_map := c • ↑f, cont := _}}, one_smul := _, mul_smul := _}
theorem
continuous_linear_map.smul_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_smul'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
[monoid S₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
(c : S₂)
(f : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.is_scalar_tower
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
{T₂ : Type u_10}
[monoid S₂]
[monoid T₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
[distrib_mul_action T₂ M₂]
[smul_comm_class R₂ T₂ M₂]
[has_continuous_const_smul T₂ M₂]
[has_smul S₂ T₂]
[is_scalar_tower S₂ T₂ M₂] :
is_scalar_tower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def
continuous_linear_map.smul_comm_class
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{S₂ : Type u_9}
{T₂ : Type u_10}
[monoid S₂]
[monoid T₂]
[distrib_mul_action S₂ M₂]
[smul_comm_class R₂ S₂ M₂]
[has_continuous_const_smul S₂ M₂]
[distrib_mul_action T₂ M₂]
[smul_comm_class R₂ T₂ M₂]
[has_continuous_const_smul T₂ M₂]
[smul_comm_class S₂ T₂ M₂] :
smul_comm_class S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[protected, instance]
def
continuous_linear_map.has_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
The continuous map that is constantly zero.
Equations
- continuous_linear_map.has_zero = {zero := {to_linear_map := 0, cont := _}}
@[protected, instance]
def
continuous_linear_map.inhabited
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Equations
@[simp]
theorem
continuous_linear_map.default_def
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[simp]
theorem
continuous_linear_map.zero_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[norm_cast]
theorem
continuous_linear_map.coe_zero'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[protected, instance]
def
continuous_linear_map.unique_of_left
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[subsingleton M₁] :
@[protected, instance]
def
continuous_linear_map.unique_of_right
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[subsingleton M₂] :
theorem
continuous_linear_map.exists_ne_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f : M₁ →SL[σ₁₂] M₂}
(hf : f ≠ 0) :
def
continuous_linear_map.id
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
the identity map as a continuous linear map.
Equations
- continuous_linear_map.id R₁ M₁ = {to_linear_map := linear_map.id _inst_14, cont := _}
@[protected, instance]
def
continuous_linear_map.has_one
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
Equations
- continuous_linear_map.has_one = {one := continuous_linear_map.id R₁ M₁ _inst_14}
theorem
continuous_linear_map.one_def
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
1 = continuous_linear_map.id R₁ M₁
theorem
continuous_linear_map.id_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(x : M₁) :
⇑(continuous_linear_map.id R₁ M₁) x = x
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
↑(continuous_linear_map.id R₁ M₁) = linear_map.id
@[simp, norm_cast]
theorem
continuous_linear_map.coe_id'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
⇑(continuous_linear_map.id R₁ M₁) = id
@[simp, norm_cast]
theorem
continuous_linear_map.coe_eq_id
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{f : M₁ →L[R₁] M₁} :
↑f = linear_map.id ↔ f = continuous_linear_map.id R₁ M₁
@[simp]
theorem
continuous_linear_map.one_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(x : M₁) :
@[protected, instance]
def
continuous_linear_map.has_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂] :
@[simp]
theorem
continuous_linear_map.add_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂) :
@[norm_cast]
theorem
continuous_linear_map.coe_add'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
(f g : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.add_comm_monoid
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂] :
add_comm_monoid (M₁ →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.add_comm_monoid = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul mul_action.to_has_smul, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂)) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sum'
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂)) :
theorem
continuous_linear_map.sum_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
[has_continuous_add M₂]
{ι : Type u_3}
(t : finset ι)
(f : ι → (M₁ →SL[σ₁₂] M₂))
(b : M₁) :
def
continuous_linear_map.comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
Composition of bounded linear maps.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(h : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_comp'
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(h : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
theorem
continuous_linear_map.comp_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂)
(x : M₁) :
@[simp]
theorem
continuous_linear_map.comp_id
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
f.comp (continuous_linear_map.id R₁ M₁) = f
@[simp]
theorem
continuous_linear_map.id_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂) :
(continuous_linear_map.id R₂ M₂).comp f = f
@[simp]
theorem
continuous_linear_map.comp_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →SL[σ₂₃] M₃) :
@[simp]
theorem
continuous_linear_map.zero_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_add
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[has_continuous_add M₂]
[has_continuous_add M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f₁ f₂ : M₁ →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.add_comp
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[has_continuous_add M₃]
(g₁ g₂ : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
theorem
continuous_linear_map.comp_assoc
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{R₄ : Type u_5}
[semiring R₄]
[module R₄ M₄]
{σ₁₄ : R₁ →+* R₄}
{σ₂₄ : R₂ →+* R₄}
{σ₃₄ : R₃ →+* R₄}
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
[ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄]
[ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
(h : M₃ →SL[σ₃₄] M₄)
(g : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.has_mul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
Equations
- continuous_linear_map.has_mul = {mul := continuous_linear_map.comp continuous_linear_map.has_mul._proof_1}
theorem
continuous_linear_map.mul_def
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(f g : M₁ →L[R₁] M₁) :
theorem
continuous_linear_map.mul_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(f g : M₁ →L[R₁] M₁)
(x : M₁) :
@[protected, instance]
def
continuous_linear_map.monoid_with_zero
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
monoid_with_zero (M₁ →L[R₁] M₁)
Equations
- continuous_linear_map.monoid_with_zero = {mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul continuous_linear_map.monoid_with_zero._proof_4 continuous_linear_map.monoid_with_zero._proof_5, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}
@[protected, instance]
def
continuous_linear_map.semiring
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
Equations
- continuous_linear_map.semiring = {add := add_comm_monoid.add continuous_linear_map.add_comm_monoid, add_assoc := _, zero := monoid_with_zero.zero continuous_linear_map.monoid_with_zero, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul continuous_linear_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul continuous_linear_map.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast._default 1 add_comm_monoid.add continuous_linear_map.semiring._proof_14 monoid_with_zero.zero continuous_linear_map.semiring._proof_15 continuous_linear_map.semiring._proof_16 add_comm_monoid.nsmul continuous_linear_map.semiring._proof_17 continuous_linear_map.semiring._proof_18, nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow continuous_linear_map.monoid_with_zero, npow_zero' := _, npow_succ' := _}
def
continuous_linear_map.to_linear_map_ring_hom
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
continuous_linear_map.to_linear_map as a ring_hom.
Equations
- continuous_linear_map.to_linear_map_ring_hom = {to_fun := continuous_linear_map.to_linear_map _inst_14, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
continuous_linear_map.to_linear_map_ring_hom_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁]
(self : M₁ →L[R₁] M₁) :
@[protected, instance]
def
continuous_linear_map.apply_module
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
The tautological action by M₁ →L[R₁] M₁ on M.
This generalizes function.End.apply_mul_action.
@[protected, simp]
theorem
continuous_linear_map.smul_def
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁]
(f : M₁ →L[R₁] M₁)
(a : M₁) :
@[protected, instance]
def
continuous_linear_map.apply_has_faithful_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
has_faithful_smul (M₁ →L[R₁] M₁) M₁
continuous_linear_map.apply_module is faithful.
@[protected, instance]
def
continuous_linear_map.apply_smul_comm_class
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
smul_comm_class R₁ (M₁ →L[R₁] M₁) M₁
@[protected, instance]
def
continuous_linear_map.apply_smul_comm_class'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
smul_comm_class (M₁ →L[R₁] M₁) R₁ M₁
@[protected, instance]
def
continuous_linear_map.has_continuous_const_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[has_continuous_add M₁] :
has_continuous_const_smul (M₁ →L[R₁] M₁) M₁
@[protected]
def
continuous_linear_map.prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃) :
The cartesian product of two bounded linear maps, as a bounded linear map.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃) :
@[simp, norm_cast]
theorem
continuous_linear_map.prod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₁ →L[R₁] M₃)
(x : M₁) :
def
continuous_linear_map.inl
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
The left injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inl R₁ M₁ M₂ = (continuous_linear_map.id R₁ M₁).prod 0
def
continuous_linear_map.inr
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
The right injection into a product is a continuous linear map.
Equations
- continuous_linear_map.inr R₁ M₁ M₂ = 0.prod (continuous_linear_map.id R₁ M₂)
@[simp]
theorem
continuous_linear_map.inl_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(x : M₁) :
⇑(continuous_linear_map.inl R₁ M₁ M₂) x = (x, 0)
@[simp]
theorem
continuous_linear_map.inr_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(x : M₂) :
⇑(continuous_linear_map.inr R₁ M₁ M₂) x = (0, x)
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inl
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.inl R₁ M₁ M₂) = linear_map.inl R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_inr
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.inr R₁ M₁ M₂) = linear_map.inr R₁ M₁ M₂
theorem
continuous_linear_map.is_closed_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{F : Type u_9}
[t1_space M₂]
[continuous_semilinear_map_class F σ₁₂ M₁ M₂]
(f : F) :
theorem
continuous_linear_map.is_complete_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{F : Type u_9}
{M' : Type u_3}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R₁ M']
[t1_space M₂]
[continuous_semilinear_map_class F σ₁₂ M' M₂]
(f : F) :
@[protected, instance]
def
continuous_linear_map.complete_space_ker
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{F : Type u_9}
{M' : Type u_3}
[uniform_space M']
[complete_space M']
[add_comm_monoid M']
[module R₁ M']
[t1_space M₂]
[continuous_semilinear_map_class F σ₁₂ M' M₂]
(f : F) :
@[simp]
theorem
continuous_linear_map.ker_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
linear_map.ker (f.prod g) = linear_map.ker f ⊓ linear_map.ker g
def
continuous_linear_map.cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
Restrict codomain of a continuous linear map.
Equations
- f.cod_restrict p h = {to_linear_map := linear_map.cod_restrict p ↑f h, cont := _}
@[norm_cast]
theorem
continuous_linear_map.coe_cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
↑(f.cod_restrict p h) = linear_map.cod_restrict p ↑f h
@[simp]
theorem
continuous_linear_map.coe_cod_restrict_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p)
(x : M₁) :
↑(⇑(f.cod_restrict p h) x) = ⇑f x
@[simp]
theorem
continuous_linear_map.ker_cod_restrict
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ →SL[σ₁₂] M₂)
(p : submodule R₂ M₂)
(h : ∀ (x : M₁), ⇑f x ∈ p) :
linear_map.ker (f.cod_restrict p h) = linear_map.ker f
def
submodule.subtypeL
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
@[simp, norm_cast]
theorem
submodule.coe_subtypeL
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
@[simp]
theorem
submodule.coe_subtypeL'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
@[simp, norm_cast]
theorem
submodule.subtypeL_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁)
(x : ↥p) :
@[simp]
theorem
submodule.range_subtypeL
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
@[simp]
theorem
submodule.ker_subtypeL
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
(p : submodule R₁ M₁) :
def
continuous_linear_map.fst
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
prod.fst as a continuous_linear_map.
Equations
- continuous_linear_map.fst R₁ M₁ M₂ = {to_linear_map := linear_map.fst R₁ M₁ M₂ _inst_19, cont := _}
def
continuous_linear_map.snd
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
(M₂ : Type u_6)
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
prod.snd as a continuous_linear_map.
Equations
- continuous_linear_map.snd R₁ M₁ M₂ = {to_linear_map := linear_map.snd R₁ M₁ M₂ _inst_19, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.fst R₁ M₁ M₂) = linear_map.fst R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_fst'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
⇑(continuous_linear_map.fst R₁ M₁ M₂) = prod.fst
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
↑(continuous_linear_map.snd R₁ M₁ M₂) = linear_map.snd R₁ M₁ M₂
@[simp, norm_cast]
theorem
continuous_linear_map.coe_snd'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
⇑(continuous_linear_map.snd R₁ M₁ M₂) = prod.snd
@[simp]
theorem
continuous_linear_map.fst_prod_snd
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂] :
(continuous_linear_map.fst R₁ M₁ M₂).prod (continuous_linear_map.snd R₁ M₁ M₂) = continuous_linear_map.id R₁ (M₁ × M₂)
@[simp]
theorem
continuous_linear_map.fst_comp_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
(continuous_linear_map.fst R₁ M₂ M₃).comp (f.prod g) = f
@[simp]
theorem
continuous_linear_map.snd_comp_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
(f : M₁ →L[R₁] M₂)
(g : M₁ →L[R₁] M₃) :
(continuous_linear_map.snd R₁ M₂ M₃).comp (f.prod g) = g
def
continuous_linear_map.prod_map
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
prod.map of two continuous linear maps.
Equations
- f₁.prod_map f₂ = (f₁.comp (continuous_linear_map.fst R₁ M₁ M₃)).prod (f₂.comp (continuous_linear_map.snd R₁ M₁ M₃))
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod_map
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_prod_map'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(f₁ : M₁ →L[R₁] M₂)
(f₂ : M₃ →L[R₁] M₄) :
def
continuous_linear_map.coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.
@[simp, norm_cast]
theorem
continuous_linear_map.coe_coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
@[simp]
theorem
continuous_linear_map.coprod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃)
(x : M₁ × M₂) :
theorem
continuous_linear_map.range_coprod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f₁ : M₁ →L[R₁] M₃)
(f₂ : M₂ →L[R₁] M₃) :
linear_map.range (f₁.coprod f₂) = linear_map.range f₁ ⊔ linear_map.range f₂
theorem
continuous_linear_map.comp_fst_add_comp_snd
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[has_continuous_add M₃]
(f : M₁ →L[R₁] M₃)
(g : M₂ →L[R₁] M₃) :
f.comp (continuous_linear_map.fst R₁ M₁ M₂) + g.comp (continuous_linear_map.snd R₁ M₁ M₂) = f.coprod g
theorem
continuous_linear_map.coprod_inl_inr
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M'₁ : Type u_5}
[topological_space M'₁]
[add_comm_monoid M'₁]
[module R₁ M₁]
[module R₁ M'₁]
[has_continuous_add M₁]
[has_continuous_add M'₁] :
(continuous_linear_map.inl R₁ M₁ M'₁).coprod (continuous_linear_map.inr R₁ M₁ M'₁) = continuous_linear_map.id R₁ (M₁ × M'₁)
def
continuous_linear_map.smul_right
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_10}
{S : Type u_11}
[semiring R]
[semiring S]
[module R M₁]
[module R M₂]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
(c : M₁ →L[R] S)
(f : M₂) :
The linear map λ x, c x • f. Associates to a scalar-valued linear map and an element of
M₂ the M₂-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂).
See also continuous_linear_map.smul_rightₗ and continuous_linear_map.smul_rightL.
Equations
- c.smul_right f = {to_linear_map := {to_fun := (c.to_linear_map.smul_right f).to_fun, map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
continuous_linear_map.smul_right_apply
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{R : Type u_10}
{S : Type u_11}
[semiring R]
[semiring S]
[module R M₁]
[module R M₂]
[module R S]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[has_continuous_smul S M₂]
{c : M₁ →L[R] S}
{f : M₂}
{x : M₁} :
⇑(c.smul_right f) x = ⇑c x • f
@[simp]
theorem
continuous_linear_map.smul_right_one_one
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
(c : R₁ →L[R₁] M₂) :
1.smul_right (⇑c 1) = c
@[simp]
theorem
continuous_linear_map.smul_right_one_eq_iff
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
{f f' : M₂} :
1.smul_right f = 1.smul_right f' ↔ f = f'
theorem
continuous_linear_map.smul_right_comp
{R₁ : Type u_1}
[semiring R₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₂]
[topological_space R₁]
[has_continuous_smul R₁ M₂]
[has_continuous_mul R₁]
{x : M₂}
{c : R₁} :
(1.smul_right x).comp (1.smul_right c) = 1.smul_right (c • x)
def
continuous_linear_map.to_span_singleton
(R₁ : Type u_1)
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
[has_continuous_smul R₁ M₁]
(x : M₁) :
Given an element x of a topological space M over a semiring R, the natural continuous
linear map from R to M by taking multiples of x.
Equations
- continuous_linear_map.to_span_singleton R₁ x = {to_linear_map := linear_map.to_span_singleton R₁ M₁ x, cont := _}
theorem
continuous_linear_map.to_span_singleton_apply
(R₁ : Type u_1)
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
[has_continuous_smul R₁ M₁]
(x : M₁)
(r : R₁) :
⇑(continuous_linear_map.to_span_singleton R₁ x) r = r • x
theorem
continuous_linear_map.to_span_singleton_add
(R₁ : Type u_1)
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
[has_continuous_smul R₁ M₁]
[has_continuous_add M₁]
(x y : M₁) :
theorem
continuous_linear_map.to_span_singleton_smul'
(R₁ : Type u_1)
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
[has_continuous_smul R₁ M₁]
{α : Type u_2}
[monoid α]
[distrib_mul_action α M₁]
[has_continuous_const_smul α M₁]
[smul_comm_class R₁ α M₁]
(c : α)
(x : M₁) :
theorem
continuous_linear_map.to_span_singleton_smul
(R : Type u_1)
{M₁ : Type u_2}
[comm_semiring R]
[add_comm_monoid M₁]
[module R M₁]
[topological_space R]
[topological_space M₁]
[has_continuous_smul R M₁]
(c : R)
(x : M₁) :
A special case of to_span_singleton_smul' for when R is commutative.
def
continuous_linear_map.pi
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
pi construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules.
Equations
- continuous_linear_map.pi f = {to_linear_map := linear_map.pi (λ (i : ι), ↑(f i)), cont := _}
@[simp]
theorem
continuous_linear_map.coe_pi'
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
⇑(continuous_linear_map.pi f) = λ (c : M) (i : ι), ⇑(f i) c
@[simp]
theorem
continuous_linear_map.coe_pi
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
↑(continuous_linear_map.pi f) = linear_map.pi (λ (i : ι), ↑(f i))
theorem
continuous_linear_map.pi_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i)
(c : M)
(i : ι) :
⇑(continuous_linear_map.pi f) c i = ⇑(f i) c
theorem
continuous_linear_map.pi_eq_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i) :
continuous_linear_map.pi f = 0 ↔ ∀ (i : ι), f i = 0
theorem
continuous_linear_map.pi_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
continuous_linear_map.pi (λ (i : ι), 0) = 0
theorem
continuous_linear_map.pi_comp
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M →L[R] φ i)
(g : M₂ →L[R] M) :
(continuous_linear_map.pi f).comp g = continuous_linear_map.pi (λ (i : ι), (f i).comp g)
def
continuous_linear_map.proj
{R : Type u_1}
[semiring R]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι) :
The projections from a family of topological modules are continuous linear maps.
Equations
- continuous_linear_map.proj i = {to_linear_map := linear_map.proj i, cont := _}
@[simp]
theorem
continuous_linear_map.proj_apply
{R : Type u_1}
[semiring R]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι)
(b : Π (i : ι), φ i) :
⇑(continuous_linear_map.proj i) b = b i
theorem
continuous_linear_map.proj_pi
{R : Type u_1}
[semiring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_monoid M₂]
[module R M₂]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →L[R] φ i)
(i : ι) :
(continuous_linear_map.proj i).comp (continuous_linear_map.pi f) = f i
theorem
continuous_linear_map.infi_ker_proj
{R : Type u_1}
[semiring R]
{ι : Type u_4}
{φ : ι → Type u_5}
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
(⨅ (i : ι), linear_map.ker (continuous_linear_map.proj i)) = ⊥
def
continuous_linear_map.infi_ker_proj_equiv
(R : Type u_1)
[semiring R]
{ι : Type u_4}
(φ : ι → Type u_5)
[Π (i : ι), topological_space (φ i)]
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I J : set ι}
[decidable_pred (λ (i : ι), i ∈ I)]
(hd : disjoint I J)
(hu : set.univ ⊆ I ∪ J) :
If I and J are complementary index sets, the product of the kernels of the Jth projections
of φ is linearly equivalent to the product over I.
Equations
- continuous_linear_map.infi_ker_proj_equiv R φ hd hu = {to_linear_equiv := linear_map.infi_ker_proj_equiv R φ hd hu, continuous_to_fun := _, continuous_inv_fun := _}
@[protected]
theorem
continuous_linear_map.map_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →SL[σ₁₂] M₂)
(x : M) :
@[protected]
theorem
continuous_linear_map.map_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f : M →SL[σ₁₂] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_map.sub_apply'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
(f g : M →SL[σ₁₂] M₂)
(x : M) :
theorem
continuous_linear_map.range_prod_eq
{R : Type u_1}
[ring R]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
{f : M →L[R] M₂}
{g : M →L[R] M₃}
(h : linear_map.ker f ⊔ linear_map.ker g = ⊤) :
linear_map.range (f.prod g) = (linear_map.range f).prod (linear_map.range g)
theorem
continuous_linear_map.ker_prod_ker_le_ker_coprod
{R : Type u_1}
[ring R]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃) :
(linear_map.ker f).prod (linear_map.ker g) ≤ linear_map.ker (f.coprod g)
theorem
continuous_linear_map.ker_coprod_of_disjoint_range
{R : Type u_1}
[ring R]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R M₂]
[module R M₃]
[has_continuous_add M₃]
(f : M →L[R] M₃)
(g : M₂ →L[R] M₃)
(hd : disjoint (linear_map.range f) (linear_map.range g)) :
linear_map.ker (f.coprod g) = (linear_map.ker f).prod (linear_map.ker g)
@[protected, instance]
def
continuous_linear_map.has_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
@[simp]
theorem
continuous_linear_map.neg_apply
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂)
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂) :
@[norm_cast]
theorem
continuous_linear_map.coe_neg'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.has_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
@[protected, instance]
def
continuous_linear_map.add_comm_group
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂] :
add_comm_group (M →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.add_comm_group = {add := has_add.add continuous_linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul add_monoid.has_smul_nat, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg continuous_linear_map.has_neg, sub := has_sub.sub continuous_linear_map.has_sub, sub_eq_add_neg := _, zsmul := has_smul.smul mul_action.to_has_smul, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
theorem
continuous_linear_map.sub_apply
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂)
(x : M) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂) :
@[simp, norm_cast]
theorem
continuous_linear_map.coe_sub'
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[topological_add_group M₂]
(f g : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{R₃ : Type u_3}
[ring R₃]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[topological_add_group M₂]
[topological_add_group M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.neg_comp
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{R₃ : Type u_3}
[ring R₃]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[topological_add_group M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{R₃ : Type u_3}
[ring R₃]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[topological_add_group M₂]
[topological_add_group M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f₁ f₂ : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.sub_comp
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{R₃ : Type u_3}
[ring R₃]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_6}
[topological_space M₃]
[add_comm_group M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[topological_add_group M₃]
(g₁ g₂ : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.ring
{R : Type u_1}
[ring R]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M] :
Equations
- continuous_linear_map.ring = {add := semiring.add continuous_linear_map.semiring, add_assoc := _, zero := semiring.zero continuous_linear_map.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul continuous_linear_map.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg continuous_linear_map.add_comm_group, sub := add_comm_group.sub continuous_linear_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul continuous_linear_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add continuous_linear_map.ring._proof_13 semiring.zero continuous_linear_map.ring._proof_14 continuous_linear_map.ring._proof_15 semiring.nsmul continuous_linear_map.ring._proof_16 continuous_linear_map.ring._proof_17 1 continuous_linear_map.ring._proof_18 continuous_linear_map.ring._proof_19 add_comm_group.neg add_comm_group.sub continuous_linear_map.ring._proof_20 add_comm_group.zsmul continuous_linear_map.ring._proof_21 continuous_linear_map.ring._proof_22 continuous_linear_map.ring._proof_23 continuous_linear_map.ring._proof_24, nat_cast := semiring.nat_cast continuous_linear_map.semiring, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul continuous_linear_map.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow continuous_linear_map.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
theorem
continuous_linear_map.smul_right_one_pow
{R : Type u_1}
[ring R]
[topological_space R]
[topological_ring R]
(c : R)
(n : ℕ) :
1.smul_right c ^ n = 1.smul_right (c ^ n)
def
continuous_linear_map.proj_ker_of_right_inverse
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
M →L[R] ↥(linear_map.ker f₁)
Given a right inverse f₂ : M₂ →L[R] M to f₁ : M →L[R] M₂,
proj_ker_of_right_inverse f₁ f₂ h is the projection M →L[R] f₁.ker along f₂.range.
Equations
- f₁.proj_ker_of_right_inverse f₂ h = (continuous_linear_map.id R M - f₂.comp f₁).cod_restrict (linear_map.ker f₁) _
@[simp]
theorem
continuous_linear_map.coe_proj_ker_of_right_inverse_apply
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
@[simp]
theorem
continuous_linear_map.proj_ker_of_right_inverse_apply_idem
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : ↥(linear_map.ker f₁)) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) ↑x = x
@[simp]
theorem
continuous_linear_map.proj_ker_of_right_inverse_comp_inv
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_4}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_5}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[topological_add_group M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(y : M₂) :
⇑(f₁.proj_ker_of_right_inverse f₂ h) (⇑f₂ y) = 0
@[protected]
theorem
continuous_linear_map.is_open_map_of_ne_zero
{R : Type u_1}
{M : Type u_2}
[topological_space R]
[division_ring R]
[has_continuous_sub R]
[add_comm_group M]
[topological_space M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M]
(f : M →L[R] R)
(hf : f ≠ 0) :
A nonzero continuous linear functional is open.
@[simp]
theorem
continuous_linear_map.smul_comp
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₂]
[semiring R₃]
[monoid S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[distrib_mul_action S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(c : S₃)
(h : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_map.comp_smul
{R : Type u_1}
{S : Type u_4}
[semiring R]
[monoid S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[distrib_mul_action S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[distrib_mul_action S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[linear_map.compatible_smul N₂ N₃ S R]
(hₗ : N₂ →L[R] N₃)
(c : S)
(fₗ : M →L[R] N₂) :
@[simp]
theorem
continuous_linear_map.comp_smulₛₗ
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R]
[semiring R₂]
[semiring R₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[smul_comm_class R₂ R₂ M₂]
[smul_comm_class R₃ R₃ M₃]
[has_continuous_const_smul R₂ M₂]
[has_continuous_const_smul R₃ M₃]
(h : M₂ →SL[σ₂₃] M₃)
(c : R₂)
(f : M →SL[σ₁₂] M₂) :
@[protected, instance]
def
continuous_linear_map.distrib_mul_action
{R : Type u_1}
{R₂ : Type u_2}
{S₃ : Type u_5}
[semiring R]
[semiring R₂]
[monoid S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₂ : Type u_7}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[distrib_mul_action S₃ M₂]
[has_continuous_const_smul S₃ M₂]
[smul_comm_class R₂ S₃ M₂]
[has_continuous_add M₂] :
distrib_mul_action S₃ (M →SL[σ₁₂] M₂)
Equations
- continuous_linear_map.distrib_mul_action = {to_mul_action := continuous_linear_map.mul_action _inst_29, smul_zero := _, smul_add := _}
def
continuous_linear_map.prod_equiv
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃] :
continuous_linear_map.prod as an equiv.
@[simp]
theorem
continuous_linear_map.prod_equiv_apply
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
(f : (M →L[R] N₂) × (M →L[R] N₃)) :
theorem
continuous_linear_map.prod_ext_iff
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
{f g : M × N₂ →L[R] N₃} :
f = g ↔ f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂) ∧ f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)
@[ext]
theorem
continuous_linear_map.prod_ext
{R : Type u_1}
[semiring R]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
{f g : M × N₂ →L[R] N₃}
(hl : f.comp (continuous_linear_map.inl R M N₂) = g.comp (continuous_linear_map.inl R M N₂))
(hr : f.comp (continuous_linear_map.inr R M N₂) = g.comp (continuous_linear_map.inr R M N₂)) :
f = g
@[protected, instance]
def
continuous_linear_map.module
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₃ : R →+* R₃}
[has_continuous_add M₃] :
Equations
- continuous_linear_map.module = {to_distrib_mul_action := continuous_linear_map.distrib_mul_action _inst_32, add_smul := _, zero_smul := _}
@[protected, instance]
def
continuous_linear_map.is_central_scalar
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
{σ₁₃ : R →+* R₃}
[has_continuous_add M₃]
[module S₃ᵐᵒᵖ M₃]
[is_central_scalar S₃ M₃] :
is_central_scalar S₃ (M →SL[σ₁₃] M₃)
@[simp]
theorem
continuous_linear_map.prodₗ_apply
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₂]
[has_continuous_add N₃]
(ᾰ : (M →L[R] N₂) × (M →L[R] N₃)) :
def
continuous_linear_map.prodₗ
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₂ : Type u_9}
[topological_space N₂]
[add_comm_monoid N₂]
[module R N₂]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₂]
[has_continuous_const_smul S N₂]
[smul_comm_class R S N₂]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₂]
[has_continuous_add N₃] :
continuous_linear_map.prod as a linear_equiv.
Equations
- continuous_linear_map.prodₗ S = {to_fun := continuous_linear_map.prod_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.prod_equiv.inv_fun, left_inv := _, right_inv := _}
def
continuous_linear_map.coe_lm
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₃] :
The coercion from M →L[R] M₂ to M →ₗ[R] M₂, as a linear map.
Equations
- continuous_linear_map.coe_lm S = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_lm_apply
{R : Type u_1}
(S : Type u_4)
[semiring R]
[semiring S]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{N₃ : Type u_10}
[topological_space N₃]
[add_comm_monoid N₃]
[module R N₃]
[module S N₃]
[smul_comm_class R S N₃]
[has_continuous_const_smul S N₃]
[has_continuous_add N₃]
(ᾰ : M →L[R] N₃) :
⇑(continuous_linear_map.coe_lm S) ᾰ = ↑ᾰ
@[simp]
theorem
continuous_linear_map.coe_lmₛₗ_apply
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
(σ₁₃ : R →+* R₃)
[has_continuous_add M₃]
(ᾰ : M →SL[σ₁₃] M₃) :
⇑(continuous_linear_map.coe_lmₛₗ σ₁₃) ᾰ = ↑ᾰ
def
continuous_linear_map.coe_lmₛₗ
{R : Type u_1}
{R₃ : Type u_3}
{S₃ : Type u_5}
[semiring R]
[semiring R₃]
[semiring S₃]
{M : Type u_6}
[topological_space M]
[add_comm_monoid M]
[module R M]
{M₃ : Type u_8}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₃ M₃]
[module S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
[has_continuous_const_smul S₃ M₃]
(σ₁₃ : R →+* R₃)
[has_continuous_add M₃] :
The coercion from M →SL[σ] M₂ to M →ₛₗ[σ] M₂, as a linear map.
Equations
- continuous_linear_map.coe_lmₛₗ σ₁₃ = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
def
continuous_linear_map.smul_rightₗ
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring S]
[semiring T]
[module R S]
[add_comm_monoid M₂]
[module R M₂]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[topological_space M₂]
[has_continuous_smul S M₂]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_add M₂]
[module T M₂]
[has_continuous_const_smul T M₂]
[smul_comm_class R T M₂]
[smul_comm_class S T M₂]
(c : M →L[R] S) :
Given c : E →L[𝕜] 𝕜, c.smul_rightₗ is the linear map from F to E →L[𝕜] F
sending f to λ e, c e • f. See also continuous_linear_map.smul_rightL.
Equations
- c.smul_rightₗ = {to_fun := c.smul_right, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_smul_rightₗ
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
{M : Type u_4}
{M₂ : Type u_5}
[semiring R]
[semiring S]
[semiring T]
[module R S]
[add_comm_monoid M₂]
[module R M₂]
[module S M₂]
[is_scalar_tower R S M₂]
[topological_space S]
[topological_space M₂]
[has_continuous_smul S M₂]
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_add M₂]
[module T M₂]
[has_continuous_const_smul T M₂]
[smul_comm_class R T M₂]
[smul_comm_class S T M₂]
(c : M →L[R] S) :
⇑(c.smul_rightₗ) = c.smul_right
@[protected, instance]
def
continuous_linear_map.algebra
{R : Type u_1}
[comm_ring R]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M₂]
[has_continuous_const_smul R M₂] :
Equations
- continuous_linear_map.algebra = algebra.of_module continuous_linear_map.algebra._proof_5 continuous_linear_map.algebra._proof_6
def
continuous_linear_map.restrict_scalars
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
(R : Type u_4)
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
If A is an R-algebra, then a continuous A-linear map can be interpreted as a continuous
R-linear map. We assume linear_map.compatible_smul M M₂ R A to match assumptions of
linear_map.map_smul_of_tower.
Equations
- continuous_linear_map.restrict_scalars R f = {to_linear_map := linear_map.restrict_scalars R ↑f, cont := _}
@[simp, norm_cast]
theorem
continuous_linear_map.coe_restrict_scalars
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.coe_restrict_scalars'
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_zero
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A] :
@[simp]
theorem
continuous_linear_map.restrict_scalars_add
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
[topological_add_group M₂]
(f g : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_neg
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
[topological_add_group M₂]
(f : M →L[A] M₂) :
@[simp]
theorem
continuous_linear_map.restrict_scalars_smul
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
{S : Type u_5}
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
(c : S)
(f : M →L[A] M₂) :
def
continuous_linear_map.restrict_scalarsₗ
(A : Type u_1)
(M : Type u_2)
(M₂ : Type u_3)
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
(R : Type u_4)
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
(S : Type u_5)
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
[topological_add_group M₂] :
continuous_linear_map.restrict_scalars as a linear_map. See also
continuous_linear_map.restrict_scalarsL.
Equations
- continuous_linear_map.restrict_scalarsₗ A M M₂ R S = {to_fun := continuous_linear_map.restrict_scalars R _inst_11, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_linear_map.coe_restrict_scalarsₗ
{A : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring A]
[add_comm_group M]
[add_comm_group M₂]
[module A M]
[module A M₂]
[topological_space M]
[topological_space M₂]
{R : Type u_4}
[ring R]
[module R M]
[module R M₂]
[linear_map.compatible_smul M M₂ R A]
{S : Type u_5}
[ring S]
[module S M₂]
[has_continuous_const_smul S M₂]
[smul_comm_class A S M₂]
[smul_comm_class R S M₂]
[topological_add_group M₂] :
def
continuous_linear_equiv.to_continuous_linear_map
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
A continuous linear equivalence induces a continuous linear map.
Equations
- e.to_continuous_linear_map = {to_linear_map := {to_fun := e.to_linear_equiv.to_linear_map.to_fun, map_add' := _, map_smul' := _}, cont := _}
@[protected, instance]
def
continuous_linear_equiv.continuous_linear_map.has_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear equivs to continuous linear maps.
@[protected, instance]
def
continuous_linear_equiv.continuous_semilinear_equiv_class
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
continuous_semilinear_equiv_class (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂
Equations
- continuous_linear_equiv.continuous_semilinear_equiv_class = {coe := λ (f : M₁ ≃SL[σ₁₂] M₂), ⇑f, inv := λ (f : M₁ ≃SL[σ₁₂] M₂), f.to_linear_equiv.inv_fun, left_inv := _, right_inv := _, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _, inv_continuous := _}
@[protected, instance]
def
continuous_linear_equiv.has_coe_to_fun
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
Coerce continuous linear equivs to maps.
@[simp]
theorem
continuous_linear_equiv.coe_def_rev
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.coe_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁) :
@[simp]
theorem
continuous_linear_equiv.coe_to_linear_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f : M₁ ≃SL[σ₁₂] M₂) :
⇑(f.to_linear_equiv) = ⇑f
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
theorem
continuous_linear_equiv.to_linear_equiv_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[ext]
theorem
continuous_linear_equiv.ext
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{f g : M₁ ≃SL[σ₁₂] M₂}
(h : ⇑f = ⇑g) :
f = g
theorem
continuous_linear_equiv.coe_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂] :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_inj
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{e e' : M₁ ≃SL[σ₁₂] M₂} :
def
continuous_linear_equiv.to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
M₁ ≃ₜ M₂
A continuous linear equivalence induces a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := e.to_linear_equiv.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
⇑(e.to_homeomorph) = ⇑e
theorem
continuous_linear_equiv.image_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
theorem
continuous_linear_equiv.preimage_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[simp]
theorem
continuous_linear_equiv.is_closed_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁} :
theorem
continuous_linear_equiv.map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.map_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x y : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_smulₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_smul
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₁ M₂]
(e : M₁ ≃L[R₁] M₂)
(c : R₁)
(x : M₁) :
@[simp]
theorem
continuous_linear_equiv.map_eq_zero_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁} :
@[protected, continuity]
theorem
continuous_linear_equiv.continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_equiv.continuous_on
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁} :
continuous_on ⇑e s
@[protected]
theorem
continuous_linear_equiv.continuous_at
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁} :
continuous_at ⇑e x
@[protected]
theorem
continuous_linear_equiv.continuous_within_at
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : set M₁}
{x : M₁} :
continuous_within_at ⇑e s x
theorem
continuous_linear_equiv.comp_continuous_on_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{α : Type u_3}
[topological_space α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁}
{s : set α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
theorem
continuous_linear_equiv.comp_continuous_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
{α : Type u_3}
[topological_space α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁} :
continuous (⇑e ∘ f) ↔ continuous f
theorem
continuous_linear_equiv.ext₁
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[topological_space R₁]
{f g : R₁ ≃L[R₁] M₁}
(h : ⇑f 1 = ⇑g 1) :
f = g
An extensionality lemma for R ≃L[R] M.
@[protected, refl]
def
continuous_linear_equiv.refl
(R₁ : Type u_1)
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
The identity map as a continuous linear equivalence.
Equations
- continuous_linear_equiv.refl R₁ M₁ = {to_linear_equiv := {to_fun := (linear_equiv.refl R₁ M₁).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.refl R₁ M₁).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_refl
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
↑(continuous_linear_equiv.refl R₁ M₁) = continuous_linear_map.id R₁ M₁
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_refl'
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
⇑(continuous_linear_equiv.refl R₁ M₁) = id
@[protected, symm]
def
continuous_linear_equiv.symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
- e.symm = {to_linear_equiv := {to_fun := e.to_linear_equiv.symm.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_linear_equiv.symm.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.symm_to_linear_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_to_homeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
def
continuous_linear_equiv.simps.apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ ≃SL[σ₁₂] M₂) :
M₁ → M₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
continuous_linear_equiv.simps.symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(h : M₁ ≃SL[σ₁₂] M₂) :
M₂ → M₁
See Note [custom simps projection]
Equations
theorem
continuous_linear_equiv.symm_map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
@[protected, trans]
def
continuous_linear_equiv.trans
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃) :
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
- e₁.trans e₂ = {to_linear_equiv := {to_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.trans_to_linear_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃) :
(e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv
def
continuous_linear_equiv.prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄) :
Product of two continuous linear equivalences. The map comes from equiv.prod_congr.
Equations
- e.prod e' = {to_linear_equiv := {to_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).to_fun, map_add' := _, map_smul' := _, inv_fun := (e.to_linear_equiv.prod e'.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp, norm_cast]
theorem
continuous_linear_equiv.prod_apply
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
(x : M₁ × M₃) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.coe_prod
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄) :
theorem
continuous_linear_equiv.prod_symm
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₁ M₂]
[module R₁ M₃]
[module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄) :
@[protected]
theorem
continuous_linear_equiv.bijective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_equiv.injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[protected]
theorem
continuous_linear_equiv.surjective
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃)
(c : M₁) :
@[simp]
theorem
continuous_linear_equiv.apply_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_apply_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁) :
@[simp]
theorem
continuous_linear_equiv.symm_trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(e₁ : M₂ ≃SL[σ₂₁] M₁)
(e₂ : M₃ ≃SL[σ₃₂] M₂)
(c : M₁) :
@[simp]
theorem
continuous_linear_equiv.symm_image_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
@[simp]
theorem
continuous_linear_equiv.image_symm_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[simp, norm_cast]
theorem
continuous_linear_equiv.comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
(f : M₁ ≃SL[σ₁₂] M₂)
(f' : M₂ ≃SL[σ₂₃] M₃) :
@[simp]
theorem
continuous_linear_equiv.coe_comp_coe_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.coe_symm_comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_comp_self
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.self_comp_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.symm_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂) :
@[simp]
theorem
continuous_linear_equiv.refl_symm
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
(continuous_linear_equiv.refl R₁ M₁).symm = continuous_linear_equiv.refl R₁ M₁
theorem
continuous_linear_equiv.symm_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁) :
theorem
continuous_linear_equiv.symm_apply_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁} :
theorem
continuous_linear_equiv.eq_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁} :
@[protected]
theorem
continuous_linear_equiv.image_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
@[protected]
theorem
continuous_linear_equiv.image_symm_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[protected, simp]
theorem
continuous_linear_equiv.symm_preimage_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₂) :
@[protected, simp]
theorem
continuous_linear_equiv.preimage_symm_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : set M₁) :
@[protected]
theorem
continuous_linear_equiv.uniform_embedding
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{E₁ : Type u_3}
{E₂ : Type u_4}
[uniform_space E₁]
[uniform_space E₂]
[add_comm_group E₁]
[add_comm_group E₂]
[module R₁ E₁]
[module R₂ E₂]
[uniform_add_group E₁]
[uniform_add_group E₂]
(e : E₁ ≃SL[σ₁₂] E₂) :
@[protected]
theorem
linear_equiv.uniform_embedding
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{E₁ : Type u_3}
{E₂ : Type u_4}
[uniform_space E₁]
[uniform_space E₂]
[add_comm_group E₁]
[add_comm_group E₂]
[module R₁ E₁]
[module R₂ E₂]
[uniform_add_group E₁]
[uniform_add_group E₂]
(e : E₁ ≃ₛₗ[σ₁₂] E₂)
(h₁ : continuous ⇑e)
(h₂ : continuous ⇑(e.symm)) :
def
continuous_linear_equiv.equiv_of_inverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
Create a continuous_linear_equiv from two continuous_linear_maps that are
inverse of each other.
Equations
- continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂ = {to_linear_equiv := {to_fun := ⇑f₁, map_add' := _, map_smul' := _, inv_fun := ⇑f₂, left_inv := h₁, right_inv := h₂}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.equiv_of_inverse_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁)
(x : M₁) :
⇑(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂) x = ⇑f₁ x
@[simp]
theorem
continuous_linear_equiv.symm_equiv_of_inverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[semiring R₁]
[semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
[module R₁ M₁]
[module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : function.left_inverse ⇑f₂ ⇑f₁)
(h₂ : function.right_inverse ⇑f₂ ⇑f₁) :
(continuous_linear_equiv.equiv_of_inverse f₁ f₂ h₁ h₂).symm = continuous_linear_equiv.equiv_of_inverse f₂ f₁ h₂ h₁
@[protected, instance]
def
continuous_linear_equiv.automorphism_group
{R₁ : Type u_1}
[semiring R₁]
(M₁ : Type u_4)
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
The continuous linear equivalences from M to itself form a group under composition.
Equations
- continuous_linear_equiv.automorphism_group M₁ = {mul := λ (f g : M₁ ≃L[R₁] M₁), g.trans f, mul_assoc := _, one := continuous_linear_equiv.refl R₁ M₁ _inst_22, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _, npow_zero' := _, npow_succ' := _, inv := λ (f : M₁ ≃L[R₁] M₁), f.symm, div := div_inv_monoid.div._default (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ (continuous_linear_equiv.refl R₁ M₁) _ _ (div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _) _ _ (λ (f : M₁ ≃L[R₁] M₁), f.symm), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ (continuous_linear_equiv.refl R₁ M₁) _ _ (div_inv_monoid.npow._default (continuous_linear_equiv.refl R₁ M₁) (λ (f g : M₁ ≃L[R₁] M₁), g.trans f) _ _) _ _ (λ (f : M₁ ≃L[R₁] M₁), f.symm), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
def
continuous_linear_equiv.ulift
{R₁ : Type u_1}
[semiring R₁]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
[module R₁ M₁] :
The continuous linear equivalence between ulift M₁ and M₁.
Equations
- continuous_linear_equiv.ulift = {to_linear_equiv := {to_fun := equiv.ulift.to_fun, map_add' := _, map_smul' := _, inv_fun := equiv.ulift.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.arrow_congr_equiv_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₂ →SL[σ₂₃] M₃) :
def
continuous_linear_equiv.arrow_congr_equiv
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃) :
A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also continuous_linear_equiv.arrow_congr.
@[simp]
theorem
continuous_linear_equiv.arrow_congr_equiv_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[semiring R₁]
[semiring R₂]
[semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[topological_space M₁]
[add_comm_monoid M₁]
{M₂ : Type u_6}
[topological_space M₂]
[add_comm_monoid M₂]
{M₃ : Type u_7}
[topological_space M₃]
[add_comm_monoid M₃]
{M₄ : Type u_8}
[topological_space M₄]
[add_comm_monoid M₄]
[module R₁ M₁]
[module R₂ M₂]
[module R₃ M₃]
{R₄ : Type u_9}
[semiring R₄]
[module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄]
[ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₁ →SL[σ₁₄] M₄) :
def
continuous_linear_equiv.skew_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_group M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄) :
Equivalence given by a block lower diagonal matrix. e and e' are diagonal square blocks,
and f is a rectangular block below the diagonal.
Equations
- e.skew_prod e' f = {to_linear_equiv := {to_fun := (e.to_linear_equiv.skew_prod e'.to_linear_equiv ↑f).to_fun, map_add' := _, map_smul' := _, inv_fun := (e.to_linear_equiv.skew_prod e'.to_linear_equiv ↑f).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.skew_prod_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_group M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M × M₃) :
@[simp]
theorem
continuous_linear_equiv.skew_prod_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
{M₃ : Type u_4}
[topological_space M₃]
[add_comm_group M₃]
{M₄ : Type u_5}
[topological_space M₄]
[add_comm_group M₄]
[module R M]
[module R M₂]
[module R M₃]
[module R M₄]
[topological_add_group M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M₂ × M₄) :
@[simp]
theorem
continuous_linear_equiv.map_sub
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x y : M) :
@[simp]
theorem
continuous_linear_equiv.map_neg
{R : Type u_1}
[ring R]
{R₂ : Type u_2}
[ring R₂]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x : M) :
The next theorems cover the identification between M ≃L[𝕜] Mand the group of units of the ring
M →L[R] M.
def
continuous_linear_equiv.of_unit
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : (M →L[R] M)ˣ) :
An invertible continuous linear map f determines a continuous equivalence from M to itself.
Equations
- continuous_linear_equiv.of_unit f = {to_linear_equiv := {to_fun := ⇑(f.val), map_add' := _, map_smul' := _, inv_fun := ⇑(f.inv), left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
continuous_linear_equiv.to_unit
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : M ≃L[R] M) :
A continuous equivalence from M to itself determines an invertible continuous linear map.
def
continuous_linear_equiv.units_equiv
(R : Type u_1)
[ring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M] :
The units of the algebra of continuous R-linear endomorphisms of M is multiplicatively
equivalent to the type of continuous linear equivalences between M and itself.
Equations
- continuous_linear_equiv.units_equiv R M = {to_fun := continuous_linear_equiv.of_unit _inst_11, inv_fun := continuous_linear_equiv.to_unit _inst_11, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
continuous_linear_equiv.units_equiv_apply
(R : Type u_1)
[ring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
(f : (M →L[R] M)ˣ)
(x : M) :
⇑(⇑(continuous_linear_equiv.units_equiv R M) f) x = ⇑f x
def
continuous_linear_equiv.units_equiv_aut
(R : Type u_1)
[ring R]
[topological_space R]
[has_continuous_mul R] :
Continuous linear equivalences R ≃L[R] R are enumerated by Rˣ.
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(u : Rˣ)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_apply_symm
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(u : Rˣ)
(x : R) :
@[simp]
theorem
continuous_linear_equiv.units_equiv_aut_symm_apply
{R : Type u_1}
[ring R]
[topological_space R]
[has_continuous_mul R]
(e : R ≃L[R] R) :
def
continuous_linear_equiv.equiv_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
M ≃L[R] M₂ × ↥(linear_map.ker f₁)
A pair of continuous linear maps such that f₁ ∘ f₂ = id generates a continuous
linear equivalence e between M and M₂ × f₁.ker such that (e x).2 = x for x ∈ f₁.ker,
(e x).1 = f₁ x, and (e (f₂ y)).2 = 0. The map is given by e x = (f₁ x, x - f₂ (f₁ x)).
Equations
- continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h = continuous_linear_equiv.equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.coprod (linear_map.ker f₁).subtypeL) _ _
@[simp]
theorem
continuous_linear_equiv.fst_equiv_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
(⇑(continuous_linear_equiv.equiv_of_right_inverse f₁ f₂ h) x).fst = ⇑f₁ x
@[simp]
theorem
continuous_linear_equiv.snd_equiv_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(x : M) :
@[simp]
theorem
continuous_linear_equiv.equiv_of_right_inverse_symm_apply
{R : Type u_1}
[ring R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[module R M]
{M₂ : Type u_4}
[topological_space M₂]
[add_comm_group M₂]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁)
(y : M₂ × ↥(linear_map.ker f₁)) :
def
continuous_linear_equiv.fun_unique
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
If ι has a unique element, then ι → M is continuously linear equivalent to M.
Equations
- continuous_linear_equiv.fun_unique ι R M = {to_linear_equiv := linear_equiv.fun_unique ι R M _inst_4, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.coe_fun_unique
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
@[simp]
theorem
continuous_linear_equiv.coe_fun_unique_symm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[unique ι]
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
⇑((continuous_linear_equiv.fun_unique ι R M).symm) = function.const ι
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_apply
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
⇑(continuous_linear_equiv.pi_fin_two R M) = λ (f : Π (i : fin 2), M i), (f 0, f 1)
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_to_linear_equiv
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
@[simp]
theorem
continuous_linear_equiv.pi_fin_two_symm_apply
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
⇑((continuous_linear_equiv.pi_fin_two R M).symm) = λ (p : M 0 × M 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
def
continuous_linear_equiv.pi_fin_two
(R : Type u_2)
[semiring R]
(M : fin 2 → Type u_1)
[Π (i : fin 2), add_comm_monoid (M i)]
[Π (i : fin 2), module R (M i)]
[Π (i : fin 2), topological_space (M i)] :
Continuous linear equivalence between dependent functions Π i : fin 2, M i and M 0 × M 1.
Equations
- continuous_linear_equiv.pi_fin_two R M = {to_linear_equiv := linear_equiv.pi_fin_two R M (λ (i : fin 2), _inst_7 i), continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_to_linear_equiv
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_apply
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
⇑(continuous_linear_equiv.fin_two_arrow R M) = λ (f : fin 2 → M), (f 0, f 1)
@[simp]
theorem
continuous_linear_equiv.fin_two_arrow_symm_apply
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
def
continuous_linear_equiv.fin_two_arrow
(R : Type u_2)
(M : Type u_3)
[semiring R]
[add_comm_monoid M]
[module R M]
[topological_space M] :
Continuous linear equivalence between vectors in M² = fin 2 → M and M × M.
Equations
- continuous_linear_equiv.fin_two_arrow R M = {to_linear_equiv := linear_equiv.fin_two_arrow R M _inst_4, continuous_to_fun := _, continuous_inv_fun := _}
noncomputable
def
continuous_linear_map.inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M] :
Introduce a function inverse from M →L[R] M₂ to M₂ →L[R] M, which sends f to f.symm if
f is a continuous linear equivalence and to 0 otherwise. This definition is somewhat ad hoc,
but one needs a fully (rather than partially) defined inverse function for some purposes, including
for calculus.
@[simp]
theorem
continuous_linear_map.inverse_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M]
(e : M ≃L[R] M₂) :
By definition, if f is invertible then inverse f = f.symm.
@[simp]
theorem
continuous_linear_map.inverse_non_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M]
[module R M]
(f : M →L[R] M₂)
(h : ¬∃ (e' : M ≃L[R] M₂), ↑e' = f) :
By definition, if f is not invertible then inverse f = 0.
@[simp]
theorem
continuous_linear_map.ring_inverse_equiv
{R : Type u_1}
{M : Type u_2}
[topological_space M]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M]
(e : M ≃L[R] M) :
ring.inverse ↑e = ↑e.inverse
theorem
continuous_linear_map.to_ring_inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[topological_space M]
[topological_space M₂]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M]
[add_comm_group M₂]
[module R M₂]
(e : M ≃L[R] M₂)
(f : M →L[R] M₂) :
The function continuous_linear_equiv.inverse can be written in terms of ring.inverse for the
ring of self-maps of the domain.
theorem
continuous_linear_map.ring_inverse_eq_map_inverse
{R : Type u_1}
{M : Type u_2}
[topological_space M]
[ring R]
[add_comm_group M]
[topological_add_group M]
[module R M] :
def
submodule.closed_complemented
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Prop
A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.
theorem
submodule.closed_complemented.has_closed_complement
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
{p : submodule R M}
[t1_space ↥p]
(h : p.closed_complemented) :
@[protected]
theorem
submodule.closed_complemented.is_closed
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
[topological_add_group M]
[t1_space M]
{p : submodule R M}
(h : p.closed_complemented) :
@[simp]
theorem
submodule.closed_complemented_bot
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M] :
@[simp]
theorem
submodule.closed_complemented_top
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M] :
theorem
continuous_linear_map.closed_complemented_ker_of_right_inverse
{R : Type u_1}
[ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
{M₂ : Type u_3}
[topological_space M₂]
[add_comm_group M₂]
[module R M]
[module R M₂]
[topological_add_group M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : function.right_inverse ⇑f₂ ⇑f₁) :
theorem
submodule.is_open_map_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[topological_space M]
(S : submodule R M)
[topological_add_group M] :
is_open_map ⇑(S.mkq)
@[protected, instance]
def
submodule.topological_add_group_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[topological_space M]
(S : submodule R M)
[topological_add_group M] :
topological_add_group (M ⧸ S)
@[protected, instance]
def
submodule.has_continuous_smul_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[topological_space M]
(S : submodule R M)
[topological_space R]
[topological_add_group M]
[has_continuous_smul R M] :
has_continuous_smul R (M ⧸ S)
@[protected, instance]
def
submodule.t3_quotient_of_is_closed
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[topological_space M]
(S : submodule R M)
[topological_add_group M]
[is_closed ↑S] :