110.79 The category of modules… to 110.82 The spectrum of the…
Section110.79 The category of modules modulo torsion modules#
Section 110.79 of the Stacks Project, Tag 0B0J. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EA5, a proposition
Tag 0EA5 in the Stacks Project.
Stacks.Examples.localizationTorsionModuleProperty_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ModulesModuloTorsion.lean, line 64. The attribute's comment: “the Serre subcategory”.
The modules whose elements are annihilated locally by
Sform a Serre subcategory.
public instance localizationTorsionModuleProperty_isSerreClass {R : Type u} [CommRing R]
(S : Submonoid R) :
(localizationTorsionModuleProperty (R := R) S :
ObjectProperty (ModuleCat.{v} R)).IsSerreClass
Stacks.Examples.localizedModuleFunctor_isLocalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ModulesModuloTorsion.lean, line 226. The attribute's comment: “the canonical equivalence”.
Localizing modules at
Spresents the category of modules overLocalization Sas the Serre quotient by the modules whose elements are annihilated by members ofS.In particular,
CategoryTheory.Localization.equivalenceFromModelapplied to this instance is the canonical equivalence from the Serre quotient toModuleCat (Localization S), andCategoryTheory.Localization.qCompEquivalenceFromModelFunctorIsoidentifies its composite with the quotient functor withModuleCat.localizedModuleFunctor S.
public instance localizedModuleFunctor_isLocalization {R : Type u} [CommRing R]
(S : Submonoid R) [Small.{v, u} R] :
(ModuleCat.localizedModuleFunctor.{v} S).IsLocalization
(localizationTorsionModuleProperty (R := R) S :
ObjectProperty (ModuleCat.{v} R)).isoModSerre
Tag 0B0K, a proposition
Tag 0B0K in the Stacks Project.
Stacks.Examples.localizedModuleFunctor_isLocalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ModulesModuloTorsion.lean, line 226. The attribute's comment: “the case S = nonzerodivisors: Mod_A modulo torsion is equivalent to Mod_{Q(A)}”.
Localizing modules at
Spresents the category of modules overLocalization Sas the Serre quotient by the modules whose elements are annihilated by members ofS.In particular,
CategoryTheory.Localization.equivalenceFromModelapplied to this instance is the canonical equivalence from the Serre quotient toModuleCat (Localization S), andCategoryTheory.Localization.qCompEquivalenceFromModelFunctorIsoidentifies its composite with the quotient functor withModuleCat.localizedModuleFunctor S.
public instance localizedModuleFunctor_isLocalization {R : Type u} [CommRing R]
(S : Submonoid R) [Small.{v, u} R] :
(ModuleCat.localizedModuleFunctor.{v} S).IsLocalization
(localizationTorsionModuleProperty (R := R) S :
ObjectProperty (ModuleCat.{v} R)).isoModSerre
Tag 0B0L, a proposition
Tag 0B0L in the Stacks Project.
Stacks.Examples.fgTorsionModuleProperty_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FGModulesModuloTorsion.lean, line 89. The attribute's comment: “the Serre subcategory”.
Finitely generated torsion modules form a Serre subcategory.
public instance fgTorsionModuleProperty_isSerreClass (A : Type u) [CommRing A]
[IsNoetherianRing A] :
(fgTorsionModuleProperty A : ObjectProperty (FGModuleCat.{v} A)).IsSerreClass
Stacks.Examples.fgFractionModuleFunctor_isLocalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FGModulesModuloTorsion.lean, line 195. The attribute's comment: “the canonical equivalence”.
Localizing finitely generated modules at the nonzerodivisors presents the category of finite-dimensional fraction-field vector spaces as their Serre quotient by the torsion modules.
public instance fgFractionModuleFunctor_isLocalization (A : Type u) [CommRing A]
[IsDomain A] [IsNoetherianRing A] [Small.{v, u} A] :
(fgFractionModuleFunctor A : FGModuleCat.{v} A ⥤
FGModuleCat.{v} (FractionRing A)).IsLocalization
(fgTorsionModuleProperty A : ObjectProperty (FGModuleCat.{v} A)).isoModSerre
Tag 0B0M, a proposition
Tag 0B0M in the Stacks Project.
Stacks.Examples.extendScalarsRat_isLocalization, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/AbelianGroupsModuloTorsion.lean, line 95.
Rationalization presents rational vector spaces as the Serre quotient of abelian groups by torsion groups.
public instance extendScalarsRat_isLocalization :
(ModuleCat.extendScalars (algebraMap ℤ ℚ) :
ModuleCat.{v} ℤ ⥤ ModuleCat.{v} ℚ).IsLocalization
(localizationTorsionModuleProperty (R := ℤ)
(nonZeroDivisors ℤ) : ObjectProperty (ModuleCat.{v} ℤ)).isoModSerre
Sources
Section110.80 Different colimit topologies#
Section 110.80 of the Stacks Project, Tag 0B2Y. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0B2Z, a lemma
Tag 0B2Z in the Stacks Project.
Stacks.Examples.exists_sequential_colimit_not_preserved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ColimitTopologies.lean, line 450.
A sequential diagram of abelian topological groups for which the colimit topology as spaces differs from the colimit topology as groups.
public theorem exists_sequential_colimit_not_preserved :
∃ F : ℕ ⥤ TopGrp.{u},
(∀ n : ℕ, ∀ x y : F.obj n, x * y = y * x) ∧
¬ PreservesColimit F TopGrp.forgetToTopCat
Sources
Section110.81 Universally submersive but not V covering#
Section 110.81 of the Stacks Project, Tag 0EU8. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EU9, a lemma
Tag 0EU9 in the Stacks Project.
Stacks.Examples.exists_universallySubmersive_not_isVCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/UniversallySubmersiveNotVCovering.lean, line 775.
An affine, universally submersive morphism whose singleton family is not a V covering.
public theorem exists_universallySubmersive_not_isVCovering :
∃ (X Y : Scheme.{u}) (_ : IsAffine X) (_ : IsAffine Y) (f : X ⟶ Y),
(topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally f ∧
¬ AlgebraicGeometry.IsVCovering (fun _ : Unit => X) (fun _ => f)
Sources
Section110.82 The spectrum of the integers is not quasi-compact#
Section 110.82 of the Stacks Project, Tag 0EUE. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EUF, a lemma
Tag 0EUF in the Stacks Project.
Stacks.Examples.exists_infinite_flat_family_moduleDescentEqualizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/NonFpqcDescent.lean, line 557.
An infinite family of flat algebra maps satisfies module descent, but no finite subfamily satisfies it.
public theorem exists_infinite_flat_family_moduleDescentEqualizer :
∃ (A : CommRingCat.{u}) (I : Type v) (_ : Infinite I)
(B : I → CommAlgCat.{u} A),
(∀ i, Module.Flat A (B i)) ∧
IsModuleDescentEqualizer A B Set.univ ∧
(∀ J : Set I, J.Finite → ¬ IsModuleDescentEqualizer A B J)
Tag 0EUG, a lemma
Tag 0EUG in the Stacks Project.
Stacks.AlgebraicGeometry.SpecIntQuasiCompactCounterexample.specInt_not_isQuasiCompactObject_canonicalTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SpecIntQuasiCompactCounterexample.lean, line 982.
The spectrum of the integers is not quasi-compact in the canonical topology on the category of schemes.
public theorem specInt_not_isQuasiCompactObject_canonicalTopology :
¬(Sheaf.canonicalTopology Scheme.{0}).IsQuasiCompactObject
(Spec (CommRingCat.of ℤ))
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.