Foundations of adic spaces, part II — morphisms and analytification

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremExactness 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.

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

Lean

Formalized in Tau Ceti as TauCeti.cechComplexLocalization_exact.

Sources

• Tau Ceti documentation: TauCeti.cechComplexLocalization_exact
• Source of TauCeti.cechComplexLocalization_exact in TauCeti/Algebra/Module/LocalizedModule/Cech.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.cechComplexLocalization_exact

TheoremCompletion preserves strict exact sequences#

If M → N → P is exact with strict maps, where M is a first-countable nonarchimedean group and N is a nonarchimedean group, then the sequence of separated completions is exact. Its maps are again strict by AddMonoidHom.isStrictMap_completion when M and N are first countable. No Hausdorff hypothesis is needed.

AddMonoidHom.exact_completion.{u_3, u_4, u_5} {M : Type u_3} {N : Type u_4} {P : Type u_5}
  [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [NonarchimedeanAddGroup M]
  [(nhds 0).IsCountablyGenerated] [AddCommGroup N] [UniformSpace N] [IsUniformAddGroup N]
  [NonarchimedeanAddGroup N] [AddGroup P] [UniformSpace P] [IsUniformAddGroup P] {f : M →+ N}
  {g : N →+ P} (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g)
  (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(f.completion ⋯) ⇑(g.completion ⋯)

Lean

Formalized in Tau Ceti as AddMonoidHom.exact_completion.

Sources

• Tau Ceti documentation: AddMonoidHom.exact_completion
• Source of AddMonoidHom.exact_completion in TauCeti/Topology/Algebra/Nonarchimedean/Completion/Strict.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanAddMonoidHom.exact_completion

TheoremLinear maps of finite modules over a Huber ring with a noetherian ring of definition are strict (Huber, Lemma 2.3(i))#

If A₀ is noetherian, every A-linear map between finitely generated A-modules with their natural topologies is continuous and open onto its image.

TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing.{u_1, u_2, u_3} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M]
  [_root_.Module A M] [Module.Finite A M] [TopologicalSpace M] [IsModuleTopology A M] {N : Type u_3}
  [AddCommGroup N] [_root_.Module A N] [Module.Finite A N] [TopologicalSpace N]
  [IsModuleTopology A N] (P : TauCeti.Huber.PairOfDefinition A)
  [IsNoetherianRing ↥P.ringOfDefinition] (u : M →ₗ[A] N) : Topology.IsStrictMap ⇑u

Lean

Formalized in Tau Ceti as TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing.

Sources

• Tau Ceti documentation: TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing
• Source of TauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing in TauCeti/RingTheory/Huber/ModuleTopology/Strict.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.PairOfDefinition.isStrictMap_of_isNoetherianRing

Uses 1

Proof usesArtin–Rees for a finitely generated submodule

TheoremSubmodules of finite modules over a complete Huber ring with a noetherian ring of definition are closed (Huber, Lemma 2.3(ii))#

If A is complete and Hausdorff with a noetherian ring of definition, every A-submodule of a finite A-module is closed in its natural topology.

TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing.{u_1, u_2} {A : Type u_1} [CommRing A]
  {M : Type u_2} [AddCommGroup M] [_root_.Module A M] [UniformSpace A] [IsUniformAddGroup A]
  [CompleteSpace A] [T0Space A] [IsTopologicalRing A] [Module.Finite A M] [TopologicalSpace M]
  [IsModuleTopology A M] (P : TauCeti.Huber.PairOfDefinition A)
  [IsNoetherianRing ↥P.ringOfDefinition] (N : Submodule A M) : IsClosed ↑N

Lean

Formalized in Tau Ceti as TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing.

Sources

• Tau Ceti documentation: TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing
• Source of TauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing in TauCeti/RingTheory/Huber/ModuleTopology/Complete.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.PairOfDefinition.isClosed_of_isNoetherianRing

Used by 1

Used byCompletion of a finite module is base change to the completed ring (Huber, Lemma 2.3(iii))

TheoremCompletion of a finite module is base change to the completed ring (Huber, Lemma 2.3(iii))#

If A is a Huber ring with a noetherian ring of definition and M is a finitely generated A-module with its natural topology, the canonical map  ⊗[A] M → M̂ is bijective.

TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective.{u_1, u_2} {A : Type u_1} [CommRing A]
  [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {M : Type u_2} [AddCommGroup M]
  [_root_.Module A M] [Module.Finite A M] [UniformSpace M] [IsUniformAddGroup M]
  [IsModuleTopology A M] [UniformContinuousConstSMul A M] (P : TauCeti.Huber.PairOfDefinition A)
  [IsNoetherianRing ↥P.ringOfDefinition] :
  Function.Bijective ⇑(UniformSpace.Completion.ofTensorProduct A M)

Lean

Formalized in Tau Ceti as TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective.

Sources

• Tau Ceti documentation: TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective
• Source of TauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective in TauCeti/RingTheory/Huber/ModuleTopology/Completion.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.PairOfDefinition.ofTensorProduct_bijective

Uses 2

Proof usesNoetherianity of complete rings · Submodules of finite modules over a complete Huber ring with a noetherian ring of definition are closed (Huber, Lemma 2.3(ii))

TheoremThe blowup of a finitely generated submodule is proper#

If F is finite, the structure morphism Proj R(J) ⟶ Spec C is proper.

TauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec.{u} (C : Type u) {B : Type u} [CommRing C]
  [CommRing B] [Algebra C B] {F : Set B} (hF : F.Finite) :
  AlgebraicGeometry.IsProper (TauCeti.AlgebraicGeometry.submoduleBlowup.toSpec C F)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec
• Source of TauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec in TauCeti/AlgebraicGeometry/Blowup/Submodule/Basic.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.AlgebraicGeometry.submoduleBlowup.isProper_toSpec

DefinitionThe affine charts of the blowup of a submodule#

For a nonempty finite subset S ⊆ F with product t, the standard open D₊(t T^{#S}) of Proj R(J) is isomorphic to Spec C[F/S], the spectrum of the C-subalgebra of B_t generated by the fractions f/f' with f ∈ F and f' ∈ S. It is Mathlib's Proj.basicOpenIsoSpec followed by the spectrum of awayEquivFractionSubalgebra.

TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec.{u} (C : Type u) {B : Type u}
  [CommRing C] [CommRing B] [Algebra C B] {F : Set B} {S : Finset B} (L : Type u) [CommRing L]
  [Algebra C L] [Algebra B L] [IsScalarTower C B L] [IsLocalization.Away (∏ g ∈ S, g) L]
  (hS : ↑S ⊆ F) (hS₀ : S.Nonempty) :
  ↑(AlgebraicGeometry.Proj.basicOpen (TauCeti.AlgebraicGeometry.submoduleBlowup.gradedRing C F)
        (TauCeti.AlgebraicGeometry.submoduleBlowup.monomialProd C hS)) ≅
    AlgebraicGeometry.Spec ↧↥(TauCeti.AlgebraicGeometry.submoduleBlowup.fractionSubalgebra C F S L)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec
• Source of TauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec in TauCeti/AlgebraicGeometry/Blowup/Submodule/Basic.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.AlgebraicGeometry.submoduleBlowup.basicOpenIsoSpec

TheoremNoetherianity of complete rings#

A ring that is I-adically complete for a finitely generated ideal I is Noetherian as soon as R ⧸ I is Noetherian.

Ideal.isNoetherianRing_of_isAdicComplete.{u_1} {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I.FG)
  [IsAdicComplete I R] [IsNoetherianRing (R ⧸ I)] : IsNoetherianRing R

Lean

Formalized in Tau Ceti as Ideal.isNoetherianRing_of_isAdicComplete.

Sources

• Tau Ceti documentation: Ideal.isNoetherianRing_of_isAdicComplete
• Source of Ideal.isNoetherianRing_of_isAdicComplete in TauCeti/RingTheory/AdicCompletion/Noetherian.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanIdeal.isNoetherianRing_of_isAdicComplete

Used by 1

Used byCompletion of a finite module is base change to the completed ring (Huber, Lemma 2.3(iii))

ClassTauCeti.Huber.IsNoetherianType#

A Huber ring is of noetherian type if it has a noetherian ring of definition, or if it is a strongly noetherian Tate ring.

TauCeti.Huber.IsNoetherianType.{u_1} (A : Type u_1) [CommRing A] [TopologicalSpace A]
  [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] : Prop

Lean

Formalized in Tau Ceti as TauCeti.Huber.IsNoetherianType.

Sources

• Tau Ceti documentation: TauCeti.Huber.IsNoetherianType
• Source of TauCeti.Huber.IsNoetherianType in TauCeti/RingTheory/Huber/NoetherianType/Basic.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.IsNoetherianType

DefinitionHuber'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}.

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

Lean

Formalized in Tau Ceti as TauCeti.Huber.NoetherianCech.filtration.

Sources

• Tau Ceti documentation: TauCeti.Huber.NoetherianCech.filtration
• Source of TauCeti.Huber.NoetherianCech.filtration in TauCeti/RingTheory/Huber/NoetherianCech/Topology.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.NoetherianCech.filtration

AbbreviationTauCeti.Huber.NoetherianCech.completedTerm#

The separated completion of the degree-p term of the rational-localization Čech complex, for the product of the natural module topologies on its faces.

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

Lean

Formalized in Tau Ceti as TauCeti.Huber.NoetherianCech.completedTerm.

Sources

• Tau Ceti documentation: TauCeti.Huber.NoetherianCech.completedTerm
• Source of TauCeti.Huber.NoetherianCech.completedTerm in TauCeti/RingTheory/Huber/NoetherianCech/Completion.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.NoetherianCech.completedTerm

DefinitionThe tensor topology on B ⊗[A] C, for adic structure maps A → B and A → C#

for any compatible pairs of definition (A₀, I), (B₀, I B₀) and (C₀, I C₀), its neighbourhoods of zero are generated by the images of Iⁿ F, where F is the image of B₀ ⊗[A₀] C₀ (TauCeti.Huber.hasBasis_tensorTopology). It is not an instance, since B ⊗[A] C may carry other topologies.

TauCeti.Huber.tensorTopology.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (C : Type u_3)
  [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] [TopologicalSpace A]
  [TopologicalSpace B] [TopologicalSpace C] [IsTopologicalRing A] [IsTopologicalRing B]
  [IsTopologicalRing C] [TauCeti.Huber.IsAdicHom (algebraMap A B)]
  [TauCeti.Huber.IsAdicHom (algebraMap A C)] : TopologicalSpace (TensorProduct A B C)

Lean

Formalized in Tau Ceti as TauCeti.Huber.tensorTopology.

Sources

• Tau Ceti documentation: TauCeti.Huber.tensorTopology
• Source of TauCeti.Huber.tensorTopology in TauCeti/RingTheory/Huber/TensorProduct/Topology.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part II — morphisms and analytification

LeanTauCeti.Huber.tensorTopology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.