The Čech complex of localizations

Let R be a commutative ring, M an R-module and f : ι → R a family indexed by a linearly ordered type. For a finite set S ⊆ ι write f_S = ∏_{i ∈ S} f i and M_{f_S} for the localization of M away from f_S. The (alternating, extended) Čech complex of localizations is 0 → M → ∏_{|S| = 1} M_{f_S} → ∏_{|S| = 2} M_{f_S} → ⋯. Its augmentation sends m to m / 1 in every factor. Its differential sends x to the family whose S-component is ∑_{a ∈ S} (-1)^k x_{S ∖ {a}}, where k is the number of elements of S below a and x_{S ∖ {a}} is restricted along M_{f_{S ∖ {a}}} → M_{f_S}. Listing S as i₀ < ⋯ < i_{p+1}, this is the usual formula ∑_k (-1)^k x_{i₀ ⋯ î_k ⋯ i_{p+1}}.

When ι is finite and the f i generate the unit ideal, the complex is exact. This is the module-level form of the vanishing of the higher Čech cohomology of the quasi-coherent sheaf associated to M on the cover of Spec R by the basic opens D(f i). It is the algebraic input to Huber's proof of sheafiness for Huber rings with a noetherian ring of definition, where this complex of localizations is topologized and completed.

Main definitions

• TauCeti.cechLocalizationTerm M f p: the degree p term ∏_{|S| = p + 1} M_{f_S}.
• TauCeti.cechLocalizationRestriction M f h: the restriction M_{f_T} → M_{f_S} for T ⊆ S.
• TauCeti.cechLocalizationAugmentation M f: the augmentation M → ∏_{|S| = 1} M_{f_S}.
• TauCeti.cechLocalizationDifferential M f p: the differential in degree p.

Main results

• TauCeti.cechLocalizationDifferential_comp_augmentation and TauCeti.cechLocalizationDifferential_comp_differential: the maps form a complex.
• TauCeti.injective_cechLocalizationAugmentation, TauCeti.exact_cechLocalizationAugmentation_differential and TauCeti.cechComplexLocalization_exact: the complex is exact if ι is finite and the f i generate the unit ideal.

Implementation notes

Indexing by finite subsets rather than by increasing tuples turns deletion of a vertex into Finset.erase, and lets the contracting homotopy insert a vertex with insert. Exactness is local on Spec R (exact_of_isLocalized_span): after inverting f j, the localized complex is the Čech complex of M_{f j}, on which f j acts invertibly, and inserting j into each subset gives a contracting homotopy.

References

• The Stacks Project, Tag 01X9 (Lemma 30.2.1, Čech cohomology of quasi-coherent sheaves on affine schemes).
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, proof of (1.3).

noncomputable def TauCeti.cechLocalizationEraseRingHom {R : Type u_1} [CommRing R] {ι : Type u_3} (f : ι → R) [DecidableEq ι] (S : Finset ι) (a : ↥S) : Localization.Away (∏ i ∈ S.erase ↑a, f i) →+* Localization.Away (∏ i ∈ S, f i)

The localization homomorphism from a face with one vertex deleted to the full face.

theorem TauCeti.cechLocalizationEraseRingHom_eq_awayLift {R : Type u_1} [CommRing R] {ι : Type u_3} (f : ι → R) [DecidableEq ι] (S : Finset ι) (a : ↥S) : cechLocalizationEraseRingHom f S a = IsLocalization.Away.lift (∏ x ∈ S.erase ↑a, f x) ⋯

The deleted-face homomorphism is the canonical lift between the two localizations.

