The topology of the Čech complex of uncompleted rational localisations

Let B be a topological ring with a pair of definition (C, I), let f : ι → B be a family generating the unit ideal and let M be a B-module. For a finite set S ⊆ ι with p + 1 elements write f_S = ∏_{i ∈ S} f i. The intersection U_S = ⋂_{i ∈ S} R(f / f i) of the standard rational subsets is the rational subset R(F_p / f_S), whose numerators F_p = {∏_k f (j k) | j : Fin (p + 1) → ι} are the products of p + 1 members of the family. Its uncompleted coordinate ring is the localisation B_{f_S}, with Wedhorn's topology TauCeti.Huber.PairOfDefinition.locTopology: the ring of definition is C[F_p / f_S] = C[f j / f i : j ∈ ι, i ∈ S] with ideal of definition generated by I.

The degree p term ∏_{|S| = p + 1} M_{f_S} of the Čech complex of localizations (TauCeti.cechLocalizationTerm) is then a product of modules over these Huber rings. This file gives it the product of their natural module topologies and the corresponding uniformity, and describes the topology by the filtration of Huber's proof of sheafiness for Huber rings with a noetherian ring of definition: for a set N of generators of M, the i-th subgroup in degree p is the product over the faces S of Iⁱ · C[F_p / f_S] · N ⊆ M_{f_S}. When ι is finite, N is finite and N generates M, these subgroups form a basis of neighbourhoods of zero. These are the topologised terms whose completions form Huber's completed Čech complex.

No noetherian or completeness hypothesis is needed for anything in this file. The noetherian ring of definition enters in the strictness of the complex and in the topology of its augmentation term, which are not treated here.

Main definitions

• TauCeti.Huber.NoetherianCech.numerators f p: the numerators F_p of the rational subsets U_S, |S| = p + 1.
• TauCeti.Huber.NoetherianCech.faceTopology and TauCeti.Huber.NoetherianCech.facePair: the topology of B_{f_S} as the uncompleted rational localisation B(F_p / f_S), and its pair of definition.
• TauCeti.Huber.NoetherianCech.termTopology, termUniformSpace: the product of the natural module topologies on the term of degree p, and its additive uniformity.
• TauCeti.Huber.NoetherianCech.filtration: Huber's filtration K_i^p of the term of degree p.

Main results

• TauCeti.Huber.NoetherianCech.hasDenominatorPower: Wedhorn's denominator-power hypothesis for every face, so that the topologies above exist.
• TauCeti.Huber.NoetherianCech.isTopologicalAddGroup_termTopology and isUniformAddGroup_termUniformSpace: the term is a topological, and a uniform, additive group.
• TauCeti.Huber.NoetherianCech.hasBasis_nhds_zero_filtration: the filtration is a basis of neighbourhoods of zero.
• TauCeti.Huber.NoetherianCech.hasBasis_uniformity_filtration: the filtration gives a basis of entourages of termUniformSpace.

References

• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, proof of Theorem 2.5, Case I, (1.2)(ii) and (1.3.1)(ii).
• T. Wedhorn, Adic Spaces, Proposition and Definition 5.51.

The numerators of the faces

def TauCeti.Huber.NoetherianCech.numerators {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) (p : ℕ) : Set B

The numerators F_p = {∏_k f (j k) | j : Fin (p + 1) → ι} of the rational subset ⋂_{i ∈ S} R(f / f i) = R(F_p / f_S) attached to a face S with p + 1 elements.

@[simp]

theorem TauCeti.Huber.NoetherianCech.mem_numerators {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) {p : ℕ} {b : B} : b ∈ numerators f p ↔ ∃ (j : Fin (p + 1) → ι), ∏ k : Fin (p + 1), f (j k) = b

The numerators in degree p are the products of p + 1 members of the family.

theorem TauCeti.Huber.NoetherianCech.pow_mem_numerators {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) (p : ℕ) (i : ι) : f i ^ (p + 1) ∈ numerators f p

Each f i ^ (p + 1) is a numerator in degree p.

