Theorems · Definition · category theory

TopModuleCat.toCoinduced

{R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {M : ModuleCat R} →
        {I : Type u_1} →
          {X : I → TopModuleCat R} → (f : (i : I) → (X i).toModuleCat ⟶ M) → (i : I) → X i ⟶ TopModuleCat.coinduced f

The maps into the coinduced topology as homs in TopModuleCat R.

Defined in: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Quiver.Homstatement and proof · cited by 32,603
TopologicalSpacestatement and proof · cited by 24,529
Ringstatement and proof · cited by 7,463
ModuleCatstatement and proof · cited by 1,429
ModuleCat.Hom.homproof · cited by 341
TopModuleCatstatement and proof · cited by 45
TopModuleCat.toModuleCatstatement and proof · cited by 29
TopModuleCat.ofHomproof · cited by 4
TopModuleCat.coinducedstatement · cited by 0

Cited by1

Results whose statement or proof uses this declaration.

TopModuleCat.ofCoconeproof · cited by 0