theorem TauCeti.isScalarTower_compHom_cechLocalizationEraseRingHom {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [DecidableEq ι] (S : Finset ι) (a : ↥S) : IsScalarTower R (Localization.Away (∏ i ∈ S.erase ↑a, f i)) (LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M)

Restricting the localized module action along cechLocalizationEraseRingHom respects the original coefficient-ring action.

The complex

@[reducible, inline]

abbrev TauCeti.cechLocalizationTerm {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) (p : ℕ) : Type (max (max u_1 u_2) u_3)

The degree p term of the Čech complex of localizations: the product of the localizations M_{f_S}, f_S = ∏_{i ∈ S} f i, over the subsets S with p + 1 elements.

noncomputable def TauCeti.cechLocalizationRestriction {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {T S : Finset ι} (h : T ⊆ S) : LocalizedModule (Submonoid.powers (∏ i ∈ T, f i)) M →ₗ[R] LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M

The restriction M_{f_T} → M_{f_S} for T ⊆ S: the map out of M_{f_T} extending the canonical map M → M_{f_S}, which exists since f_T divides f_S.

@[simp]

theorem TauCeti.cechLocalizationRestriction_mk {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {T S : Finset ι} (h : T ⊆ S) (m : M) : (cechLocalizationRestriction M f h) (LocalizedModule.mk m 1) = LocalizedModule.mk m 1

The restriction maps extend the canonical maps from M.

theorem TauCeti.cechLocalizationRestriction_restriction {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {T S U : Finset ι} (hTS : T ⊆ S) (hSU : S ⊆ U) (x : LocalizedModule (Submonoid.powers (∏ i ∈ T, f i)) M) : (cechLocalizationRestriction M f hSU) ((cechLocalizationRestriction M f hTS) x) = (cechLocalizationRestriction M f ⋯) x

The restriction maps are compatible with composition.

@[simp]

theorem TauCeti.cechLocalizationRestriction_comp_mkLinearMap {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {T S : Finset ι} (h : T ⊆ S) : cechLocalizationRestriction M f h ∘ₗ LocalizedModule.mkLinearMap (Submonoid.powers (∏ i ∈ T, f i)) M = LocalizedModule.mkLinearMap (Submonoid.powers (∏ i ∈ S, f i)) M

The restriction maps are compatible with the canonical maps from M.

theorem TauCeti.eq_cechLocalizationRestriction {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {T S : Finset ι} (h : T ⊆ S) {g : LocalizedModule (Submonoid.powers (∏ i ∈ T, f i)) M →ₗ[R] LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M} (hg : g ∘ₗ LocalizedModule.mkLinearMap (Submonoid.powers (∏ i ∈ T, f i)) M = LocalizedModule.mkLinearMap (Submonoid.powers (∏ i ∈ S, f i)) M) : g = cechLocalizationRestriction M f h

The restriction M_{f_T} → M_{f_S} is the unique linear map extending the canonical map M → M_{f_S}.

@[simp]

theorem TauCeti.cechLocalizationRestriction_self {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) {S : Finset ι} (h : S ⊆ S) (x : LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M) : (cechLocalizationRestriction M f h) x = x

Restriction along S ⊆ S is the identity.

noncomputable def TauCeti.cechLocalizationAugmentation {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) : M →ₗ[R] cechLocalizationTerm M f 0

The augmentation M → ∏_{|S| = 1} M_{f_S}, sending m to m / 1 in every factor.

@[simp]

theorem TauCeti.cechLocalizationAugmentation_apply {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) (m : M) (S : { S : Finset ι // S.card = 0 + 1 }) : (cechLocalizationAugmentation M f) m S = LocalizedModule.mk m 1

The differential is defined uniformly on the products ∏_{|S| = q} M_{f_S} for all q, including q = 0, where the only factor is M_{f_∅} = M_1.

The contracting homotopy after inverting f j

Localizing the complex

The augmented complex

noncomputable def TauCeti.cechLocalizationDifferential {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] (p : ℕ) : cechLocalizationTerm M f p →ₗ[R] cechLocalizationTerm M f (p + 1)

The differential of the Čech complex of localizations in degree p. The component of cechLocalizationDifferential M f p x at S is the alternating sum of the restrictions of the components of x at the subsets S ∖ {a} (cechLocalizationDifferential_apply).

theorem TauCeti.cechLocalizationDifferential_apply {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] (p : ℕ) (x : cechLocalizationTerm M f p) (S : { S : Finset ι // S.card = p + 1 + 1 }) : (cechLocalizationDifferential M f p) x S = ∑ a ∈ (↑S).attach, (-1) ^ {x ∈ ↑S | x < ↑a}.card • (cechLocalizationRestriction M f ⋯) (x ⟨(↑S).erase ↑a, ⋯⟩)

The differential of the Čech complex: the component at S is ∑_{a ∈ S} (-1)^k x_{S ∖ {a}}, where k is the number of elements of S below a.

theorem TauCeti.cechLocalizationDifferential_comp_augmentation {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] : cechLocalizationDifferential M f 0 ∘ₗ cechLocalizationAugmentation M f = 0

The augmentation followed by the first differential is zero.

theorem TauCeti.cechLocalizationDifferential_comp_differential {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] (p : ℕ) : cechLocalizationDifferential M f (p + 1) ∘ₗ cechLocalizationDifferential M f p = 0

Two consecutive differentials compose to zero.

theorem TauCeti.injective_cechLocalizationAugmentation {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] [Finite ι] (hf : Ideal.span (Set.range f) = ⊤) : Function.Injective ⇑(cechLocalizationAugmentation M f)

If the f i generate the unit ideal, the augmentation of the Čech complex is injective.

theorem TauCeti.exact_cechLocalizationAugmentation_differential {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] [Finite ι] (hf : Ideal.span (Set.range f) = ⊤) : Function.Exact ⇑(cechLocalizationAugmentation M f) ⇑(cechLocalizationDifferential M f 0)

If the f i generate the unit ideal, the Čech complex is exact at its degree 0 term.

theorem TauCeti.cechComplexLocalization_exact {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] {ι : Type u_3} (f : ι → R) [LinearOrder ι] [Finite ι] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : Function.Exact ⇑(cechLocalizationDifferential M f p) ⇑(cechLocalizationDifferential M f (p + 1))

Exactness of the Čech complex of localizations. If ι is finite and the f i generate the unit ideal, the Čech complex of localizations of M is exact in every positive degree.