Mathlib Map

Theorems Β· Definition Β· algebraic topology

Bundle.Trivialization.continuousLinearMap

{π•œβ‚ : Type u_1} β†’
  [inst : NontriviallyNormedField π•œβ‚] β†’
    {π•œβ‚‚ : Type u_2} β†’
      [inst_1 : NontriviallyNormedField π•œβ‚‚] β†’
        (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) β†’
          {B : Type u_3} β†’
            {F₁ : Type u_4} β†’
              [inst_2 : NormedAddCommGroup F₁] β†’
                [inst_3 : NormedSpace π•œβ‚ F₁] β†’
                  {E₁ : B β†’ Type u_5} β†’
                    [inst_4 : (x : B) β†’ AddCommGroup (E₁ x)] β†’
                      [inst_5 : (x : B) β†’ Module π•œβ‚ (E₁ x)] β†’
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] β†’
                          {Fβ‚‚ : Type u_6} β†’
                            [inst_7 : NormedAddCommGroup Fβ‚‚] β†’
                              [inst_8 : NormedSpace π•œβ‚‚ Fβ‚‚] β†’
                                {Eβ‚‚ : B β†’ Type u_7} β†’
                                  [inst_9 : (x : B) β†’ AddCommGroup (Eβ‚‚ x)] β†’
                                    [inst_10 : (x : B) β†’ Module π•œβ‚‚ (Eβ‚‚ x)] β†’
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace Fβ‚‚ Eβ‚‚)] β†’
                                        [inst_12 : TopologicalSpace B] β†’
                                          (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) β†’
                                            (eβ‚‚ : Bundle.Trivialization Fβ‚‚ Bundle.TotalSpace.proj) β†’
                                              [inst_13 : (x : B) β†’ TopologicalSpace (E₁ x)] β†’
                                                [inst_14 : FiberBundle F₁ E₁] β†’
                                                  [inst_15 : VectorBundle π•œβ‚ F₁ E₁] β†’
                                                    [inst_16 : (x : B) β†’ TopologicalSpace (Eβ‚‚ x)] β†’
                                                      [inst_17 : FiberBundle Fβ‚‚ Eβ‚‚] β†’
                                                        [inst_18 : VectorBundle π•œβ‚‚ Fβ‚‚ Eβ‚‚] β†’
                                                          [inst_19 : βˆ€ (x : B), IsTopologicalAddGroup (Eβ‚‚ x)] β†’
                                                            [inst_20 : βˆ€ (x : B), ContinuousSMul π•œβ‚‚ (Eβ‚‚ x)] β†’
                                                              [inst_21 : RingHomIsometric Οƒ] β†’
                                                                [he₁ : MemTrivializationAtlas e₁] β†’
                                                                  [heβ‚‚ : MemTrivializationAtlas eβ‚‚] β†’
                                                                    Bundle.Trivialization (F₁ β†’SL[Οƒ] Fβ‚‚)
                                                                      Bundle.TotalSpace.proj

Given trivializations e₁, eβ‚‚ in the atlas for vector bundles E₁, Eβ‚‚ over a base B, the induced trivialization for the continuous Οƒ-semilinear maps from E₁ to Eβ‚‚, whose base set is e₁.baseSet ∩ eβ‚‚.baseSet.

Defined in
Mathlib.Topology.VectorBundle.Hom
Cited by
5 results in Mathlib
Foundations
Depth 183 from the axioms Β· uses propext, Classical.choice, Quot.sound
Assumes
NontriviallyNormedFieldNontriviallyNormedFieldNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceNormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundleTopologicalSpaceFiberBundleVectorBundleIsTopologicalAddGroupContinuousSMulRingHomIsometricMemTrivializationAtlasMemTrivializationAtlas
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

inCoordinates_apply_eqβ‚‚ Β· cited by 2inCoordinates_apply_eqβ‚‚Bundle.Trivialization.continuousLinearMap.congr_simp Β· cited by 0continuousLinearMap.congr…Bundle.Trivialization.baseSet_continuousLinearMap Β· cited by 0Trivialization.baseSet_co…Bundle.Trivialization.continuousLinearMap_apply Β· cited by 0Trivialization.continuous…hom_trivializationAt Β· cited by 0hom_trivializationAtTopologicalSpace Β· cited by 24529TopologicalSpaceModule Β· cited by 20661ModuleNormedAddCommGroup Β· cited by 15752NormedAddCommGroupAddCommGroup Β· cited by 12871AddCommGroupNormedSpace Β· cited by 12499NormedSpaceRingHom Β· cited by 10189RingHomNontriviallyNormedField Β· cited by 8742NontriviallyNormedFieldContinuousLinearMap Β· cited by 5352ContinuousLinearMapIsTopologicalAddGroup Β· cited by 1394IsTopologicalAddGroupContinuousSMul Β· cited by 1016ContinuousSMulBundle.TotalSpace Β· cited by 766Bundle.TotalSpaceFiberBundle Β· cited by 471FiberBundleBundle.TotalSpace.proj Β· cited by 447TotalSpace.projBundle.Trivialization Β· cited by 324Bundle.TrivializationVectorBundle Β· cited by 315VectorBundleTrivialization.continuousLine…CITED BYCITES

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.