Theorems · Definition · global analysis

ContMDiff.smoothSheafCommRingHom

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          {I : ModelWithCorners 𝕜 E H} →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  {R : Type u} →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        {EP : Type u_7} →
                                          [inst_11 : NormedAddCommGroup EP] →
                                            [inst_12 : NormedSpace 𝕜 EP] →
                                              {HP : Type u_8} →
                                                [inst_13 : TopologicalSpace HP] →
                                                  (IP : ModelWithCorners 𝕜 EP HP) →
                                                    (P : Type u) →
                                                      [inst_14 : TopologicalSpace P] →
                                                        [inst_15 : ChartedSpace HP P] →
                                                          [inst_16 : CommRing R] →
                                                            [inst_17 : ContMDiffRing I (↑⊤) R] →
                                                              (f : M → P) →
                                                                (hf : ContMDiff IM IP (↑⊤) f) →
                                                                  smoothSheafCommRing IP I P R ⟶
                                                                    (TopCat.Sheaf.pushforward CommRingCat
                                                                          (TopCat.ofHom
                                                                            { toFun := f, continuous_toFun := ⋯ })).obj
                                                                      (smoothSheafCommRing IM I M R)

A smooth function f : M → N induces a morphism of sheaves (of rings) 𝒪_N ⟶ f_* 𝒪_M, by pre-composing with f.

Defined in

Mathlib.Geometry.Manifold.Sheaf.Smooth

Cited by

1 results in Mathlib

Foundations

Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceCommRingContMDiffRing