10.4 Snake lemma to 10.23 Glueing properties

Section10.4 Snake lemma#

Section 10.4 of the Stacks Project, Tag 07JV. 1 tag here is carried by 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07JW, a lemma

Tag 07JW in the Stacks Project.

Declarations registered for the tag:

Sources
LeanCategoryTheory.ShortComplex.SnakeInput.snake_lemma

Section10.5 Finite modules and finitely presented modules#

Section 10.5 of the Stacks Project, Tag 0517. 5 tags here are carried by 5 declarations of the repository (all in StacksCore) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0518, a definition

Tag 0518 in the Stacks Project.

Declarations registered for the tag:

  • Module.FinitePresentation registered with add_to_stacks in StacksCore/Algebra/Module/FinitePresentation.lean, line 10 (StacksCore): “part 2”. References: EGA 0 (1.0.5); EGA IV (2.5.3); SGA 4 VI (5.6), “special case”; SGA 5 IIIB (5.10); SGA 6 I (2.8), “special case”.
  • Module.Finite registered with add_to_stacks in StacksCore/RingTheory/Finiteness/Defs.lean, line 14 (StacksCore): “part 1”. References: EGA 0 (10.3.1.2); EGA 0 (1.0.5); EGA II (6.3.1); EGA III (4.4.7); EGA III (7.4.6); EGA III (7.9.1); EGA IV (6.1.3); EGA IV (7.2.4); EGA IV (14.5.5); EGA IV (2.5.3); EGA IV (18.3.2.1); SGA 1 I (2.1); SGA 3 VIII (3.4); SGA 3 XXI (1.1.1), “partial”; SGA 4 VI (5.6), “special case”; SGA 4 XVII (5.5.6.3); SGA 4½ Rapport (4.11); SGA 5 X (3.1), “partial”; SGA 6 I (1.2), “special case”; SGA 6 I (1.3), “special case”; SGA 6 I (2.8), “special case”; SGA 6 II (2.2.10).
Tag 07JX, a lemma

Tag 07JX in the Stacks Project.

Module.projective_iff_lift_map_range_le, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/Projective.lean, line 17. References: SGA 5 XV (3.Lemma3), “more general”; SGA 6 I (1.3), “more general”.

This is a generalisation of 07JX to an characterization of projective modules, the forward direction is exactly what 07JX states.

theorem Module.projective_iff_lift_map_range_le
    {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P] [Small.{v} R] :
    Module.Projective R P ↔ ∀ {M N : Type v} [AddCommMonoid M] [AddCommMonoid N] [Module R M]
      [Module R N] (α : P →ₗ[R] M) (β : N →ₗ[R] M), LinearMap.range α ≤ LinearMap.range β →
      ∃ γ : P →ₗ[R] N, α = β.comp γ
Tag 0519, a lemma

Tag 0519 in the Stacks Project.

Module.FinitePresentation.of_exact_fst, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/FinitePresentation.lean, line 26. The attribute's comment: “2”.

lemma Module.FinitePresentation.of_exact_fst [Module.FinitePresentation R M1]
    [Module.FinitePresentation R M3] :
    Module.FinitePresentation R M2

Module.FinitePresentation.of_exact_third, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/FinitePresentation.lean, line 34. The attribute's comment: “4”. References: EGA 0 (1.0.5), “partial”.

lemma Module.FinitePresentation.of_exact_third [Module.Finite R M1]
    [Module.FinitePresentation R M2] :
    Module.FinitePresentation R M3

Module.Finite.of_exact_left, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/FinitePresentation.lean, line 43. The attribute's comment: “5”.

lemma Module.Finite.of_exact_left [Module.Finite R M2]
    [Module.FinitePresentation R M3] :
    Module.Finite R M1
Tag 00KZ, a lemma

Tag 00KZ in the Stacks Project.

Module.Finite.exists_relSeries_isQuotientEquivQuotientCyclic, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Ideal/AssociatedPrime/Finiteness.lean, line 78.

Stacks 00KZ. Let R be a ring and M a finite R-module. Then M admits a finite filtration 0 = M₀ ≤ M₁ ≤ ⋯ ≤ Mₙ = M, packaged as a RelSeries of Submodule.IsQuotientEquivQuotientCyclic, whose terms are finitely generated and whose successive quotients Mᵢ₊₁ ⧸ Mᵢ are cyclic, i.e. each isomorphic to R ⧸ Iᵢ for some ideal Iᵢ.

The quotients are cyclic but not necessarily simple, so this is a filtration rather than a composition series in the sense of CompositionSeries (which requires simple quotients, hence finite length).

theorem Module.Finite.exists_relSeries_isQuotientEquivQuotientCyclic (R M : Type*) [Ring R]
    [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ X : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientCyclic N₂},
      X.head = (⊥ : Submodule R M) ∧ X.last = ⊤ ∧ ∀ i, Module.Finite R (X i)
Tag 0560, a lemma

Tag 0560 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.FinitePresentation · Module.Finite · Module.projective_iff_lift_map_range_le · Module.FinitePresentation.of_exact_fst · Module.FinitePresentation.of_exact_third · Module.Finite.of_exact_left · Module.Finite.exists_relSeries_isQuotientEquivQuotientCyclic · Module.Finite.of_restrictScalars_finite

Section10.6 Ring maps of finite type and of finite presentation#

Section 10.6 of the Stacks Project, Tag 00F2. 4 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00F3, a definition

Tag 00F3 in the Stacks Project.

Declarations registered for the tag:

Tag 00F4, a lemma

Tag 00F4 in the Stacks Project.

Declarations registered for the tag:

Tag 00R2, a lemma

Tag 00R2 in the Stacks Project.

Declarations registered for the tag:

Tag 0561, a lemma

Tag 0561 in the Stacks Project.

Module.FinitePresentation.of_restrictScalars_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/BlowupFiniteTypeReduction.lean, line 238. The attribute's comment: “the module statement, not the analogue for algebras”.

Stacks 0561. Let R → S be a ring map of finite type and let M be an S-module which is finitely presented as an R-module. Then M is finitely presented as an S-module.

Mathlib's Module.FinitePresentation.trans is the converse implication: it deduces finite presentation over R from finite presentation over S together with finite presentation of S over R. Mathlib's own declaration carrying the tag 0561, Algebra.FinitePresentation.of_restrict_scalars_finitePresentation, is not this lemma but the analogue for algebras in place of modules.

theorem Module.FinitePresentation.of_restrictScalars_of_finiteType (R S M : Type*) [CommRing R]
    [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M]
    [Algebra.FiniteType R S] [Module.FinitePresentation R M] : Module.FinitePresentation S M
Sources
LeanRingHom.FinitePresentation · RingHom.FiniteType · RingHom.FinitePresentation.comp · RingHom.FinitePresentation.of_comp_finiteType · RingHom.FiniteType.comp · RingHom.FiniteType.of_comp_finiteType · Algebra.FinitePresentation.ker_fg_of_mvPolynomial · Module.FinitePresentation.of_restrictScalars_of_finiteType

Section10.7 Finite ring maps#

Section 10.7 of the Stacks Project, Tag 0562. 3 tags here are carried by 1 declaration of the repository (in StacksCore) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00GJ, a lemma

Tag 00GJ in the Stacks Project.

Module.Finite.iff_scalarTower, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Finiteness/Basic.lean, line 15.

theorem Module.Finite.iff_scalarTower {R S M : Type*} [Semiring R] [Semiring S] [AddCommMonoid M]
    [Module R S] [Module R M] [Module S M] [Module.Finite R S] [IsScalarTower R S M] :
    Module.Finite R M ↔ Module.Finite S M
Tag 00GL, a lemma

Tag 00GL in the Stacks Project.

Declarations registered for the tag:

Tag 0D46, a lemma

Tag 0D46 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.Finite.iff_scalarTower · RingHom.Finite.comp · Module.FinitePresentation.of_finite_of_finitePresentation · RingHom.FiniteType.of_finite

Section10.8 Colimits#

Section 10.8 of the Stacks Project, Tag 07N7. 10 tags here are carried by 6 declarations of the repository (2 in StacksCore and 4 in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00D4, a definition

Tag 00D4 in the Stacks Project.

Declarations registered for the tag:

Tag 00D5, a lemma

Tag 00D5 in the Stacks Project.

Declarations registered for the tag:

Tag 00D6, a lemma

Tag 00D6 in the Stacks Project.

Declarations registered for the tag:

Tag 00D7, a lemma

Tag 00D7 in the Stacks Project.

Declarations registered for the tag:

Tag 00D8, an example

Tag 00D8 in the Stacks Project.

ModuleCat.ker_hom_comp_inl_and_ker_hom_inl_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Colimits.lean, line 112. The attribute's comment: “The poset {a < b, a < c} is the span shape, so the colimit of a system over it is a pushout in ModuleCat R, taken here abstractly rather than through the model Coker(μ_ab ⊕ -μ_ac); that the pushout is that cokernel is Mathlib's CategoryTheory.IsPushout.isColimitCokernelCofork. The mirror Ker(inr) = μ_ac(Ker(μ_ab)) is this statement applied to h.flip.”.

Let R be a ring and let M = colim M_i be the colimit of a system of R-modules over the poset {a < b, a < c}, that is, the pushout of a span M_b ← M_a → M_c of R-modules, with canonical maps inl : M_b → M and inr : M_c → M. Then the kernel of the canonical map M_a → M is Ker(μ_ab) + Ker(μ_ac), and the kernel of inl is the image of Ker(μ_ac) under μ_ab.

theorem ModuleCat.ker_hom_comp_inl_and_ker_hom_inl_of_isPushout {R : Type u} [Ring R]
    {Ma Mb Mc M : ModuleCat.{v} R} {μab : Ma ⟶ Mb} {μac : Ma ⟶ Mc} {inl : Mb ⟶ M} {inr : Mc ⟶ M}
    (h : IsPushout μab μac inl inr) :
    LinearMap.ker (μab ≫ inl).hom = LinearMap.ker μab.hom ⊔ LinearMap.ker μac.hom ∧
      LinearMap.ker inl.hom = Submodule.map μab.hom (LinearMap.ker μac.hom)
Tag 00D9, a definition

Tag 00D9 in the Stacks Project.

Module.IsSystemHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Defs/Colimits.lean, line 75. The attribute's comment: “Stated as a Prop-valued predicate on the family φ, in the unbundled language of Module.DirectLimit, so that Module.DirectLimit.map φ h is the induced map on colimits of Lemma 00DA. The axioms of a system (DirectedSystem) are not assumed, the commuting squares not referring to them, and R is only a semiring acting on additive commutative monoids.”.

Stacks 00D9. Let (M i, μ i j) and (N i, ν i j) be systems of R-modules over the same preordered set ι. A family of R-linear maps φ i : M i →ₗ[R] N i is a homomorphism of systems from (M, μ) to (N, ν) when every transition square commutes, that is, when φ j ∘ₗ μ i j = ν i j ∘ₗ φ i for all i ≤ j; equivalently, when φ is a natural transformation between the associated diagrams ι ⥤ ModuleCat R. The axioms making μ and ν systems are not needed to state the condition and are not assumed.

def IsSystemHom {R : Type*} [Semiring R] {ι : Type*} [Preorder ι]
    {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
    (μ : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
    {N : ι → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
    (ν : (i j : ι) → i ≤ j → N i →ₗ[R] N j)
    (φ : (i : ι) → M i →ₗ[R] N i) : Prop

Declarations registered for the tag:

Tag 00DA, a lemma

Tag 00DA in the Stacks Project.

Declarations registered for the tag:

Tag 00DB, a lemma

Tag 00DB in the Stacks Project.

Module.DirectLimit.comp_eq_zero, a lemma in StacksCore (human-reviewed), declared in StacksCore/Algebra/Colimit/Module.lean, line 28. The attribute's comment: “part 1”.

public lemma Module.DirectLimit.comp_eq_zero :
    Module.DirectLimit.map g' hg' ∘ₗ Module.DirectLimit.map g hg = 0

Module.DirectLimit.homologyColimitEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Colimit/Module.lean, line 127. The attribute's comment: “part 2”.

Homology intertwines with direct limits.

public def Module.DirectLimit.homologyColimitEquiv
    [Nonempty ι] [IsDirectedOrder ι]
    [DirectedSystem M fun i j h ↦ ⇑(f' i j h)]
    [DirectedSystem N fun x1 x2 x3 ↦ ⇑(l x1 x2 x3)] :
    Module.DirectLimit (hObj g g') (hMap g hg g' hg') ≃ₗ[R] homologyLimit g hg g' hg'
Tag 00DC, an example

Tag 00DC in the Stacks Project.

ModuleCat.not_injective_hom_of_isColimit_binaryCofan_of_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Colimits.lean, line 149. The attribute's comment: “The poset {a < b, a < c} is the span shape, so the colimit of a system over it is a pushout in ModuleCat R and the colimit of the sub-system with apex the zero module is the coproduct B ⊔ C; the morphism of systems (0 → A, 𝟙 B, 𝟙 C) is injective on each object, and ψ is pinned by the two commuting squares of Stacks 00DA. Stated for an arbitrary nonzero span over an arbitrary ring instead of the source's (0, ℤ, ℤ, 0, 0) → (ℤ, ℤ, ℤ, 1, 1).”.

Taking colimits is not exact in general: let R be a ring, let M be the colimit of a system (A, B, C, μ_ab, μ_ac) of R-modules over the poset {a < b, a < c}, that is, the pushout of the span B ← A → C, and let L be the colimit B ⊔ C of the sub-system (0, B, C, 0, 0). If one of μ_ab, μ_ac is nonzero, then the induced map of colimits ψ : L → M is not injective, even though the morphism of systems (0 → A, 𝟙 B, 𝟙 C) is injective on each object.

theorem ModuleCat.not_injective_hom_of_isColimit_binaryCofan_of_isPushout {R : Type u}
    [Ring R] {A B C L M : ModuleCat.{v} R} {μab : A ⟶ B} {μac : A ⟶ C} {l : B ⟶ L} {r : C ⟶ L}
    {inl : B ⟶ M} {inr : C ⟶ M} {ψ : L ⟶ M} (hL : IsColimit (BinaryCofan.mk l r))
    (hM : IsPushout μab μac inl inr) (hl : l ≫ ψ = inl) (hr : r ≫ ψ = inr)
    (hμ : μab ≠ 0 ∨ μac ≠ 0) :
    ¬ Function.Injective ψ.hom
Tag 04B0, a lemma

Tag 04B0 in the Stacks Project.

CategoryTheory.hasExactColimitsOfShape_of_isPseudofiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/AssociatedPrime/Colimits.lean, line 290. The attribute's comment: “Stated as HasExactColimitsOfShape J C, i.e. colim : (J ⥤ C) ⥤ C preserves finite limits, which for a left adjoint is exactness and is the form of Stacks 00DB the source asks for. The assumptions of Stacks 002X are spelled out because Mathlib has no predicate for a pseudofiltered category. Stated for an arbitrary abelian category with colimits of size w whose filtered colimits are exact, instead of the source's abelian groups, since the source's proof uses only that; AB4 is derived from AB5 rather than assumed.”.

Let J be an index category satisfying the assumptions of Stacks 002X: every span y ← x → z is completed by some commutative square, and every pair of parallel morphisms a b : x ⟶ y is coequalized by some c : y ⟶ z. Then taking colimits of diagrams over J in an abelian category with exact filtered colimits is exact.

theorem CategoryTheory.hasExactColimitsOfShape_of_isPseudofiltered {C : Type u}
    [Category.{v} C] [Abelian C] [Limits.HasColimitsOfSize.{w, w} C] [AB5OfSize.{w, w} C]
    {J : Type w} [Category.{w} J]
    (hspan : ∀ ⦃x y z : J⦄ (a : x ⟶ y) (b : x ⟶ z), ∃ (t : J) (c : y ⟶ t) (d : z ⟶ t),
      a ≫ c = b ≫ d)
    (hpar : ∀ ⦃x y : J⦄ (a b : x ⟶ y), ∃ (z : J) (c : y ⟶ z), a ≫ c = b ≫ c) :
    HasExactColimitsOfShape J C

Declarations registered for the tag:

Sources
LeanDirectedSystem · Module.DirectLimit · DirectLimit.Module.of · DirectLimit.Module.lift · ModuleCat.directLimitIsColimit · DirectLimit.exists_eq_zero · ModuleCat.ker_hom_comp_inl_and_ker_hom_inl_of_isPushout · Module.IsSystemHom

Section10.9 Localization#

Section 10.9 of the Stacks Project, Tag 00CM. 16 tags here are carried by 6 declarations of the repository (all in StacksCore) and 16 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00CN, a definition

Tag 00CN in the Stacks Project.

Declarations registered for the tag:

Tag 00CO, a definition

Tag 00CO in the Stacks Project.

Declarations registered for the tag:

Tag 00CP, a proposition

Tag 00CP in the Stacks Project.

Declarations registered for the tag:

Tag 00CQ, a lemma

Tag 00CQ in the Stacks Project.

Declarations registered for the tag:

Tag 07JY, a lemma

Tag 07JY in the Stacks Project.

ModuleCat.invertibleSMulEquivalentLocalizationModuleCat, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Category/ModuleCat/Localization.lean, line 283.

Stacks 07JY. The category of Localization S-modules is equivalent to the full subcategory of R-modules on which every s ∈ S acts invertibly. The functor is ModuleCat.localizedModuleFunctor restricted to the subcategory; the quasi-inverse is restriction of scalars along algebraMap R (Localization S).

noncomputable def invertibleSMulEquivalentLocalizationModuleCat [Small.{v, u} R] :
    (invertibleSMul S).FullSubcategory ≌ ModuleCat.{v} (Localization S)
Tag 07JZ, a definition

Tag 07JZ in the Stacks Project.

Declarations registered for the tag:

Tag 07K0, a lemma

Tag 07K0 in the Stacks Project.

Declarations registered for the tag:

Tag 02C5, an example

Tag 02C5 in the Stacks Project.

Declarations registered for the tag:

Tag 00CR, a lemma

Tag 00CR in the Stacks Project.

LocalizedModule.equivAwayColimit, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/LocalizedModule/Colimit.lean, line 208.

Stacks 00CR. S⁻¹M = colim_{f ∈ S} M_f: the localization of M at S is the directed colimit of the away-localizations M_f over f ∈ S with the divisibility preorder, with transition maps M_f → M_g for f ∣ g induced by the universal property.

noncomputable def equivAwayColimit : LocalizedModule S M ≃ₗ[R] AwayColimit S M
Tag 02C6, a proposition

Tag 02C6 in the Stacks Project.

Declarations registered for the tag:

Tag 02C7, a proposition

Tag 02C7 in the Stacks Project.

LocalizedModule.equivLocalizedModuleLocalizedModule, a def in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/LocalizedModule/LocalizationLocalization.lean, line 67.

Stacks 02C7. Iterated localization of modules: for multiplicative subsets S, S' ⊆ R and an R-module M, the localization of M at the multiplicative set SS' = S ⊔ S' is the localization at S of the R-module S'⁻¹M.

noncomputable def equivLocalizedModuleLocalizedModule :
    LocalizedModule (S ⊔ S') M ≃ₗ[R] LocalizedModule S (LocalizedModule S' M)
Tag 00CS, a proposition

Tag 00CS in the Stacks Project.

Declarations registered for the tag:

Tag 02C8, a lemma

Tag 02C8 in the Stacks Project.

Declarations registered for the tag:

Tag 00CT, a proposition

Tag 00CT in the Stacks Project.

IsLocalization.quotientEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Localization/Ideal.lean, line 30. The attribute's comment: “(2)”.

Localization commutes with quotients: for any localization Q of A/I at the image S̄ of S, there is a canonical algebra (in particular ring) isomorphism S̄⁻¹(A/I) ≅ S⁻¹A/S⁻¹I.

noncomputable def quotientEquiv : Q ≃ₐ[A ⧸ I] A_S ⧸ I.map (algebraMap A A_S)

Declarations registered for the tag:

Tag 00CU, a lemma

Tag 00CU in the Stacks Project.

Submodule.localized'_comap_restrictScalars, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/LocalizedModule/Submodule.lean, line 19. References: SGA 6 0 (2.11), “affine step”.

theorem localized'_comap_restrictScalars (N' : Submodule S N) :
    ((N'.restrictScalars R).comap f).localized' S p f = N'

Submodule.localized'_surjective, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/LocalizedModule/Submodule.lean, line 24. The attribute's comment: “existence form”.

theorem localized'_surjective : Function.Surjective (localized' S p f)
Tag 02C9, a lemma

Tag 02C9 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanSubmonoid · Localization · IsLocalization · IsLocalization.lift · IsLocalization.subsingleton_iff · ModuleCat.invertibleSMulEquivalentLocalizationModuleCat · LocalizedModule · IsLocalizedModule.lift_unique

Section10.10 Internal Hom#

Section 10.10 of the Stacks Project, Tag 0581. 2 tags here are carried by 2 declarations of the repository (all in StacksCore) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0582, a lemma

Tag 0582 in the Stacks Project.

LinearMap.exact_iff_homLeft, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Exact.lean, line 59. The attribute's comment: “part 2”.

theorem exact_iff_homLeft : (Function.Injective f ∧ Function.Exact f g) ↔
    ∀ (N : Type v) [AddCommGroup N] [Module R N],
      Function.Injective (compRight (M := N) ℕ f) ∧
      Function.Exact (compRight (M := N) ℕ f) (compRight (M := N) ℕ g)

LinearMap.exact_iff_homRight, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Exact.lean, line 81. The attribute's comment: “part 1”.

theorem exact_iff_homRight : (Function.Exact f g ∧ Function.Surjective g) ↔ ∀ (N : Type v)
    [AddCommGroup N] [Module R N], Function.Injective (lcomp ℕ N g) ∧
    Function.Exact (lcomp ℕ N g) (lcomp ℕ N f)
Tag 0583, a lemma

Tag 0583 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanLinearMap.exact_iff_homLeft · LinearMap.exact_iff_homRight · instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation · Module.FinitePresentation.isLocalizedModule_mapExtendScalars · Module.FinitePresentation.isLocalizedModule_map

Section10.11 Characterizing finite and finitely presented modules#

Section 10.11 of the Stacks Project, Tag 0G8M. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0G8N, a lemma

Tag 0G8N in the Stacks Project.

Stacks.Module.FinitenessViaHomColimit.finite_iff_comparisonMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Finiteness/HomColimit.lean, line 362. References: EGA IV (8.5.2.1), “Forward implication”.

Stacks Tag 0G8N. An R-module N is finite (finitely generated) if and only if for every filtered colimit M = colim_i M_i of R-modules the canonical comparison map Θ_N : colim_i Hom_R(N, M_i) → Hom_R(N, M) is injective.

theorem finite_iff_comparisonMap_injective (N : ModuleCat.{w} R) :
    Module.Finite R N ↔ InjectiveForAllFilteredColimits R N
Tag 07N8, a definition

Tag 07N8 in the Stacks Project.

Module.IsRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/Colimit.lean, line 215.

IsRelation f x says that the coefficients f give a relation among the elements x of an R-module, i.e. ∑ i, f i • x i = 0.

def IsRelation {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M]
    {ι : Type*} [Fintype ι] (f : ι → R) (x : ι → M) : Prop
Tag 00HA, a lemma

Tag 00HA in the Stacks Project.

Module.exists_linearEquiv_directLimit_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/Colimit.lean, line 162.

Every R-module M is the colimit of a directed system of finitely presented R-modules in the universe of M, provided R is small in that universe.

theorem Module.exists_linearEquiv_directLimit_finitePresentation
    (R : Type u) [Ring R] [Small.{v} R] (M : Type v) [AddCommGroup M] [Module R M] :
    ∃ (ι : Type v) (_ : Preorder ι) (_ : IsDirectedOrder ι) (_ : Nonempty ι)
      (_ : DecidableEq ι)
      (G : ι → Type v) (_ : (i : ι) → AddCommGroup (G i))
      (_ : (i : ι) → Module R (G i))
      (f : (i j : ι) → i ≤ j → (G i →ₗ[R] G j))
      (_ : DirectedSystem G (fun i j h => f i j h)),
      -- each module in the system is finitely presented
      (∀ i, Module.FinitePresentation R (G i)) ∧
      -- and M is isomorphic to the colimit of the system
      Nonempty (M ≃ₗ[R] Module.DirectLimit G f)

Module.exists_linearEquiv_directLimit_finitePresentation_max, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/FinitePresentation/Colimit.lean, line 195. The attribute's comment: “no smallness assumption on the ring”.

Every module is a directed colimit of finitely presented modules in the maximum of the universes of the ring and the module.

theorem Module.exists_linearEquiv_directLimit_finitePresentation_max
    (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] :
    ∃ (ι : Type (max u v)) (_ : Preorder ι) (_ : IsDirectedOrder ι) (_ : Nonempty ι)
      (_ : DecidableEq ι)
      (G : ι → Type (max u v)) (_ : (i : ι) → AddCommGroup (G i))
      (_ : (i : ι) → Module R (G i))
      (f : (i j : ι) → i ≤ j → (G i →ₗ[R] G j))
      (_ : DirectedSystem G (fun i j h => f i j h)),
      (∀ i, Module.FinitePresentation R (G i)) ∧
      Nonempty (M ≃ₗ[R] Module.DirectLimit G f)
Tag 0G8P, a lemma

Tag 0G8P in the Stacks Project.

finitePresentation_iff_comparisonMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/Finiteness/HomColimit.lean, line 692. References: EGA IV (8.5.2), “(i), special case”; EGA IV (8.5.2.1), “more general”; SGA 3 VIIB (0.3.5), “(3), special case”.

Stacks Tag 0G8P. An R-module N is finitely presented if and only if for every directed (filtered) system of R-modules the canonical comparison map Φ : colim_i Hom_R(N, M_i) → Hom_R(N, colim_i M_i) is bijective.

We quantify over index types ι and module families G in the universe u of R and N. The forward direction holds for directed systems in any universe. The converse uses the system of finitely generated submodules of N, which lives in the universe of N, and the system of quotients (Fin n →₀ R) ⧸ S Q, which lives in the universe of R.

theorem finitePresentation_iff_comparisonMap_bijective
    (R : Type u) [CommRing R] (N : Type u) [AddCommGroup N] [Module R N] :
    Module.FinitePresentation R N ↔
      ∀ {ι : Type u} [Preorder ι] [DecidableEq ι] [IsDirectedOrder ι] [Nonempty ι]
        (G : ι → Type u) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)]
        (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
        [DirectedSystem G (fun i j h => f i j h)],
        Function.Bijective (homColimComparison (R := R) (N := N) (ι := ι) G f)
Sources
LeanStacks.Module.FinitenessViaHomColimit.finite_iff_comparisonMap_injective · Module.IsRelation · Module.exists_linearEquiv_directLimit_finitePresentation · Module.exists_linearEquiv_directLimit_finitePresentation_max · finitePresentation_iff_comparisonMap_bijective

Section10.12 Tensor products#

Section 10.12 of the Stacks Project, Tag 00CV. 16 tags here are carried by 5 declarations of the repository (3 in StacksCore and 2 in StacksFrontier) and 25 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00CW, a definition

Tag 00CW in the Stacks Project.

Declarations registered for the tag:

Tag 00CX, a lemma

Tag 00CX in the Stacks Project.

Declarations registered for the tag:

Tag 00CY, a lemma

Tag 00CY in the Stacks Project.

Declarations registered for the tag:

Tag 00CZ, a lemma

Tag 00CZ in the Stacks Project.

Declarations registered for the tag:

Tag 00D0, a lemma

Tag 00D0 in the Stacks Project.

Declarations registered for the tag:

Tag 00D1, a definition

Tag 00D1 in the Stacks Project.

DistribMulAction.commute_toAddMonoidEnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Bimodule.lean, line 95. The attribute's comment: “The source's condition, that multiplication by a and multiplication by b commute, at the level of the multiplication operators: an equation in AddMonoid.End N. The condition as a class on the two actions is SMulCommClass, tagged below.”.

Stacks 00D1. In an (A, B)-bimodule multiplication by a : A and multiplication by b : B commute, as additive endomorphisms of N: this is the source's own phrasing of the bimodule condition, an equation in AddMonoid.End N.

The condition itself is SMulCommClass A B N, whose field smul_comm is the pointwise identity a • b • n = b • a • n; commuting of the operators is the form consumed by Algebra.TensorProduct.liftEquiv, hence by TensorProduct.Algebra.module.

public theorem DistribMulAction.commute_toAddMonoidEnd {A B N : Type*} [Monoid A] [Monoid B]
    [AddMonoid N] [DistribMulAction A N] [DistribMulAction B N] [SMulCommClass A B N] (a : A)
    (b : B) :
    Commute (DistribMulAction.toAddMonoidEnd A N a) (DistribMulAction.toAddMonoidEnd B N b)

Declarations registered for the tag:

  • SMulCommClass registered with add_to_stacks in StacksFrontier/Algebra/Module/Bimodule.lean, line 104 (StacksFrontier): “An (A, B)-bimodule is a type with [Module A N] [Module B N] [SMulCommClass A B N]: the source's data is the two module structures, and its one condition, that the actions commute, is this class, smul_comm being a • b • n = b • a • n, the source's b (a n) = a (b n) read from the other side. The class asks only for two SMuls, so this covers semirings acting on an additive commutative monoid as well as the source's rings acting on an abelian group. Writing the B-action on the right is the source's notation, not a further condition; the genuine right-action form is this class at Bᵐᵒᵖ, the bimodule set-up of Mathlib/Algebra/Module/Bimodule.lean.”.
Tag 00D2, a lemma

Tag 00D2 in the Stacks Project.

Declarations registered for the tag:

Tag 00DE, a lemma

Tag 00DE in the Stacks Project.

Declarations registered for the tag:

Tag 00DD, a lemma

Tag 00DD in the Stacks Project.

Declarations registered for the tag:

Tag 00DF, a lemma

Tag 00DF in the Stacks Project.

Declarations registered for the tag:

Tag 00DH, a remark

Tag 00DH in the Stacks Project.

tensorRight_not_preserve_exactness, a theorem in StacksCore (human-reviewed), declared in StacksCore/Counterexamples/TensorProduct.lean, line 25.

theorem tensorRight_not_preserve_exactness :
    ¬ ∀ (R : Type u) (_ : CommRing R) (M₁ : Type v)
      (M₂ M₃ : Type v') (N : Type w)
      (_ : AddCommGroup M₁) (_ : Module R M₁)
      (_ : AddCommGroup M₂) (_ : Module R M₂)
      (_ : AddCommGroup M₃) (_ : Module R M₃)
      (_ : AddCommGroup N) (_ : Module R N)
      (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃),
      Function.Exact f g →
      Function.Exact (f.rTensor N) (g.rTensor N)
Tag 00DI, an example

Tag 00DI in the Stacks Project.

TensorProduct.not_injective_rTensor_zmod_two_lsmul_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/TensorProduct/NotLeftExact.lean, line 84.

Stacks 00DI. Multiplication by 2 is an injective map of ℤ-modules ℤ → ℤ, but the induced map ℤ ⊗[ℤ] ℤ/2 → ℤ ⊗[ℤ] ℤ/2 is the zero map and hence not injective, ℤ ⊗[ℤ] ℤ/2 being nonzero. So tensoring does not preserve injectivity.

public theorem TensorProduct.not_injective_rTensor_zmod_two_lsmul_two :
    Function.Injective (LinearMap.lsmul ℤ ℤ (2 : ℤ)) ∧
      (LinearMap.lsmul ℤ ℤ (2 : ℤ)).rTensor (ZMod 2) = 0 ∧
      ¬ Function.Injective ((LinearMap.lsmul ℤ ℤ (2 : ℤ)).rTensor (ZMod 2))
Tag 00DJ, a remark

Tag 00DJ in the Stacks Project.

Declarations registered for the tag:

  • Module.Flat registered with add_to_stacks in StacksCore/RingTheory/Flat/Basic.lean, line 8 (StacksCore). References: EGA 0 (10.3.1.2); EGA 0 (10.3.1.3); EGA 0 (6.1.1); EGA IV (6.1.3); EGA IV (2.1.12); SGA 1 IV (4.3); SGA 3 VIIB (2.2.1), “special case”; SGA 4 V (1.1), “special case”; SGA 4 XVII (5.5.6.3); SGA 4½ Etat 0 (6.2), “special case”; SGA 5 IIIB (5.10); SGA 5 IIIB (6.1), “partial”; SGA 6 X (7.18.1).
Tag 05BS, a lemma

Tag 05BS in the Stacks Project.

Module.FinitePresentation.tensorProduct, an instance in StacksCore (human-reviewed), declared in StacksCore/RingTheory/TensorProduct/Finite.lean, line 38. The attribute's comment: “part 2”.

Stacks 05BS (2). The tensor product of two finitely presented modules is finitely presented.

instance Module.FinitePresentation.tensorProduct
    [Module.FinitePresentation R M] [Module.FinitePresentation R N] :
    Module.FinitePresentation R (M ⊗[R] N)

Declarations registered for the tag:

Tag 00DK, a lemma

Tag 00DK in the Stacks Project.

Declarations registered for the tag:

Tag 00DL, a lemma

Tag 00DL in the Stacks Project.

IsLocalization.tensorLocalizeEquivTensor, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Localization/BaseChange.lean, line 62. References: EGA 0 (1.3.4), “more general”.

Stacks 00DL. Localization commutes with tensor product: for any localization P of M ⊗[R] N at S, there is a canonical Rₛ-linear isomorphism M' ⊗[Rₛ] N' ≃ P. Taking Rₛ = S⁻¹R, M' = S⁻¹M, N' = S⁻¹N and P = S⁻¹(M ⊗_R N) gives the isomorphism S⁻¹M ⊗_{S⁻¹R} S⁻¹N ≅ S⁻¹(M ⊗_R N) of the Stacks project.

noncomputable def IsLocalization.tensorLocalizeEquivTensor
    [IsLocalizedModule S f] [IsLocalizedModule S g] [IsLocalizedModule S h] :
    M' ⊗[Rₛ] N' ≃ₗ[Rₛ] P
Sources
LeanLinearMap.mk₂ · TensorProduct.lift · TensorProduct.lift.unique · TensorProduct.directSumLeft · TensorProduct.lid · TensorProduct.comm · TensorProduct.comm_tmul · TensorProduct.prodLeft

Section10.13 Tensor algebra#

Section 10.13 of the Stacks Project, Tag 00DM. 6 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00DN, a lemma

Tag 00DN in the Stacks Project.

exteriorPower_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/SymmetricPower/Free.lean, line 37. References: EGA 0 (5.5.4), “free case”; SGA 6 X (6.1), “special case”.

If M is a free R-module, then for every n ≥ 0 the n-th exterior power ⋀^n(M) is a free R-module.

theorem exteriorPower_free
    (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M] [Module R M]
    [Module.Free R M] (n : ℕ) :
    Module.Free R (ExteriorAlgebra.exteriorPower R n M)

symmetricPower_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/SymmetricPower/Free.lean, line 299.

If M is a free R-module, then for every n ≥ 0 the n-th symmetric power Sym^n(M) is a free R-module.

theorem symmetricPower_free
    (R : Type) [CommSemiring R] (M : Type*) [AddCommMonoid M] [Module R M]
    [Module.Free R M] (n : ℕ) :
    Module.Free R (SymmetricPower R (Fin n) M)
Tag 00DO, a lemma

Tag 00DO in the Stacks Project.

symmetric_and_exterior_power_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/SymmetricPower/Presentation.lean, line 992.

Let R be a commutative ring and let M₂ --g--> M₁ --f--> M → 0 be an exact sequence of R-modules (f surjective and range g = ker f). With n = k + 1 ≥ 1, both presentation sequences are exact:

  • symmetric: M₂ ⊗ Sym^k(M₁) --α--> Sym^{k+1}(M₁) --Sym^{k+1}(f)--> Sym^{k+1}(M) → 0;
  • exterior: M₂ ⊗ ∧^k(M₁) --β--> ∧^{k+1}(M₁) --∧^{k+1}(f)--> ∧^{k+1}(M) → 0.

In each case the right-hand map is surjective and the image of the left-hand connecting map equals the kernel of the right-hand map.

theorem symmetric_and_exterior_power_presentation
    {R : Type*} [CommRing R]
    {M M₁ M₂ : Type*}
    [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup M₂] [Module R M₂]
    (g : M₂ →ₗ[R] M₁) (f : M₁ →ₗ[R] M)
    (hf : Function.Surjective f) (hexact : LinearMap.range g = LinearMap.ker f)
    (k : ℕ) :
    (Function.Surjective (symMap (k + 1) f) ∧
        LinearMap.range (symMulMap k g) = LinearMap.ker (symMap (k + 1) f)) ∧
      (Function.Surjective (exteriorPower.map (k + 1) f) ∧
        LinearMap.range (beta k g) = LinearMap.ker (exteriorPower.map (k + 1) f))
Tag 00DP, a lemma

Tag 00DP in the Stacks Project.

exists_presentation_exteriorPower_and_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/SymmetricPower/QuotientOfTensorPower.lean, line 300.

Stacks Tag 00DP. Let M be a module over a commutative ring R with a generating system x : I → M, and let n + 2 ≥ 2. There are canonical exact sequences

(⊕ relators) → Tⁿ⁺²(M) → ⋀ⁿ⁺²(M) → 0 and (⊕ relators) → Tⁿ⁺²(M) → Symⁿ⁺²(M) → 0,

with the relator maps and projections determined by their values on pure tensors as described in the module docstring.

theorem exists_presentation_exteriorPower_and_symmetricPower {I : Type*} [DecidableEq I] (x : I → M)
    (hx : Submodule.span R (Set.range x) = ⊤) (n : ℕ) :
    -- exterior power presentation
    (∃ (Φ : DirectSum ((SlotPair n × I × I) ⊕ (SlotPair n × I)) (fun _ => ⨂[R]^n M)
              →ₗ[R] ⨂[R]^(n + 2) M)
       (π : ⨂[R]^(n + 2) M →ₗ[R] ⋀[R]^(n + 2) M),
        (∀ (jp : SlotPair n) (i₁ i₂ : I) (f : Fin n → M),
          Φ (DirectSum.lof R _ _ (Sum.inl (jp, i₁, i₂)) (⨂ₜ[R] k, f k))
            = (⨂ₜ[R] k, insTwo jp.1.1 jp.1.2 jp.2 (x i₁) (x i₂) f k)
              + (⨂ₜ[R] k, insTwo jp.1.1 jp.1.2 jp.2 (x i₂) (x i₁) f k)) ∧
        (∀ (jp : SlotPair n) (i : I) (f : Fin n → M),
          Φ (DirectSum.lof R _ _ (Sum.inr (jp, i)) (⨂ₜ[R] k, f k))
            = (⨂ₜ[R] k, insTwo jp.1.1 jp.1.2 jp.2 (x i) (x i) f k)) ∧
        (∀ f : Fin (n + 2) → M, π (⨂ₜ[R] k, f k) = exteriorPower.ιMulti R (n + 2) f) ∧
        Function.Exact Φ π ∧ Function.Surjective π) ∧
    -- symmetric power presentation
    (∃ (Ψ : DirectSum (SlotPair n × I × I) (fun _ => ⨂[R]^n M) →ₗ[R] ⨂[R]^(n + 2) M)
       (ρ : ⨂[R]^(n + 2) M →ₗ[R] Sym[R]^(n + 2) M),
        (∀ (jp : SlotPair n) (i₁ i₂ : I) (f : Fin n → M),
          Ψ (DirectSum.lof R _ _ (jp, i₁, i₂) (⨂ₜ[R] k, f k))
            = (⨂ₜ[R] k, insTwo jp.1.1 jp.1.2 jp.2 (x i₁) (x i₂) f k)
              - (⨂ₜ[R] k, insTwo jp.1.1 jp.1.2 jp.2 (x i₂) (x i₁) f k)) ∧
        (∀ f : Fin (n + 2) → M, ρ (⨂ₜ[R] k, f k) = ⨂ₛ[R] k, f k) ∧
        Function.Exact Ψ ρ ∧ Function.Surjective ρ)
Tag 0H1C, a lemma

Tag 0H1C in the Stacks Project.

exteriorPower.ker_eq_span_of_tprod_eq_ιMulti, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/ExteriorPower/Presentation.lean, line 360. The attribute's comment: “first family mᵢ = b • mⱼ, not mᵢ = mⱼ: the latter fails for n = 2”.

Stacks 0H1C. Let A → B be a ring map, let M be a B-module and let n ≥ 1. The kernel of the canonical A-linear map M ⊗_A ⋯ ⊗_A M → ⋀[B]^n M, m₁ ⊗ ⋯ ⊗ mₙ ↦ m₁ ∧ ⋯ ∧ mₙ, is generated as an A-module by the pure tensors m₁ ⊗ ⋯ ⊗ mₙ with mᵢ = b • mⱼ for some i ≠ j and b ∈ B, together with the differences m₁ ⊗ ⋯ ⊗ b mᵢ ⊗ ⋯ ⊗ mₙ - m₁ ⊗ ⋯ ⊗ b mⱼ ⊗ ⋯ ⊗ mₙ for i ≠ j and b ∈ B.

theorem exteriorPower.ker_eq_span_of_tprod_eq_ιMulti
    {A B M : Type*} [CommRing A] [CommRing B] [Algebra A B] [AddCommGroup M]
    [Module A M] [Module B M] [IsScalarTower A B M] {n : ℕ} (hn : 0 < n)
    (φ : (⨂[A]^n M) →ₗ[A] ⋀[B]^n M)
    (hφ : ∀ m : Fin n → M, φ (PiTensorProduct.tprod A m) = exteriorPower.ιMulti B n m) :
    LinearMap.ker φ =
      Submodule.span A
        ({x | ∃ (m : Fin n → M) (i j : Fin n) (b : B), i ≠ j ∧ m i = b • m j ∧
              PiTensorProduct.tprod A m = x} ∪
          {x | ∃ (m : Fin n → M) (i j : Fin n) (b : B), i ≠ j ∧
              PiTensorProduct.tprod A (Function.update m i (b • m i)) -
                PiTensorProduct.tprod A (Function.update m j (b • m j)) = x})

exteriorPower.ker_eq_span_of_tprod_eq_ιMulti_of_two_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/ExteriorPower/Presentation.lean, line 379. The attribute's comment: “the stated form, for n ≥ 3”.

For 2 < n the tensors with two equal entries, together with the scaling differences, already generate the kernel.

theorem exteriorPower.ker_eq_span_of_tprod_eq_ιMulti_of_two_lt
    {A B M : Type*} [CommRing A] [CommRing B] [Algebra A B] [AddCommGroup M]
    [Module A M] [Module B M] [IsScalarTower A B M] {n : ℕ} (hn : 2 < n)
    (φ : (⨂[A]^n M) →ₗ[A] ⋀[B]^n M)
    (hφ : ∀ m : Fin n → M, φ (tprod A m) = exteriorPower.ιMulti B n m) :
    LinearMap.ker φ =
      Submodule.span A
        ({x | ∃ (m : Fin n → M) (i j : Fin n), i ≠ j ∧ m i = m j ∧ tprod A m = x} ∪
          {x | ∃ (m : Fin n → M) (i j : Fin n) (b : B), i ≠ j ∧
              tprod A (update m i (b • m i)) - tprod A (update m j (b • m j)) = x})
Tag 00DQ, a lemma

Tag 00DQ in the Stacks Project.

TensorAlgebra.ofDirectLimit_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Colimit.lean, line 168. The attribute's comment: “tensor”.

Forming the tensor algebra commutes with directed colimits: the canonical algebra map colim T(M_i) → T(colim M_i) is a bijection.

theorem TensorAlgebra.ofDirectLimit_bijective :
    Function.Bijective (TensorAlgebra.ofDirectLimit f)

SymmetricAlgebra.ofDirectLimit_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Colimit.lean, line 315. The attribute's comment: “symmetric”.

Forming the symmetric algebra commutes with directed colimits: the canonical algebra map colim Sym(M_i) → Sym(colim M_i) is a bijection.

theorem SymmetricAlgebra.ofDirectLimit_bijective :
    Function.Bijective (SymmetricAlgebra.ofDirectLimit f)

ExteriorAlgebra.ofDirectLimit_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Colimit.lean, line 433. The attribute's comment: “exterior”.

Forming the exterior algebra commutes with directed colimits: the canonical algebra map colim ⋀(M_i) → ⋀(colim M_i) is a bijection.

theorem ExteriorAlgebra.ofDirectLimit_bijective :
    Function.Bijective (ExteriorAlgebra.ofDirectLimit f)
Tag 0C6F, a lemma

Tag 0C6F in the Stacks Project.

TensorAlgebra.exists_algEquiv_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Localization.lean, line 32. The attribute's comment: “(1)”.

The tensor algebra of a base change is isomorphic to the base change of the tensor algebra, sending ι (1 ⊗ₜ m) to 1 ⊗ₜ ι m. Taking A = S⁻¹R gives compatibility with localization.

theorem TensorAlgebra.exists_algEquiv_baseChange :
    ∃ e : TensorAlgebra A (A ⊗[R] M) ≃ₐ[A] A ⊗[R] TensorAlgebra R M,
      ∀ m : M, e (ι A (1 ⊗ₜ[R] m)) = 1 ⊗ₜ[R] ι R m

SymmetricAlgebra.exists_algEquiv_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Localization.lean, line 43. The attribute's comment: “(2)”.

The symmetric algebra of a base change is isomorphic to the base change of the symmetric algebra, sending ι (1 ⊗ₜ m) to 1 ⊗ₜ ι m. Taking A = S⁻¹R gives compatibility with localization.

theorem SymmetricAlgebra.exists_algEquiv_baseChange :
    ∃ e : SymmetricAlgebra A (A ⊗[R] M) ≃ₐ[A] A ⊗[R] SymmetricAlgebra R M,
      ∀ m : M, e (ι A (A ⊗[R] M) (1 ⊗ₜ[R] m)) = 1 ⊗ₜ[R] ι R M m

ExteriorAlgebra.exists_algEquiv_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/TensorAlgebra/Localization.lean, line 89. The attribute's comment: “(3)”.

The exterior algebra of a base change is isomorphic to the base change of the exterior algebra, sending ι (1 ⊗ₜ m) to 1 ⊗ₜ ι m. Taking A = S⁻¹R gives compatibility with localization.

theorem ExteriorAlgebra.exists_algEquiv_baseChange :
    ∃ e : ExteriorAlgebra A (A ⊗[R] M) ≃ₐ[A] A ⊗[R] ExteriorAlgebra R M,
      ∀ m : M, e (ι A (1 ⊗ₜ[R] m)) = 1 ⊗ₜ[R] ι R m
Sources
LeanexteriorPower_free · symmetricPower_free · symmetric_and_exterior_power_presentation · exists_presentation_exteriorPower_and_symmetricPower · exteriorPower.ker_eq_span_of_tprod_eq_ιMulti · exteriorPower.ker_eq_span_of_tprod_eq_ιMulti_of_two_lt · TensorAlgebra.ofDirectLimit_bijective · SymmetricAlgebra.ofDirectLimit_bijective

Section10.14 Base change#

Section 10.14 of the Stacks Project, Tag 05G3. 5 tags here are carried by 3 declarations of the repository (all in StacksCore) and 13 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05G4, a definition

Tag 05G4 in the Stacks Project.

Declarations registered for the tag:

  • TensorProduct registered with add_to_stacks in StacksCore/LinearAlgebra/TensorProduct/Basic.lean, line 11 (StacksCore). References: EGA 0 (21.1.4), “partial”; EGA III (7.2.6); EGA IV (2.5.8), “partial”; EGA IV (18.3.2.1); SGA 2 III (2.11); SGA 2 IV (4.6); SGA 3 VIIB (2.3.2), “partial”; SGA 4 IV (12.7), “special case”; SGA 4 XVII (4.1.6), “special case”; SGA 4½ Cycle (1.3), “Clause a)”; SGA 4½ Fonctions L (3.8); SGA 5 V (1.2), “special case”; SGA 6 IV (2.6), “special case”; SGA 6 VII (4.6), “more general”; SGA 7 IX (4.7.3).
  • LinearMap.baseChange registered with add_to_stacks in StacksCore/LinearAlgebra/TensorProduct/Tower.lean, line 12 (StacksCore). References: EGA II (6.4.1); EGA II (6.4.2); EGA II (6.4.7); SGA 1 IV (2.6); SGA 4½ Fonctions L (3.8).
Tag 05G5, a lemma

Tag 05G5 in the Stacks Project.

Module.Finite.tensorBaseChange, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/FiniteStability.lean, line 156. The attribute's comment: “(1)”.

Stacks 05G5 (1): if M is a finite S-module then M' = M ⊗[R] R' is a finite S' = S ⊗[R] R'-module.

theorem Module.Finite.tensorBaseChange [Module.Finite S M] :
    Module.Finite (S ⊗[R] R') (M ⊗[R] R')

Module.FinitePresentation.tensorBaseChange, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/FiniteStability.lean, line 165. The attribute's comment: “(2)”.

Stacks 05G5 (2): if M is a finitely presented S-module then M' = M ⊗[R] R' is a finitely presented S' = S ⊗[R] R'-module.

theorem Module.FinitePresentation.tensorBaseChange [Module.FinitePresentation S M] :
    Module.FinitePresentation (S ⊗[R] R') (M ⊗[R] R')

Declarations registered for the tag:

Tag 05DQ, a lemma

Tag 05DQ in the Stacks Project.

Declarations registered for the tag:

Tag 08YP, a lemma

Tag 08YP in the Stacks Project.

Declarations registered for the tag:

Tag 08YQ, a lemma

Tag 08YQ in the Stacks Project.

tensorHomAdjEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/TensorProduct/Tower.lean, line 116.

Stacks 08YQ: Hom_R(M ⊗_S N, P) = Hom_S(M, Hom_R(N, P)) for S-modules M, N and an R-module P.

Stated S-linearly rather than as a bare bijection: both sides carry the source S-action — the left through M ⊗_S N, the right through Hom_R(N, P) — so S is the finer structure and R-linearity is its restriction. This matches how Mathlib states the sibling tag 05DQ, where LinearMap.liftBaseChangeEquiv is linear over the bigger ring.

noncomputable def tensorHomAdjEquiv : (M ⊗[S] N →ₗ[R] P) ≃ₗ[S] (M →ₗ[S] (N →ₗ[R] P))
Sources
LeanTensorProduct · LinearMap.baseChange · Module.Finite.tensorBaseChange · Module.FinitePresentation.tensorBaseChange · Algebra.FiniteType.baseChange · Algebra.FinitePresentation.baseChange · Module.Finite.tensorProduct · FinitePresentation.of_isBaseChange

Section10.15 Miscellany#

Section 10.15 of the Stacks Project, Tag 00DR. 7 tags here are carried by 13 declarations of the repository (9 in StacksCore and 4 in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07K1, a lemma

Tag 07K1 in the Stacks Project.

Declarations registered for the tag:

Tag 0EHL, a lemma

Tag 0EHL in the Stacks Project.

Ideal.exists_add_mem_notMem, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Ideal/Operations.lean, line 173.

Stacks 0EHL. If the coset x + I is contained in none of the ideals p i, then some x + y with y ∈ I avoids all of them simultaneously.

All but one of the p i must be prime; the exceptional index a matches the shape of Ideal.subset_union_prime. Allowing two exceptional indices is false.

theorem exists_add_mem_notMem (a : ι) {s : Finset ι} {p : ι → Ideal R}
    (hp : ∀ i ∈ s, i ≠ a → (p i).IsPrime) {I : Ideal R} {x : R}
    (h : ∀ i ∈ s, ¬(x ∈ p i ∧ I ≤ p i)) : ∃ y ∈ I, ∀ i ∈ s, x + y ∉ p i

Ideal.exists_add_mem_notMem', a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Ideal/Operations.lean, line 189.

Stacks 0EHL in the tag's literal wording, via Ideal.vadd_coe_subset_iff.

theorem exists_add_mem_notMem' (a : ι) {s : Finset ι} {p : ι → Ideal R}
    (hp : ∀ i ∈ s, i ≠ a → (p i).IsPrime) {I : Ideal R} {x : R}
    (h : ∀ i ∈ s, ¬x +ᵥ (I : Set R) ⊆ (p i : Set R)) : ∃ y ∈ I, ∀ i ∈ s, x + y ∉ p i
Tag 00DT, a lemma

Tag 00DT in the Stacks Project.

Declarations registered for the tag:

Tag 07DQ, a lemma

Tag 07DQ in the Stacks Project.

Matrix.exists_mul_eq_smul_one_of_mem_minorIdeal, a theorem in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/Matrix/Minor.lean, line 76. The attribute's comment: “(1)”.

Stacks 07DQ (1): every element of the ideal of maximal minors of A is realised as a scalar left inverse of A.

theorem exists_mul_eq_smul_one_of_mem_minorIdeal {A : Matrix n m R} {f : R}
    (hf : f ∈ A.minorIdeal) : ∃ B : Matrix m n R, B * A = f • 1

Matrix.pow_card_mem_minorIdeal, a theorem in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/Matrix/Minor.lean, line 99. The attribute's comment: “(2)”.

Stacks 07DQ (2): a scalar left inverse of A lies in the ideal of maximal minors of A after raising it to the number of columns of A.

theorem pow_card_mem_minorIdeal {A : Matrix n m R} {B : Matrix m n R} {f : R}
    (h : B * A = f • 1) : f ^ Fintype.card m ∈ A.minorIdeal

Matrix.mem_radical_minorIdeal_iff, a theorem in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/Matrix/Minor.lean, line 107.

Stacks 07DQ, both parts at once: the radical of the ideal of maximal minors of A is exactly the set of scalars some power of which admits a left inverse against A.

theorem mem_radical_minorIdeal_iff {A : Matrix n m R} {f : R} :
    f ∈ A.minorIdeal.radical ↔ ∃ k : ℕ, ∃ B : Matrix m n R, B * A = (f ^ k) • 1

exists_matrix_of_mem_minorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/MaximalMinors.lean, line 62. The attribute's comment: “(1)”.

Statement 1. For any f in the ideal J generated by the m × m minors of A, there is an m × n matrix B with B * A = f • 1 (the m × m matrix f · I_m).

theorem exists_matrix_of_mem_minorIdeal (A : Matrix (Fin n) (Fin m) R)
    (f : R) (hf : f ∈ maximalMinorsIdeal A) :
    ∃ B : Matrix (Fin m) (Fin n) R, B * A = f • (1 : Matrix (Fin m) (Fin m) R)

pow_mem_minorIdeal_of_matrix, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/MaximalMinors.lean, line 141. The attribute's comment: “(2)”.

Statement 2. If B * A = f • 1 for some m × n matrix B, then f ^ m lies in the ideal J generated by the m × m minors of A.

theorem pow_mem_minorIdeal_of_matrix (A : Matrix (Fin n) (Fin m) R)
    (f : R) (B : Matrix (Fin m) (Fin n) R)
    (hB : B * A = f • (1 : Matrix (Fin m) (Fin m) R)) :
    f ^ m ∈ maximalMinorsIdeal A
Tag 080R, a lemma

Tag 080R in the Stacks Project.

Matrix.fromRows_mul_adjugate, a theorem in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/Matrix/Adjugate.lean, line 34.

Stacks 080R.

theorem fromRows_mul_adjugate (A₁ : Matrix m m R) (A₂ : Matrix p m R) :
    fromRows A₁ A₂ * adjugate A₁ =
      fromRows (A₁.det • (1 : Matrix m m R))
        (Matrix.of fun (i : p) (j : m) => (A₁.updateRow j (A₂ i)).det)

Matrix.fromRows_mul_adjugate_apply_inr, a theorem in StacksCore (human-reviewed), declared in StacksCore/LinearAlgebra/Matrix/Adjugate.lean, line 44.

Stacks 080R, identifying the bottom block's entries as m × m minors of the stacked matrix — with no sign, taking the rows in the order 1, …, ĵ, …, m with i at slot j.

theorem fromRows_mul_adjugate_apply_inr (A₁ : Matrix m m R)
    (A₂ : Matrix p m R) (i : p) (j : m) :
    (fromRows A₁ A₂ * adjugate A₁) (Sum.inr i) j =
      ((fromRows A₁ A₂).submatrix (Function.update Sum.inl j (Sum.inr i)) id).det

ab_top_block, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/MaximalMinors.lean, line 309. The attribute's comment: “top block”.

Top block. With B = adj(A₁) and f = det(A₁), the top m × m block of A * B is f • 1: for all row/column indices i, j in the top block, (A * B)_{i j} = f · δ_{i j}.

theorem ab_top_block (hmn : m₀ + 1 ≤ n) (A : Matrix (Fin n) (Fin (m₀ + 1)) R)
    (i j : Fin (m₀ + 1)) :
    (A * (topBlock hmn A).adjugate) (Fin.castLE hmn i) j
      = (topBlock hmn A).det • (1 : Matrix (Fin (m₀ + 1)) (Fin (m₀ + 1)) R) i j

ab_bottom_block, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/MaximalMinors.lean, line 323. The attribute's comment: “bottom block”.

Bottom block. With B = adj(A₁), for a row index i lying in the bottom block (i.e. m ≤ i, here m₀ + 1 ≤ i) and any column index j, (A * B)_{i j} = (-1)^{m - j} · det(M_{i j}).

theorem ab_bottom_block (hmn : m₀ + 1 ≤ n) (A : Matrix (Fin n) (Fin (m₀ + 1)) R)
    (i : Fin n) (j : Fin (m₀ + 1)) :
    (A * (topBlock hmn A).adjugate) i j
      = (-1) ^ (m₀ - (j : ℕ)) * (minorMat hmn A i j).det
Tag 05WI, a lemma

Tag 05WI in the Stacks Project.

Module.not_injective_of_spanRank_lt, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/SpanRank.lean, line 31.

Stacks 05WI, in its general form: no nontriviality or Ring hypothesis, and stated as non-injectivity rather than as a nonzero kernel.

theorem not_injective_of_spanRank_lt [StrongRankCondition R] {n : ℕ}
    (h : (⊤ : Submodule R M).spanRank < n) (f : (Fin n → R) →ₗ[R] M) :
    ¬ Function.Injective f

LinearMap.ker_ne_bot_of_spanRank_lt, a theorem in StacksCore (human-reviewed), declared in StacksCore/Algebra/Module/SpanRank.lean, line 52.

Stacks 05WI in the tag's literal wording: the kernel is nonzero. The tag's n ≥ 1 is implied by spanRank ⊤ < n, and Module.Finite M is not needed.

theorem LinearMap.ker_ne_bot_of_spanRank_lt {n : ℕ}
    (h : (⊤ : Submodule R M).spanRank < n) (f : (Fin n → R) →ₗ[R] M) : LinearMap.ker f ≠ ⊥
Tag 0FJ7, a lemma

Tag 0FJ7 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanIdeal.IsPrime.mul_le · Ideal.exists_add_mem_notMem · Ideal.exists_add_mem_notMem' · Ideal.prod_eq_iInf_of_pairwise_isCoprime · Ideal.isCoprime_of_isMaximal · Ideal.IsMaximal.coprime_of_ne · Ideal.quotientInfRingEquivPiQuotient · Matrix.exists_mul_eq_smul_one_of_mem_minorIdeal

Section10.16 Cayley-Hamilton#

Section 10.16 of the Stacks Project, Tag 05G6. 4 tags here are carried by 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00DX, a lemma

Tag 00DX in the Stacks Project.

Declarations registered for the tag:

Tag 05BT, a lemma

Tag 05BT in the Stacks Project.

Declarations registered for the tag:

Tag 05G7, a lemma

Tag 05G7 in the Stacks Project.

Declarations registered for the tag:

Tag 05G8, a lemma

Tag 05G8 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanMatrix.aeval_self_charpoly · LinearMap.exists_monic_and_aeval_eq_zero · LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero · OrzechProperty.bijective_of_surjective_endomorphism

Section10.17 The spectrum of a ring#

Section 10.17 of the Stacks Project, Tag 00DY. 9 tags here are carried by 4 declarations of the repository (all in StacksCore) and 25 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00DZ, a definition

Tag 00DZ in the Stacks Project.

Declarations registered for the tag:

Tag 00E0, a lemma

Tag 00E0 in the Stacks Project.

PrimeSpectrum.basicOpen_eq_top_iff_isUnit, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 33. The attribute's comment: “17”.

theorem basicOpen_eq_top_iff_isUnit {f : R} :
    basicOpen f = ⊤ ↔ IsUnit f

PrimeSpectrum.basicOpen_eq_of_unit_mul, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 39. The attribute's comment: “13”. References: EGA I (1.1.9), “last clause”.

theorem basicOpen_eq_of_unit_mul {f f' u : R} (hu : IsUnit u) (h : f = u * f') :
    basicOpen f = basicOpen f'

PrimeSpectrum.exists_basicOpen_disjoint_zeroLocus, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 44. The attribute's comment: “14”.

theorem exists_basicOpen_disjoint_zeroLocus {I : Ideal R} {p : PrimeSpectrum R}
    (hp : p ∉ zeroLocus (I : Set R)) : ∃ f : R, p ∈ basicOpen f ∧
      (basicOpen f : Set (PrimeSpectrum R)) ∩ zeroLocus (I : Set R) = ∅

PrimeSpectrum.iUnion_basicOpen_eq_compl_zeroLocus, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 56. The attribute's comment: “16”. References: EGA I (1.1.1), “more general”.

theorem iUnion_basicOpen_eq_compl_zeroLocus {ι : Type*} (f : ι → R) :
    (⋃ i, (basicOpen (f i) : Set (PrimeSpectrum R))) = (zeroLocus (Set.range f))ᶜ

Declarations registered for the tag:

Tag 00E1, a definition

Tag 00E1 in the Stacks Project.

Declarations registered for the tag:

Tag 00E2, a lemma

Tag 00E2 in the Stacks Project.

Declarations registered for the tag:

Tag 00E3, a lemma

Tag 00E3 in the Stacks Project.

Declarations registered for the tag:

Tag 00E4, a lemma

Tag 00E4 in the Stacks Project.

Declarations registered for the tag:

Tag 00E5, a lemma

Tag 00E5 in the Stacks Project.

Declarations registered for the tag:

Tag 00E8, a lemma

Tag 00E8 in the Stacks Project.

Declarations registered for the tag:

Tag 04PM, a lemma

Tag 04PM in the Stacks Project.

Declarations registered for the tag:

Sources
LeanPrimeSpectrum · PrimeSpectrum.zeroLocus · PrimeSpectrum.basicOpen · PrimeSpectrum.basicOpen_eq_top_iff_isUnit · PrimeSpectrum.basicOpen_eq_of_unit_mul · PrimeSpectrum.exists_basicOpen_disjoint_zeroLocus · PrimeSpectrum.iUnion_basicOpen_eq_compl_zeroLocus · Ideal.exists_maximal

Section10.18 Local rings#

Section 10.18 of the Stacks Project, Tag 07BH. 4 tags here are carried by 5 declarations of the repository (all in StacksCore) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07BI, a definition

Tag 07BI in the Stacks Project.

Declarations registered for the tag:

Tag 0H70, an example

Tag 0H70 in the Stacks Project.

not_isLocalHom_algebraMap_atPrime, a theorem in StacksCore (human-reviewed), declared in StacksCore/Counterexamples/LocalHom.lean, line 30.

Stacks 0H70: for a local ring R and a non-maximal prime 𝔭, the localization map R → R_𝔭 is not a local homomorphism.

The witness is any x ∈ 𝔪_R \ 𝔭, which exists precisely because 𝔭 ⊊ 𝔪_R: it becomes a unit in R_𝔭, so a local homomorphism would force it to be a unit already in R, contradicting x ∈ 𝔪_R.

theorem not_isLocalHom_algebraMap_atPrime {R : Type*} [CommRing R] [IsLocalRing R]
    (p : Ideal R) [hp : p.IsPrime] (hne : p ≠ maximalIdeal R) :
    ¬ IsLocalHom (algebraMap R (Localization.AtPrime p))
Tag 00E9, a lemma

Tag 00E9 in the Stacks Project.

isLocalRing_iff_exists_maximal_isUnit, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/LocalRing/MaximalIdeal/Basic.lean, line 41. The attribute's comment: “(1) ⇔ (3)”.

Stacks 00E9, clause (1) ⇔ (3): a ring is local if and only if it has a maximal ideal m such that every element outside m is a unit.

The forward direction takes m to be IsLocalRing.maximalIdeal R, where being outside m is definitionally being a unit (IsLocalRing.notMem_maximalIdeal). The reverse direction cannot use IsLocalRing.of_unique_max_ideal directly — that wants uniqueness, which is not assumed — so it goes through IsLocalRing.of_nonunits_add: the hypothesis says every nonunit lies in m, and m is closed under addition. Nontriviality comes from m ≠ ⊤.

theorem isLocalRing_iff_exists_maximal_isUnit {R : Type*} [CommSemiring R] :
    IsLocalRing R ↔ ∃ m : Ideal R, m.IsMaximal ∧ ∀ x : R, x ∉ m → IsUnit x

isLocalRing_iff_existsUnique_isClosed_singleton, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 145. The attribute's comment: “(1) ⇔ (2)”. References: EGA I (2.4.1), “more general”.

Stacks 00E9, clause (1) ⇔ (2): a ring is local if and only if its spectrum has exactly one closed point.

The clause is genuinely topological, so it is stated that way rather than as uniqueness of a maximal ideal. PrimeSpectrum.isClosed_singleton_iff_isMaximal is what converts between the two, in both directions; the rest is transport between PrimeSpectrum R and Ideal R along PrimeSpectrum.ext.

No nontriviality hypothesis is needed: for the zero ring the spectrum is empty, so it has no closed point at all and clause (2) fails on its own.

theorem isLocalRing_iff_existsUnique_isClosed_singleton {R : Type*} [CommSemiring R] :
    IsLocalRing R ↔ ∃! p : PrimeSpectrum R, IsClosed ({p} : Set (PrimeSpectrum R))

Declarations registered for the tag:

Tag 00E7, a lemma

Tag 00E7 in the Stacks Project.

Ideal.nontrivial_fiber_iff, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Fiber.lean, line 75. The attribute's comment: “(2) ⇔ (3)”.

Stacks 00E7, clause (2) ⇔ clause (3): the fibre κ(𝔭) ⊗_R S is nonzero if and only if S_𝔭 / 𝔭 S_𝔭 is nonzero.

Both are ways of saying the fibre of Spec S → Spec R over 𝔭 is nonempty; for the link to clause (1), that 𝔭 lies in the image, see PrimeSpectrum.nontrivial_iff_mem_rangeComap (tagged in StacksCore.RingTheory.Spectrum.Prime.RingHom).

theorem nontrivial_fiber_iff :
    Nontrivial (p.Fiber S) ↔ Nontrivial (Sp ⧸ p.map (algebraMap R Sp))

Ideal.nontrivial_quotient_localization_iff, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Fiber.lean, line 128. The attribute's comment: “(3) ⇔ (4)”.

Stacks 00E7, clause (3) ⇔ clause (4): S_𝔭 / 𝔭 S_𝔭 is nonzero if and only if (S/𝔭S)_𝔭 is nonzero.

theorem nontrivial_quotient_localization_iff :
    Nontrivial SpS ↔ Nontrivial (Sp ⧸ p.map (algebraMap R Sp))

Declarations registered for the tag:

Sources
LeanIsLocalHom · IsLocalRing · IsLocalRing.maximal_ideal_unique · IsLocalRing.maximalIdeal · IsLocalRing.ResidueField · IsLocalRing.residue · not_isLocalHom_algebraMap_atPrime · isLocalRing_iff_exists_maximal_isUnit

Section10.19 The Jacobson radical of a ring#

Section 10.19 of the Stacks Project, Tag 0AMD. 2 tags here are carried by 2 declarations of the repository (all in StacksCore) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AME, a lemma

Tag 0AME in the Stacks Project.

Ideal.le_ringJacobson_iff_isUnit_one_add, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Jacobson/Ideal.lean, line 35. The attribute's comment: “(1) ⇔ (2)”.

Stacks 0AME, (1) ⇔ (2): an ideal is contained in the Jacobson radical if and only if every element of 1 + I is a unit.

Forwards is Ideal.mem_jacobson_bot at y = 1. Backwards uses that I is an ideal: to place x ∈ I in the radical one must invert 1 + x * y for every y, and x * y is again in I.

theorem le_ringJacobson_iff_isUnit_one_add (I : Ideal R) :
    I ≤ Ring.jacobson R ↔ ∀ x ∈ I, IsUnit (1 + x)

Ideal.isUnit_of_isUnit_quotient_mk, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Jacobson/Ideal.lean, line 49. The attribute's comment: “in this case a unit mod I is a unit”.

Stacks 0AME, the closing clause: if I is contained in the Jacobson radical, then an element of R whose image in R ⧸ I is a unit is itself a unit.

Given a right inverse y mod I, the difference x * y - 1 lies in I and hence in the radical, so x * y is a unit by Ideal.isUnit_of_sub_one_mem_jacobson_bot; a factor of a unit in a commutative ring is a unit.

theorem isUnit_of_isUnit_quotient_mk (I : Ideal R) (h : I ≤ Ring.jacobson R) (x : R)
    (hx : IsUnit (Ideal.Quotient.mk I x)) : IsUnit x
Tag 0B7C, a lemma

Tag 0B7C in the Stacks Project.

Declarations registered for the tag:

Sources
LeanIdeal.le_ringJacobson_iff_isUnit_one_add · Ideal.isUnit_of_isUnit_quotient_mk · IsLocalHom.of_comap_surjective

Section10.20 Nakayama's lemma#

Section 10.20 of the Stacks Project, Tag 07RC. 3 tags here are carried by 12 declarations of the repository (all in StacksCore) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00DV, a lemma

Tag 00DV in the Stacks Project.

LinearMap.exists_sub_one_mem_and_map_surjective_of_surjective_comp_mkQ, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 93. The attribute's comment: “(5)”.

Stacks 00DV (5): if φ : N →ₗ[R] M has N/IN → M/IM surjective and M is finite, then some r ∈ 1 + I makes φ surjective after localizing at the powers of r.

Stated against arbitrary localization witnesses fN, fM, so it applies to any model of N_r and M_r. For the concrete LocalizedModule reading see LinearMap.exists_sub_one_mem_and_localizedMap_surjective_of_surjective_comp_mkQ.

Dropping the hypothesis I ≤ rad(R) of LinearMap.surjective_of_surjective_comp_mkQ (part (6)) costs surjectivity of φ itself; inverting one element of 1 + I recovers it.

theorem LinearMap.exists_sub_one_mem_and_map_surjective_of_surjective_comp_mkQ
    (I : Ideal R) (φ : N →ₗ[R] M) [Module.Finite R M]
    (hsurj : Function.Surjective ((I • (⊤ : Submodule R M)).mkQ ∘ₗ φ)) :
    ∃ r : R, r - 1 ∈ I ∧ ∀ {Nᵣ Mᵣ : Type*} [AddCommGroup Nᵣ] [Module R Nᵣ]
      [AddCommGroup Mᵣ] [Module R Mᵣ] (fN : N →ₗ[R] Nᵣ) (fM : M →ₗ[R] Mᵣ)
      [IsLocalizedModule (Submonoid.powers r) fN] [IsLocalizedModule (Submonoid.powers r) fM],
      Function.Surjective (IsLocalizedModule.map (Submonoid.powers r) fN fM φ)

LinearMap.exists_sub_one_mem_and_localizedMap_surjective_of_surjective_comp_mkQ, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 114. The attribute's comment: “(5)”.

Stacks 00DV (5), in the concrete LocalizedModule model: the tag's literal "N_f → M_f is surjective".

This is LinearMap.exists_sub_one_mem_and_map_surjective_of_surjective_comp_mkQ at the canonical witnesses LocalizedModule.mkLinearMap.

theorem LinearMap.exists_sub_one_mem_and_localizedMap_surjective_of_surjective_comp_mkQ
    (I : Ideal R) (φ : N →ₗ[R] M) [Module.Finite R M]
    (hsurj : Function.Surjective ((I • (⊤ : Submodule R M)).mkQ ∘ₗ φ)) :
    ∃ r : R, r - 1 ∈ I ∧
      Function.Surjective (LocalizedModule.map (Submonoid.powers r) φ)

Submodule.exists_sub_one_mem_and_span_image_eq_top, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 136. The attribute's comment: “(7)”.

Stacks 00DV (7): if s generates M/IM and M is finite, then some r ∈ 1 + I makes s generate M after localizing at the powers of r.

"s generates M/IM" is taken literally, as s spanning the quotient M ⧸ I • ⊤. Internally that is converted to the Submodule.span R s ⊔ I • ⊤ = ⊤ form which part (3) consumes, by span_sup_smul_top_eq_top_of_span_image_mk_eq_top. Stated against arbitrary localization witnesses S, fM; for the concrete reading see Submodule.exists_sub_one_mem_and_span_image_mkLinearMap_eq_top.

The tag writes a finite list x₁, …, xₙ, but finiteness of the generating set is not used — only finiteness of M. Take s := Set.range x to recover the tag's form.

theorem Submodule.exists_sub_one_mem_and_span_image_eq_top
    (I : Ideal R) [Module.Finite R M] (s : Set M)
    (hs : Submodule.span R
      (Submodule.Quotient.mk '' s : Set (M ⧸ I • (⊤ : Submodule R M))) = ⊤) :
    ∃ r : R, r - 1 ∈ I ∧ ∀ {S Mᵣ : Type*} [CommRing S] [Algebra R S]
      [AddCommGroup Mᵣ] [Module R Mᵣ] [Module S Mᵣ] [IsScalarTower R S Mᵣ]
      [IsLocalization (Submonoid.powers r) S] (fM : M →ₗ[R] Mᵣ)
      [IsLocalizedModule (Submonoid.powers r) fM],
      Submodule.span S (fM '' s) = ⊤

Submodule.exists_sub_one_mem_and_span_image_mkLinearMap_eq_top, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 158. The attribute's comment: “(7)”.

Stacks 00DV (7), in the concrete LocalizedModule model: the tag's literal "x₁, …, xₙ generate M_f over R_f".

theorem Submodule.exists_sub_one_mem_and_span_image_mkLinearMap_eq_top
    (I : Ideal R) [Module.Finite R M] (s : Set M)
    (hs : Submodule.span R
      (Submodule.Quotient.mk '' s : Set (M ⧸ I • (⊤ : Submodule R M))) = ⊤) :
    ∃ r : R, r - 1 ∈ I ∧
      Submodule.span (Localization (Submonoid.powers r))
        (LocalizedModule.mkLinearMap (Submonoid.powers r) M '' s) = ⊤

Submodule.eq_bot_of_le_smul_of_isNilpotent, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 170. The attribute's comment: “(9)”.

Stacks 00DV (9): if N ≤ I • N and I is nilpotent, then N = ⊥.

theorem Submodule.eq_bot_of_le_smul_of_isNilpotent (I : Ideal R) (N : Submodule R M)
    (hI : IsNilpotent I) (hN : N ≤ I • N) : N = ⊥

Submodule.le_of_le_smul_of_isNilpotent, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 189. The attribute's comment: “(10)”.

Stacks 00DV (10): if N' ≤ N ⊔ I • N' and I is nilpotent, then N' ≤ N.

The nilpotent counterpart of Submodule.le_of_le_smul_of_le_jacobson_bot (part (4)), which assumes I ≤ jacobson ⊥ and N'.FG instead; as everywhere in this block the finiteness goes.

This is (9) read in M ⧸ N: mapping the hypothesis through N.mkQ kills the N summand (Submodule.mkQ_map_self) while Submodule.map_smul'' carries I • N' across, leaving map N.mkQ N' ≤ I • map N.mkQ N' — exactly (9)'s hypothesis on the quotient.

The tag words it as M = N + I N'; that is the case N' := ⊤, reached from the tag's hypothesis via I • N' ≤ I • ⊤. Parts (11) and (12) are both this lemma at N' := ⊤, with N taken to be range φ and span R s respectively.

theorem Submodule.le_of_le_smul_of_isNilpotent {I : Ideal R} {N N' : Submodule R M}
    (hI : IsNilpotent I) (hNN : N' ≤ N ⊔ I • N') : N' ≤ N

LinearMap.surjective_of_surjective_comp_mkQ_of_isNilpotent, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 199. The attribute's comment: “(11)”.

Stacks 00DV (11): if φ : N →ₗ[R] M has N/IN → M/IM surjective and I is nilpotent, then φ is surjective.

theorem LinearMap.surjective_of_surjective_comp_mkQ_of_isNilpotent
    (I : Ideal R) (φ : N →ₗ[R] M) (hI : IsNilpotent I)
    (hsurj : Function.Surjective ((I • (⊤ : Submodule R M)).mkQ ∘ₗ φ)) :
    Function.Surjective φ

Submodule.span_eq_top_of_span_image_mkQ_eq_top_of_isNilpotent, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Nakayama.lean, line 214. The attribute's comment: “(12)”.

Stacks 00DV (12): if s generates M/IM and I is nilpotent, then s generates M.

The nilpotent counterpart of part (8), and (10) at N := span R s, N' := ⊤. As in part (7) the hypothesis is taken literally — s spans the quotient M ⧸ I • ⊤ — and nothing requires s to be finite, so the tag's {xα} is an arbitrary s : Set M. Unlike (7), M need not be finite either.

theorem Submodule.span_eq_top_of_span_image_mkQ_eq_top_of_isNilpotent
    (I : Ideal R) (hI : IsNilpotent I) (s : Set M)
    (hs : Submodule.span R
      (Submodule.Quotient.mk '' s : Set (M ⧸ I • (⊤ : Submodule R M))) = ⊤) :
    Submodule.span R s = ⊤

Declarations registered for the tag:

Tag 0GLX, a lemma

Tag 0GLX in the Stacks Project.

Module.exists_localizedMap_away_surjective_of_localizedMap_surjective, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Support.lean, line 82. The attribute's comment: “the footnote's special case (I), I = 0; for the general statement see Submodule.exists_mem_addIdeal_and_span_image_eq_top below”.

Stacks 0GLX, special case (I) I = 0: if φ becomes surjective after localizing at S, it is already surjective after localizing at a single f ∈ S.

Taking φ to be (a₁, …, a_r) ↦ ∑ aⱼxⱼ recovers the footnote's wording: if x₁, …, x_r generate S⁻¹M, then they generate M_f for some f ∈ S.

The arbitrary-submonoid form of Module.exists_localizedMap_away_surjective_of_localizedMap_atPrime_surjective, and it needs only Module.Finite on the target — Module.FinitePresentation, which the bijective analogue exists_bijective_map_powers requires, is not needed for surjectivity alone.

theorem Module.exists_localizedMap_away_surjective_of_localizedMap_surjective
    {N : Type*} [AddCommGroup N] [Module R N]
    (S : Submonoid R) [Module.Finite R M] (φ : N →ₗ[R] M)
    (hφ : Function.Surjective (LocalizedModule.map S φ)) :
    ∃ f ∈ S, Function.Surjective (LocalizedModule.map (Submonoid.powers f) φ)

Submodule.exists_mem_addIdeal_and_span_image_eq_top, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Support.lean, line 172. References: EGA IV (2.5.8.8), “partial, special case”; SGA 3 V (4.1.3), “more general”; SGA 6 III (5.4.1), “special case”.

Stacks 0GLX: if s generates S⁻¹(M/IM) and M is finite, then s generates M_f for some f ∈ S + I.

The proof does not follow the Stacks argument, which localizes twice — first at some s ∈ S, then at some g ∈ 1 + I_s via Nakayama — and then glues the two into a single f = ss' + is, a step the tag leaves as "details omitted". Instead it localizes once, at T = S + I.

That works because T is a submonoid (Submonoid.addIdeal) which absorbs I under addition, so I lands in the Jacobson radical of T⁻¹R (Ideal.map_addIdeal_le_ringJacobson) and Nakayama applies over T directly. Concretely: enlarge the hypothesis from S to T (Submodule.span_image_eq_top_iff at both ends), strip the quotient, apply 00DV (4) (Submodule.le_of_le_smul_of_le_jacobson_bot) to get that s spans T⁻¹M, then descend to a single f ∈ T by the I = 0 case above. S + I is not an ad-hoc answer: it is exactly the submonoid over which I becomes Jacobson.

Stated against arbitrary localization witnesses; see Submodule.exists_mem_addIdeal_and_span_image_mkLinearMap_eq_top for the concrete reading. The hypothesis is phrased over S⁻¹R rather than the tag's S⁻¹(R/I); spans agree along the surjection S⁻¹R ↠ S⁻¹(R/I), so this is a simplification and not a weakening. As in 00DV (7), s need not be finite — only M — and the tag's x₁, …, x_r is s := Set.range x.

theorem Submodule.exists_mem_addIdeal_and_span_image_eq_top
    (S : Submonoid R) (I : Ideal R) [Module.Finite R M] (s : Set M)
    {Rₛ Qₛ : Type*} [CommRing Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ]
    [AddCommGroup Qₛ] [Module R Qₛ] [Module Rₛ Qₛ] [IsScalarTower R Rₛ Qₛ]
    (fQ : (M ⧸ I • (⊤ : Submodule R M)) →ₗ[R] Qₛ) [IsLocalizedModule S fQ]
    (hs : Submodule.span Rₛ (fQ '' (Submodule.Quotient.mk '' s)) = ⊤) :
    ∃ f ∈ S.addIdeal I, ∀ {Rf Mf : Type*} [CommRing Rf] [Algebra R Rf]
      [IsLocalization (Submonoid.powers f) Rf] [AddCommGroup Mf] [Module R Mf] [Module Rf Mf]
      [IsScalarTower R Rf Mf] (g : M →ₗ[R] Mf) [IsLocalizedModule (Submonoid.powers f) g],
      Submodule.span Rf (g '' s) = ⊤

Submodule.exists_mem_addIdeal_and_span_image_mkLinearMap_eq_top, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Support.lean, line 194.

Stacks 0GLX, in the concrete LocalizedModule model: the tag's literal M_f.

theorem Submodule.exists_mem_addIdeal_and_span_image_mkLinearMap_eq_top
    (S : Submonoid R) (I : Ideal R) [Module.Finite R M] (s : Set M)
    (hs : Submodule.span (Localization S)
      (LocalizedModule.mkLinearMap S (M ⧸ I • (⊤ : Submodule R M)) ''
        (Submodule.Quotient.mk '' s)) = ⊤) :
    ∃ f ∈ S.addIdeal I, Submodule.span (Localization (Submonoid.powers f))
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M '' s) = ⊤
Tag 0E8M, a lemma

Tag 0E8M in the Stacks Project.

IsLocalRing.surjective_of_surjective_mapCotangent, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/LocalRing/RingHom/Basic.lean, line 75.

Stacks 0E8M: a local homomorphism A → B with B finite over A, m_B finitely generated, surjective on residue fields, and surjective on cotangent spaces, is surjective.

The cotangent hypothesis gives m_A B = m_B, so B ⧸ m_A B is the residue field of B, and the residue hypothesis says A already surjects onto it. Nakayama (00DV (6)) promotes that to surjectivity of A → B.

The tag asks for an isomorphism on residue fields; surjectivity is all that is used.

theorem IsLocalRing.surjective_of_surjective_mapCotangent [Module.Finite A B]
    (hmB : (maximalIdeal B).FG)
    (hres : Function.Surjective (ResidueField.map (algebraMap A B)))
    (hcot : Function.Surjective (Ideal.mapCotangent (maximalIdeal A) (maximalIdeal B)
      (Algebra.ofId A B) (le_of_eq (maximalIdeal_comap (algebraMap A B)).symm))) :
    Function.Surjective (algebraMap A B)
Sources
LeanLinearMap.exists_sub_one_mem_and_map_surjective_of_surjective_comp_mkQ · LinearMap.exists_sub_one_mem_and_localizedMap_surjective_of_surjective_comp_mkQ · Submodule.exists_sub_one_mem_and_span_image_eq_top · Submodule.exists_sub_one_mem_and_span_image_mkLinearMap_eq_top · Submodule.eq_bot_of_le_smul_of_isNilpotent · Submodule.le_of_le_smul_of_isNilpotent · LinearMap.surjective_of_surjective_comp_mkQ_of_isNilpotent · Submodule.span_eq_top_of_span_image_mkQ_eq_top_of_isNilpotent

Section10.21 Open and closed subsets of spectra#

Section 10.21 of the Stacks Project, Tag 04PN. 3 tags here are carried by 6 declarations of the repository (all in StacksCore) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00ED, a lemma

Tag 00ED in the Stacks Project.

Declarations registered for the tag:

Tag 00EF, a lemma

Tag 00EF in the Stacks Project.

PrimeSpectrum.preconnectedSpace_iff_mul_eq_zero_add_eq_one, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 72. The attribute's comment: “for a semiring, phrased with complementary pairs”.

Stacks 00EF, in its most general form. Over a semiring the statement must be phrased with complementary pairs rather than idempotents: an idempotent need not have a complement, so "every idempotent is 0 or 1" is strictly stronger than preconnectedness there. Mathlib's own example, on PrimeSpectrum.mulZeroAddOneEquivClopens, is the semiring {0, 0.5, 1} with ⊔ = + and ⊓ = *, in which 0.5 is idempotent and uncomplemented.

Pairs e * f = 0, e + f = 1 are exactly what index the clopens of Spec R, which is why this is the level at which the equivalence is true.

theorem preconnectedSpace_iff_mul_eq_zero_add_eq_one :
    PreconnectedSpace (PrimeSpectrum R) ↔
      ∀ e f : R, e * f = 0 → e + f = 1 → e = 0 ∨ f = 0

PrimeSpectrum.preconnectedSpace_iff_isIdempotentElem, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 96. The attribute's comment: “without the nonzero hypothesis, for PreconnectedSpace”. References: EGA III (7.8.6.1), “affine case Z = Spec R”.

Stacks 00EF without the nonzero hypothesis. Over a ring every idempotent e has the complement 1 - e, so the pair formulation collapses to the familiar one.

This form needs no Nontrivial R: for the zero ring Spec R is empty, hence preconnected, and the right-hand side holds vacuously. It is ConnectedSpace — which bundles nonemptiness — that forces the hypothesis, see connectedSpace_iff_isIdempotentElem.

theorem preconnectedSpace_iff_isIdempotentElem :
    PreconnectedSpace (PrimeSpectrum R) ↔ ∀ e : R, IsIdempotentElem e → e = 0 ∨ e = 1

PrimeSpectrum.connectedSpace_iff_isIdempotentElem, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 110. References: EGA III (7.8.6.1), “special case”.

Stacks 00EF: for a nonzero ring, Spec R is connected if and only if R has no nontrivial idempotents.

The Nontrivial R hypothesis is load-bearing and not merely inherited from the tag's wording: for the zero ring the right-hand side holds vacuously while Spec R is empty, so ConnectedSpace fails. Dropping it would make the statement false, not weaker.

theorem connectedSpace_iff_isIdempotentElem [Nontrivial R] :
    ConnectedSpace (PrimeSpectrum R) ↔ ∀ e : R, IsIdempotentElem e → e = 0 ∨ e = 1
Tag 00EH, a lemma

Tag 00EH in the Stacks Project.

IsLocalization.Away.quotient_span_singleton_of_isIdempotentElem, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Localization/Away/Lemmas.lean, line 30. The attribute's comment: “(2)”. References: SGA 3 VIIB (0.1.1), “partial”.

Stacks 00EH, clause (2), in the tag's orientation: for an idempotent e, the quotient R ⧸ (e) is the localization of R away from 1 - e.

This is IsLocalization.Away.quotient_of_isIdempotentElem with e replaced by 1 - e, but that substitution cannot be performed by rewriting: the offending 1 - (1 - e) occurs as a type index of the quotient, so simp and ▸ both fail on the motive. Going through IsLocalization.away_of_isIdempotentElem instead puts the kernel equation in hypothesis position, where simp reaches it.

theorem IsLocalization.Away.quotient_span_singleton_of_isIdempotentElem {e : R}
    (he : IsIdempotentElem e) : IsLocalization.Away (1 - e) (R ⧸ Ideal.span {e})

IsLocalization.Away.quotientAlgEquiv, a def in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Localization/Away/Lemmas.lean, line 37. The attribute's comment: “(2)”.

Stacks 00EH, clause (2), as the isomorphism the tag states. Mathlib carries only the IsLocalization.Away predicate, never a bundled map, so this records R ⧸ (e) ≅ R_{1 - e}.

noncomputable def IsLocalization.Away.quotientAlgEquiv {e : R} (he : IsIdempotentElem e) :
    (R ⧸ Ideal.span {e}) ≃ₐ[R] Localization.Away (1 - e)

PrimeSpectrum.isClopen_zeroLocus_of_isIdempotentElem_of_fg, a theorem in StacksCore (human-reviewed), declared in StacksCore/RingTheory/Spectrum/Prime/Topology.lean, line 123. The attribute's comment: “(3)”.

Stacks 00EH, clause (3): the vanishing locus of a finitely generated idempotent ideal is open as well as closed.

Only one implication holds. I.FG cannot be dropped — in a rank-one non-discrete valuation ring the maximal ideal satisfies m * m = m without being finitely generated, and V(m) is closed but not open — and there is no converse: for I = (x) in k[x]/(x²) the set V(I) is all of Spec R, hence clopen, while I * I = 0 ≠ I.

theorem isClopen_zeroLocus_of_isIdempotentElem_of_fg {I : Ideal R} (hfg : I.FG)
    (h : IsIdempotentElem I) : IsClopen (zeroLocus (I : Set R))

Declarations registered for the tag:

Sources
LeanPrimeSpectrum.primeSpectrumProdHomeo · PrimeSpectrum.sigmaToPiHomeo · PrimeSpectrum.preconnectedSpace_iff_mul_eq_zero_add_eq_one · PrimeSpectrum.preconnectedSpace_iff_isIdempotentElem · PrimeSpectrum.connectedSpace_iff_isIdempotentElem · IsLocalization.Away.quotient_span_singleton_of_isIdempotentElem · IsLocalization.Away.quotientAlgEquiv · PrimeSpectrum.isClopen_zeroLocus_of_isIdempotentElem_of_fg

Section10.22 Connected components of spectra#

Section 10.22 of the Stacks Project, Tag 00EB. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04PP, a lemma

Tag 04PP in the Stacks Project.

PrimeSpectrum.isClosed_and_biUnion_connectedComponent_eq_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/ConnectedComponents.lean, line 288.

Let R be a commutative ring and T ⊆ Spec R. The following are equivalent: T is closed and a union of connected components of Spec R; T is an intersection of open and closed subsets of Spec R; T = V I for some ideal I generated by idempotents; there is a unique such ideal I; and T is the zero locus of the ideal generated by all idempotents vanishing on T.

theorem isClosed_and_biUnion_connectedComponent_eq_tfae (T : Set (PrimeSpectrum R)) :
    [IsClosed T ∧ (⋃ x ∈ T, connectedComponent x) = T,
      ∃ S : Set (Set (PrimeSpectrum R)), (∀ U ∈ S, IsClopen U) ∧ T = ⋂₀ S,
      ∃ I : Ideal R, (∃ s : Set R, (∀ e ∈ s, IsIdempotentElem e) ∧ I = Ideal.span s) ∧
        T = zeroLocus (I : Set R),
      ∃! I : Ideal R, (∃ s : Set R, (∀ e ∈ s, IsIdempotentElem e) ∧ I = Ideal.span s) ∧
        T = zeroLocus (I : Set R),
      T = zeroLocus
        (Ideal.span {e : R | IsIdempotentElem e ∧ T ⊆ zeroLocus {e}} : Set R)].TFAE
Tag 00EG, a lemma

Tag 00EG in the Stacks Project.

PrimeSpectrum.exists_connectedComponent_eq_zeroLocus_span_isIdempotentElem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Spectrum/Prime/ConnectedComponents.lean, line 354.

Stacks Tag 00EG. For any commutative ring R and any point x of Spec R, the connected component of x is V(I) for an ideal I generated by idempotents such that every idempotent of R maps to 0 or 1 in R/I.

theorem PrimeSpectrum.exists_connectedComponent_eq_zeroLocus_span_isIdempotentElem
    (x : PrimeSpectrum R) :
    ∃ I : Ideal R,
      connectedComponent x = PrimeSpectrum.zeroLocus (I : Set R) ∧
      I = Ideal.span {e : R | e ∈ I ∧ IsIdempotentElem e} ∧
      ∀ e : R, IsIdempotentElem e →
        (Ideal.Quotient.mk I e = 0 ∨ Ideal.Quotient.mk I e = 1)
Sources
LeanPrimeSpectrum.isClosed_and_biUnion_connectedComponent_eq_tfae · PrimeSpectrum.exists_connectedComponent_eq_zeroLocus_span_isIdempotentElem

Section10.23 Glueing properties#

Section 10.23 of the Stacks Project, Tag 00EN. 3 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 15 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00HN, a lemma

Tag 00HN in the Stacks Project.

Declarations registered for the tag:

Tag 00EO, a lemma

Tag 00EO in the Stacks Project.

Module.subsingleton_of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 60. The attribute's comment: “(1)”.

Stacks 00EO (1). If each canonical localisation LocalizedModule (powers (f i)) M is the zero module and the f i generate the unit ideal, then M itself is the zero module.

theorem Module.subsingleton_of_localizationSpan_range
    {R : Type*} [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, Subsingleton (LocalizedModule (Submonoid.powers (f i)) M)) :
    Subsingleton M

Module.Finite.of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 73. The attribute's comment: “(2)”. References: SGA 4½ Arcata (1.4.2), “(ii) fin type, Zariski”.

Stacks 00EO (2). If each canonical localisation M_{f i} is finite over R_{f i} and the f i generate the unit ideal, then M is a finite R-module.

theorem Module.Finite.of_localizationSpan_range
    {R : Type*} [CommSemiring R] {M : Type*} [AddCommMonoid M] [Module R M]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, Module.Finite (Localization.Away (f i))
                            (LocalizedModule (Submonoid.powers (f i)) M)) :
    Module.Finite R M

bijective_of_localized_span_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 86. The attribute's comment: “(4)”.

Stacks 00EO (4). If φ : M →ₗ[R] N is bijective after canonical localisation at each f i and the f i generate the unit ideal, then φ is bijective.

theorem bijective_of_localized_span_range
    {R : Type*} [CommSemiring R]
    {M N : Type*} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
    (φ : M →ₗ[R] N)
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (hiso : ∀ i, Function.Bijective
                  (LocalizedModule.map (Submonoid.powers (f i)) φ)) :
    Function.Bijective φ

shortExact_of_localized_span_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 101. The attribute's comment: “(5)”.

Stacks 00EO (5). Let g : M'' →ₗ[R] M and h : M →ₗ[R] M' be linear maps. If 0 → M''_{f i} → M_{f i} → M'_{f i} → 0 is exact for each i and the f i generate the unit ideal, then 0 → M'' → M → M' → 0 is exact.

theorem shortExact_of_localized_span_range
    {R : Type*} [CommSemiring R]
    {M'' M M' : Type*}
    [AddCommMonoid M''] [Module R M'']
    [AddCommMonoid M] [Module R M]
    [AddCommMonoid M'] [Module R M']
    (g : M'' →ₗ[R] M) (h : M →ₗ[R] M')
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (hexact : ∀ i,
      Function.Injective (LocalizedModule.map (Submonoid.powers (f i)) g) ∧
      Function.Exact (LocalizedModule.map (Submonoid.powers (f i)) g)
        (LocalizedModule.map (Submonoid.powers (f i)) h) ∧
      Function.Surjective (LocalizedModule.map (Submonoid.powers (f i)) h)) :
    Function.Injective g ∧ Function.Exact g h ∧ Function.Surjective h

IsNoetherianRing.of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 123. The attribute's comment: “(6)”.

Stacks 00EO (6). If each canonical R_{f i} = Localization.Away (f i) is Noetherian and the f i generate the unit ideal, then R is Noetherian.

theorem IsNoetherianRing.of_localizationSpan_range
    {R : Type*} [CommSemiring R]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, IsNoetherianRing (Localization.Away (f i))) :
    IsNoetherianRing R

Algebra.FiniteType.of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 140. The attribute's comment: “(7)”.

Stacks 00EO (7). If each canonical S_{f i} is a finite-type R_{f i}-algebra and the f i generate the unit ideal, then S is a finite-type R-algebra.

theorem Algebra.FiniteType.of_localizationSpan_range
    {R : Type*} [CommRing R] {S : Type*} [CommRing S] [Algebra R S]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, (Localization.awayMap (algebraMap R S) (f i)).FiniteType) :
    Algebra.FiniteType R S

Algebra.FinitePresentation.of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 164. The attribute's comment: “(8)”.

Stacks 00EO (8). If each canonical S_{f i} is of finite presentation over R_{f i} and the f i generate the unit ideal, then S is a finitely presented R-algebra.

theorem Algebra.FinitePresentation.of_localizationSpan_range
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, letI : Algebra (Localization.Away (f i))
                              (Localization.Away (algebraMap R S (f i))) :=
                (IsLocalization.Away.map (Localization.Away (f i))
                  (Localization.Away (algebraMap R S (f i)))
                  (algebraMap R S) (f i)).toAlgebra
              Algebra.FinitePresentation (Localization.Away (f i))
                                         (Localization.Away (algebraMap R S (f i)))) :
    Algebra.FinitePresentation R S

Module.FinitePresentation.of_localizationSpan_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalProperties/StandardCover.lean, line 183. The attribute's comment: “(3)”. References: SGA 4½ Arcata (1.4.2), “(ii) fin pres, Zariski”.

Stacks 00EO (3). If each canonical localisation M_{f i} is finitely presented over R_{f i} and the f i generate the unit ideal, then M is finitely presented over R.

theorem Module.FinitePresentation.of_localizationSpan_range
    {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
    {ι : Type*} (f : ι → R)
    (hf : Ideal.span (Set.range f) = ⊤)
    (h : ∀ i, Module.FinitePresentation (Localization.Away (f i))
                                       (LocalizedModule (Submonoid.powers (f i)) M)) :
    Module.FinitePresentation R M
Tag 00EP, a lemma

Tag 00EP in the Stacks Project.

Declarations registered for the tag:

Sources
LeanModule.eq_zero_of_localization_maximal · Module.subsingleton_of_localization_maximal · Module.support_eq_empty_iff · IsLocalizedModule.subsingleton_of_subsingleton · exact_of_localized_maximal · exact_of_isLocalized_maximal · IsLocalizedModule.map_exact · injective_of_localized_maximal

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.