Documentation

TauCeti.Topology.Category.TopPair.ContinuousLinearEquiv

The pair of a topological module and its nonzero vectors #

A continuous linear equivalence f : E ≃L[R] F carries the nonzero vectors of E onto those of F, so it induces an isomorphism of pairs (E, E ∖ {0}) ≅ (F, F ∖ {0}) (ContinuousLinearEquiv.complZeroPairIso). These pairs compute local homology and cohomology at the origin, and they are the fibres of the Thom pair of a vector bundle.

Main definitions #

source
theorem ContinuousLinearEquiv.mapsTo_compl_zero {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) :
Set.MapsTo ⇑f {0}ᶜ {0}ᶜ

A continuous linear equivalence sends nonzero vectors to nonzero vectors.

source
def ContinuousLinearEquiv.complZeroPairIso {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) :
TopPair.ofSubset {0}ᶜ ≅ TopPair.ofSubset {0}ᶜ

The isomorphism of pairs (E, E ∖ {0}) ≅ (F, F ∖ {0}) induced by a continuous linear equivalence f : E ≃L[R] F.

Instances For
    source
    @[simp]
    theorem ContinuousLinearEquiv.complZeroPairIso_hom_fst_apply {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) (x : E) :
    (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst f.complZeroPairIso.hom)) x = f x
    source
    @[simp]
    theorem ContinuousLinearEquiv.complZeroPairIso_inv_fst_apply {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) (y : F) :
    (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst f.complZeroPairIso.inv)) y = f.symm y
    source
    theorem ContinuousLinearEquiv.complZeroPairIso_hom {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) :
    f.complZeroPairIso.hom = TopPair.ofSubsetMap (TopCat.ofHom ↑↑f) ⋯

    The map of pairs underlying ContinuousLinearEquiv.complZeroPairIso f is the map induced by f as a continuous linear map.

    source
    theorem ContinuousLinearEquiv.complZeroPairIso_inv {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) :
    f.complZeroPairIso.inv = TopPair.ofSubsetMap (TopCat.ofHom ↑↑f.symm) ⋯

    The inverse map of pairs underlying ContinuousLinearEquiv.complZeroPairIso f is the map induced by f.symm as a continuous linear map.

    source
    @[simp]
    theorem ContinuousLinearEquiv.complZeroPairIso_refl {R : Type u_1} [Semiring R] {E : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] :
    (ContinuousLinearEquiv.refl R E).complZeroPairIso = CategoryTheory.Iso.refl (TopPair.ofSubset {0}ᶜ)

    The pair isomorphism of the identity is the identity.

    source
    @[simp]
    theorem ContinuousLinearEquiv.complZeroPairIso_trans {R : Type u_1} [Semiring R] {E F G : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] (f : E ≃L[R] F) (g : F ≃L[R] G) :
    (f.trans g).complZeroPairIso = f.complZeroPairIso ≪≫ g.complZeroPairIso

    The pair isomorphism of a composite is the composite of the pair isomorphisms.

    source
    @[simp]
    theorem ContinuousLinearEquiv.complZeroPairIso_symm {R : Type u_1} [Semiring R] {E F : Type w} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) :
    f.symm.complZeroPairIso = f.complZeroPairIso.symm

    The pair isomorphism of the inverse is the inverse of the pair isomorphism.