theorem TauCeti.Huber.NoetherianCech.span_numerators_eq_top {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : Ideal.span (numerators f p) = ⊤

If the f i generate the unit ideal, so do the numerators in every degree.

theorem TauCeti.Huber.NoetherianCech.mul_mem_numerators {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) {p : ℕ} {t : B} (ht : t ∈ numerators f p) (a : ι) : t * f a ∈ numerators f (p + 1)

Multiplying a degree-p numerator by one cover element gives a degree-p + 1 numerator.

theorem TauCeti.Huber.NoetherianCech.hasDenominatorPower {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : P.HasDenominatorPower (numerators f p) (∏ i ∈ S, f i) (Localization.Away (∏ i ∈ S, f i))

The denominator-power hypothesis holds on every face. If the f i generate the unit ideal, so do the numerators F_p, and an open (here: the unit) numerator ideal supplies Wedhorn's standing hypothesis for every denominator, in particular for f_S.

The topology of a face

@[instance_reducible]

noncomputable def TauCeti.Huber.NoetherianCech.faceTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : TopologicalSpace (Localization.Away (∏ i ∈ S, f i))

The topology of B_{f_S} as the uncompleted rational localisation B(F_p / f_S).

theorem TauCeti.Huber.NoetherianCech.isTopologicalRing_faceTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : IsTopologicalRing (Localization.Away (∏ i ∈ S, f i))

faceTopology is a ring topology.

theorem TauCeti.Huber.NoetherianCech.faceTopology_eq_locTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : faceTopology f P hf p S = P.locTopology (numerators f p) (∏ i ∈ S, f i) (Localization.Away (∏ i ∈ S, f i)) ⋯

faceTopology is Wedhorn's topology on B_{f_S} for the numerators F_p.

noncomputable def TauCeti.Huber.NoetherianCech.facePair {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : PairOfDefinition (Localization.Away (∏ i ∈ S, f i))

The pair of definition (C[F_p / f_S], I · C[F_p / f_S]) of B(F_p / f_S).

@[simp]

theorem TauCeti.Huber.NoetherianCech.facePair_ringOfDefinition {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : (facePair f P hf p S).ringOfDefinition = P.locSubring (numerators f p) (∏ i ∈ S, f i) (Localization.Away (∏ i ∈ S, f i))

The ring of definition of facePair is C[F_p / f_S].

@[simp]

theorem TauCeti.Huber.NoetherianCech.mem_facePair_idealOfDefinition {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) {x : ↥(facePair f P hf p S).ringOfDefinition} : x ∈ (facePair f P hf p S).idealOfDefinition ↔ ⟨↑x, ⋯⟩ ∈ P.locIdeal (numerators f p) (∏ i ∈ S, f i) (Localization.Away (∏ i ∈ S, f i))

Membership in the ideal of definition of facePair is membership in I · C[F_p / f_S].

theorem TauCeti.Huber.NoetherianCech.eraseRingHom_mem_ringOfDefinition {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) [DecidableEq ι] (p : ℕ) (S : Finset ι) (a : ↥S) {r : Localization.Away (∏ i ∈ S.erase ↑a, f i)} : r ∈ (facePair f P hf p (S.erase ↑a)).ringOfDefinition → (cechLocalizationEraseRingHom f S a) r ∈ (facePair f P hf (p + 1) S).ringOfDefinition

The deleted-face localization homomorphism preserves the rings of definition.

theorem TauCeti.Huber.NoetherianCech.map_eraseRingHom_idealOfDefinition_le {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (hf : Ideal.span (Set.range f) = ⊤) [DecidableEq ι] (p : ℕ) (S : Finset ι) (a : ↥S) : Ideal.map ((cechLocalizationEraseRingHom f S a).restrict (facePair f P hf p (S.erase ↑a)).ringOfDefinition (facePair f P hf (p + 1) S).ringOfDefinition ⋯) (facePair f P hf p (S.erase ↑a)).idealOfDefinition ≤ (facePair f P hf (p + 1) S).idealOfDefinition

The deleted-face localization homomorphism maps the ideal of definition into the ideal of definition of the full face.

The topology of the terms

@[instance_reducible]

noncomputable def TauCeti.Huber.NoetherianCech.faceModuleTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : TopologicalSpace (LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M)

The natural topology of M_{f_S} as a module over the uncompleted rational localisation B(F_p / f_S).

theorem TauCeti.Huber.NoetherianCech.isModuleTopology_faceModuleTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : IsModuleTopology (Localization.Away (∏ i ∈ S, f i)) (LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M)

faceModuleTopology is the natural module topology over B(F_p / f_S).

theorem TauCeti.Huber.NoetherianCech.isTopologicalAddGroup_faceModuleTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : IsTopologicalAddGroup (LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M)

M_{f_S} is a topological additive group for faceModuleTopology.

theorem TauCeti.Huber.NoetherianCech.continuousSMul_faceModuleTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) : ContinuousSMul B (LocalizedModule (Submonoid.powers (∏ i ∈ S, f i)) M)

The natural topology on a localized module makes its action by the original coefficient ring continuous.

@[instance_reducible]

noncomputable def TauCeti.Huber.NoetherianCech.termTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : TopologicalSpace (cechLocalizationTerm M f p)

The topology on the term ∏_{|S| = p + 1} M_{f_S} of degree p of the Čech complex of localizations: the product of the natural module topologies of the M_{f_S} over the uncompleted rational localisations B(F_p / f_S).

theorem TauCeti.Huber.NoetherianCech.termTopology_eq_pi {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : termTopology f P M hf p = Pi.topologicalSpace

termTopology is the product of the natural module topologies of the factors.

theorem TauCeti.Huber.NoetherianCech.isTopologicalAddGroup_termTopology {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : IsTopologicalAddGroup (cechLocalizationTerm M f p)

The term of degree p is a topological additive group.

@[instance_reducible]

noncomputable def TauCeti.Huber.NoetherianCech.termUniformSpace {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : UniformSpace (cechLocalizationTerm M f p)

The additive uniformity of termTopology.

theorem TauCeti.Huber.NoetherianCech.termUniformSpace_toTopologicalSpace {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : (termUniformSpace f P M hf p).toTopologicalSpace = termTopology f P M hf p

termUniformSpace induces termTopology.

instance TauCeti.Huber.NoetherianCech.isUniformAddGroup_termUniformSpace {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) : IsUniformAddGroup (cechLocalizationTerm M f p)

The term of degree p is a uniform additive group for termUniformSpace.

Huber's filtration

noncomputable def TauCeti.Huber.NoetherianCech.faceFiltration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p : ℕ) (S : Finset ι) (i : ℕ) : AddSubgroup (LocalizedModule (Submonoid.powers (∏ j ∈ S, f j)) M)

The i-th subgroup Iⁱ · C[F_p / f_S] · N of M_{f_S}, where N ⊆ M is mapped to M_{f_S} by m ↦ m / 1. These are the sections over the chart D₊(f_S T^{p + 1}) of Iⁱ times the sheaf associated to the submodule generated by N on Huber's submodule blow-up.

@[simp]

theorem TauCeti.Huber.NoetherianCech.mem_faceFiltration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p : ℕ) (S : Finset ι) (i : ℕ) (x : LocalizedModule (Submonoid.powers (∏ j ∈ S, f j)) M) : x ∈ faceFiltration f P M hf N p S i ↔ x ∈ (facePair f P hf p S).idealOfDefinition ^ i • Submodule.span (↥(facePair f P hf p S).ringOfDefinition) (⇑(LocalizedModule.mkLinearMap (Submonoid.powers (∏ j ∈ S, f j)) M) '' N)

Membership in faceFiltration is membership in Iⁱ · C[F_p / f_S] · N.

@[simp]

theorem TauCeti.Huber.NoetherianCech.faceFiltration_zero {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p : ℕ) (S : Finset ι) : faceFiltration f P M hf N p S 0 = (Submodule.span (↥(facePair f P hf p S).ringOfDefinition) (⇑(LocalizedModule.mkLinearMap (Submonoid.powers (∏ j ∈ S, f j)) M) '' N)).toAddSubgroup

Level zero of the face filtration is the C[F_p / f_S]-span of N.

@[simp]

theorem TauCeti.Huber.NoetherianCech.faceFiltration_empty {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p : ℕ) (S : Finset ι) (i : ℕ) : faceFiltration f P M hf ∅ p S i = ⊥

The face filtration of the empty set vanishes.

theorem TauCeti.Huber.NoetherianCech.faceFiltration_antitone {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p : ℕ) (S : Finset ι) : Antitone (faceFiltration f P M hf N p S)

The subgroups faceFiltration decrease.

theorem TauCeti.Huber.NoetherianCech.hasBasis_nhds_zero_faceFiltration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) {N : Set M} (hN : N.Finite) (hspan : Submodule.span B N = ⊤) (p : ℕ) (S : Finset ι) : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (i : ℕ) => ↑(faceFiltration f P M hf N p S i)

The face filtration is a basis of neighbourhoods of zero. If N is a finite set generating M, the subgroups Iⁱ · C[F_p / f_S] · N form a basis of neighbourhoods of zero in M_{f_S} for its natural topology over B(F_p / f_S).

noncomputable def TauCeti.Huber.NoetherianCech.filtration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p i : ℕ) : AddSubgroup (cechLocalizationTerm M f p)

Huber's filtration K_i^p of the term of degree p: for a set N ⊆ M, the product over the faces S, |S| = p + 1, of the subgroups Iⁱ · C[F_p / f_S] · N of M_{f_S}.

@[simp]

theorem TauCeti.Huber.NoetherianCech.mem_filtration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p i : ℕ) (x : cechLocalizationTerm M f p) : x ∈ filtration f P M hf N p i ↔ ∀ (S : { S : Finset ι // S.card = p + 1 }), x S ∈ faceFiltration f P M hf N p (↑S) i

An element lies in the filtration exactly when each of its components lies in the face filtration.

@[simp]

theorem TauCeti.Huber.NoetherianCech.filtration_empty {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (p i : ℕ) : filtration f P M hf ∅ p i = ⊥

The filtration of the empty set vanishes.

theorem TauCeti.Huber.NoetherianCech.filtration_antitone {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] (hf : Ideal.span (Set.range f) = ⊤) (N : Set M) (p : ℕ) : Antitone (filtration f P M hf N p)

The filtration is decreasing.

theorem TauCeti.Huber.NoetherianCech.hasBasis_nhds_zero_filtration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] [Finite ι] (hf : Ideal.span (Set.range f) = ⊤) {N : Set M} (hN : N.Finite) (hspan : Submodule.span B N = ⊤) (p : ℕ) : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (i : ℕ) => ↑(filtration f P M hf N p i)

The filtration is a basis of neighbourhoods of zero: the case of nonnegative degree of Huber94 §2, (1.3.1)(ii), with the subgroups K_i^p read off the charts of (1.2)(ii). If ι is finite and N is a finite set generating M, the subgroups K_i^p form a basis of neighbourhoods of zero for termTopology.

theorem TauCeti.Huber.NoetherianCech.hasBasis_uniformity_filtration {B : Type u_1} [CommRing B] {ι : Type u_2} (f : ι → B) [TopologicalSpace B] [IsTopologicalRing B] (P : PairOfDefinition B) (M : Type u_3) [AddCommGroup M] [Module B M] [Finite ι] (hf : Ideal.span (Set.range f) = ⊤) {N : Set M} (hN : N.Finite) (hspan : Submodule.span B N = ⊤) (p : ℕ) : (uniformity (cechLocalizationTerm M f p)).HasBasis (fun (x : ℕ) => True) fun (i : ℕ) => {xy : cechLocalizationTerm M f p × cechLocalizationTerm M f p | xy.2 - xy.1 ∈ filtration f P M hf N p i}

The filtration is a basis of entourages: if ι is finite and N is a finite set generating M, the sets {(x, y) | y - x ∈ K_i^p} form a basis of the uniformity termUniformSpace.