87.21 Morphisms and continuous… to 87.28 Restricted power series

Section87.21 Morphisms and continuous ring maps #

Section 87.21 of the Stacks Project, Tag 0ANA. 18 tags here are carried by 58 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ANB, a lemma

Tag 0ANB in the Stacks Project.

TopologicalRing.completionOver_isCountablyGenerated_nhds_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 545. The attribute's comment: “completion_in_sub_countable”.

Completion over a weakly admissible ring with a countable fundamental system of open ideals again has a countable fundamental system of open ideals.

public lemma completionOver_isCountablyGenerated_nhds_zero
    {B A : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] (f : B →+* A)
    (hB : TopologicalRing.IsWeaklyAdmissible B)
    (hBcount : (nhds (0 : B)).IsCountablyGenerated) :
    (nhds (0 : CompletionOver f)).IsCountablyGenerated

TopologicalRing.completionOver_isCountablyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 569. The attribute's comment: “completion_in_sub_cic”.

Completion over a countably admissible ring is again countably admissible.

public theorem completionOver_isCountablyAdmissible
    {B A : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] (f : B →+* A)
    (hB : IsCountablyAdmissible B) :
    IsCountablyAdmissible (CompletionOver f)

TopologicalRing.completionOver_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 589. The attribute's comment: “completion_in_sub_weakly_adic”.

Completion relative to a weakly admissible, weakly adic ring is weakly adic.

public theorem completionOver_isWeaklyAdic
    {B A : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] (f : B →+* A)
    (hB : TopologicalRing.IsWeaklyAdmissible B) [TopologicalRing.IsWeaklyAdic B] :
    TopologicalRing.IsWeaklyAdic (CompletionOver f)

TopologicalRing.completionOver_exists_fg_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOver.lean, line 609. The attribute's comment: “completion_in_sub_adic_star”.

Completion relative to a weakly admissible adic-star ring is again adic-star: its topology is defined by a finitely generated ideal.

public theorem completionOver_exists_fg_isAdic
    {B A : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A]
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyAdmissible B)
    (hB_adicStar : ∃ I : Ideal B, I.FG ∧ _root_.IsAdic I) :
    ∃ J : Ideal (CompletionOver f), J.FG ∧ _root_.IsAdic J

TopologicalRing.completionOver_isNoetherianAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionOverNoetherian.lean, line 69. The attribute's comment: “completion_in_sub_noetherian”.

Stacks 0ANB (5). Let B be an adic Noetherian topological ring and let f : B →+* A be a ring map, A carrying no topology. If A is Noetherian then the completion of A over B, the limit of the rings A ⧸ JA over the weak ideals of definition J of B, is again an adic Noetherian topological ring.

The topology of the completion is adic by the clause of this lemma for WAdm^{adic*}, which applies because an ideal of definition of the Noetherian ring B is finitely generated. The completion is then the IA-adic completion of A for I an ideal of definition of B, hence Noetherian by Tag 0316.

public theorem completionOver_isNoetherianAdic {B : Type u} {A : Type v}
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing A] (f : B →+* A) (hB : IsNoetherianAdic B) (hA : IsNoetherianRing A) :
    IsNoetherianAdic (CompletionOver f)

Tag 0CBA, a situation

Tag 0CBA in the Stacks Project.

TopologicalRing.LocalizationDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 53. The attribute's comment: “localization diagram”.

A commutative localization diagram of countably indexed weakly admissible rings, with étale horizontal maps and continuous vertical maps.

public structure LocalizationDiagram
    (A B A' B' : Type u)
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing A'] [CommRing B']

TopologicalRing.PropertyIsLocal, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 146. The attribute's comment: “local property”.

A property of morphisms of countably indexed weakly admissible rings is local if it ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets. The optional subclass parameter restricts all four corners of each diagram and every ring in the finite-product family.

public structure PropertyIsLocal
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A],
      (B →+* A) → Prop)
    (C : ∀ (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
      [IsLinearTopology R R], Prop := IsCountablyWeaklyAdmissible) : Prop

Tag 0ANG, a lemma

Tag 0ANG in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalProperty.lean, line 194. The attribute's comment: “condition (1) implies condition (2), with Stacks 0AJ3 as a hypothesis”.

Stacks 0ANG, condition (1) implies condition (2). If P holds on every affine étale diagram over f, then the atlas of the target and the atlases of the fibre products of its members with the source witness condition (2).

The hypothesis hpb is the assertion of Stacks 0AJ3 that the fibre product of the chart V ⟶ Y with f is a formal algebraic space; the library does not yet carry Stacks 0AJ3, so it is carried here as a hypothesis for the fibre products the statement needs.

theorem hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hpb : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
      IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS C P f) :
    HasPropertyAfterTargetCover B S hS C P f

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalProperty.lean, line 274. The attribute's comment: “condition (3) implies condition (1), with the refinement of the covering (Stacks 0AJ2 and quasi-compactness of an affine formal algebraic space) and the locality axioms of Situation 0CBA read through Stacks 0AN8 and Stacks 0AN9 carried as hypotheses”.

Stacks 0ANG, condition (3) implies condition (1). If P holds on an affine étale covering of the source of f, whose members factor through affine formal algebraic spaces representable étale over the target, then P holds on every affine étale diagram over f.

Given a diagram as in condition (1), the covering is refined against it by href; axiom (1) of locality carries P from the members of the covering to the refined charts, and axioms (2) and (3) descend it along the finite covering of the chart U₀ so obtained.

theorem hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hasc : ChartPropertyAscendsAlongAffineEtale B S hS C P)
    (hdesc : ChartPropertyDescendsAlongFiniteAffineEtaleCover B S hS C P)
    (href : HasEtaleRefinementOfSourceCover B S hS f)
    (hf : HasPropertyAfterSourceCover B S hS C P f) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS C P f

AlgebraicGeometry.FormalSpace.hasProperty_tfae_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCountablyIndexed.lean, line 161.

Stacks 0ANG. Let S be a scheme and let f : X ⟶ Y be a morphism of locally countably indexed formal algebraic spaces over S. Let P be a local property of morphisms of WAdm^count, the countably indexed weakly admissible topological rings (Situation 0CBA: P is invariant under isomorphism of source and target, and satisfies the three axioms 0AND, 0ANE and 0ANF of TopologicalRing.PropertyIsLocal). The following are equivalent:

for every commutative diagram with U and V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a morphism of WAdm^count with property P;

there is a covering {Vⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Uᵢ ⟶ Vⱼ ×_Y X} as in Definition 0AIM such that each Uᵢ ⟶ Vⱼ corresponds to a morphism of WAdm^count with property P;

there are a covering {Uᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Uᵢ ⟶ Vᵢ ⟶ Y where Vᵢ is an affine formal algebraic space, Vᵢ ⟶ Y is representable by algebraic spaces and étale, and Uᵢ ⟶ Vᵢ corresponds to a morphism of WAdm^count with property P.

"Corresponds to a morphism of WAdm^count with property P" is AlgebraicGeometry.FormalSpace.HasPropertyOnAffineChartMap: P holds on every continuous homomorphism presenting the morphism of formal spectra through rings of WAdm^count.

This is AlgebraicGeometry.FormalSpace.hasProperty_tfae_isCountablyWeaklyAdmissible_of_etale at the étale case of Stacks 0AJH, AlgebraicGeometry.FormalSpace.representableEtaleOverAffineIsFormal.

theorem hasProperty_tfae_of_isLocallyCountablyIndexed
    (hP : TopologicalRing.PropertyIsLocal P TopologicalRing.IsCountablyWeaklyAdmissible)
    (hsrc : PropertyIsInvariantUnderSourceIso.{u} TopologicalRing.IsCountablyWeaklyAdmissible P)
    (htgt : PropertyIsInvariantUnderTargetIsoOn.{u} TopologicalRing.IsCountablyWeaklyAdmissible P)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y) :
    List.TFAE
      [ HasPropertyOnEveryAffineEtaleDiagram B S hS
          TopologicalRing.IsCountablyWeaklyAdmissible P f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f ]

AlgebraicGeometry.FormalSpace.hasProperty_tfae_of_isLocallyCountablyIndexed_of_isLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCountablyIndexedIsLocal.lean, line 69. The attribute's comment: “the equivalence of conditions (1), (2) and (3) for a morphism of locally countably indexed formal algebraic spaces and a local property of WAdm^count in the sense of Situation 0CBA (invariance under isomorphism of source and target, and the axioms 0AND, 0ANE, 0ANF)”.

Stacks 0ANG. Let S be a scheme and let f : X ⟶ Y be a morphism of locally countably indexed formal algebraic spaces over S. Let P be a local property of morphisms of WAdm^count in the sense of Situation 0CBA: invariant under isomorphism of source and target in WAdm^count, and satisfying the axioms 0AND, 0ANE and 0ANF; this is TopologicalRing.PropertyIsLocal' P TopologicalRing.IsCountablyWeaklyAdmissible. The following are equivalent:

for every commutative diagram with U and V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a morphism of WAdm^count with property P;

there is a covering {Vⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Uᵢ ⟶ Vⱼ ×_Y X} as in Definition 0AIM such that each Uᵢ ⟶ Vⱼ corresponds to a morphism of WAdm^count with property P;

there are a covering {Uᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Uᵢ ⟶ Vᵢ ⟶ Y where Vᵢ is an affine formal algebraic space, Vᵢ ⟶ Y is representable by algebraic spaces and étale, and Uᵢ ⟶ Vᵢ corresponds to a morphism of WAdm^count with property P.

This is AlgebraicGeometry.FormalSpace.hasProperty_tfae_of_isLocallyCountablyIndexed, whose invariance under isomorphism of sources and of targets is derived from the invariance clause of Situation 0CBA.

theorem hasProperty_tfae_of_isLocallyCountablyIndexed_of_isLocal
    (hP : TopologicalRing.PropertyIsLocal' P TopologicalRing.IsCountablyWeaklyAdmissible)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y) :
    List.TFAE
      [ HasPropertyOnEveryAffineEtaleDiagram B S hS
          TopologicalRing.IsCountablyWeaklyAdmissible P f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f ]

AlgebraicGeometry.FormalSpace.hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram_of_formal', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RepresentableSourceRefined.lean, line 52. The attribute's comment: “condition (1) implies condition (2)”.

Stacks 0ANG, condition (1) implies condition (2). If P holds on every affine étale diagram over a morphism f : X ⟶ Y of formal algebraic spaces, then the atlas of the target and the atlases of the fibre products of its members with the source witness condition (2).

The fibre products are formal algebraic spaces by Stacks 0AJ3, which this library proves outright for a base which is a formal algebraic space: AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_chart_of_isFormalAlgebraicSpace asks only that X, Y and the chart V be formal algebraic spaces, which hX, hY and the atlas of Y give. It therefore supplies the hypothesis hpb of AlgebraicGeometry.FormalSpace.hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram with no standing hypothesis of its own, and nothing is assumed here beyond the setting of the tag.

theorem hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram_of_formal'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS C P f) :
    HasPropertyAfterTargetCover B S hS C P f

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SourceCoverImpliesEveryDiagram.lean, line 428. The attribute's comment: “condition (3) implies condition (1), for a morphism of locally countably indexed formal algebraic spaces and a local property of WAdm^count, as the source states it: hP and hPiso together are Situation 0CBA's notion of a local property”.

Stacks 0ANG, condition (3) implies condition (1). Let f : X ⟶ Y be a morphism of locally countably indexed formal algebraic spaces over S and let P be a local property of morphisms of WAdmᶜᵒᵘⁿᵗ (Situation 0CBA: hP for the three axioms and hPiso for "invariant under isomorphism of source and target in this category"). If there are an affine étale covering {Uᵢ ⟶ X} as in Definition 0AIM and factorizations Uᵢ ⟶ Vᵢ ⟶ Y through affine formal algebraic spaces representable étale over Y with P on each Uᵢ ⟶ Vᵢ, then for every commutative square with affine formal algebraic spaces U, V and representable étale maps U ⟶ X, V ⟶ Y, the morphism U ⟶ V has P.

This is hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_hasChartsPresentedByClass at the class WAdmᶜᵒᵘⁿᵗ, whose three closure conditions are theorems: membership of the class is weak admissibility with a countable fundamental system of open ideals by definition, closure under completion along an étale ring map is two clauses of Stacks 0ANB, and closure under isomorphism is TopologicalRing.isCountablyWeaklyAdmissible_of_ringEquiv. The charts of X and Y are presented by rings of the class because X and Y are locally countably indexed.

theorem hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_isLocallyCountablyIndexed
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.PropertyIsLocal P TopologicalRing.IsCountablyWeaklyAdmissible)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsCountablyWeaklyAdmissible B →
      TopologicalRing.IsCountablyWeaklyAdmissible A →
      TopologicalRing.IsCountablyWeaklyAdmissible B' →
      TopologicalRing.IsCountablyWeaklyAdmissible A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hf : HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
      f

AlgebraicGeometry.FormalSpace.hasPropertyAfterSourceCover_of_afterTargetCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautMorphismRepresentability.lean, line 131. The attribute's comment: “condition (2) implies condition (3)”.

Stacks 0ANG, condition (2) implies condition (3). A covering of the target together with coverings of the fibre products of its members with the source compose to a covering of the source whose members factor through the chart of the target they came from, by the map condition (2) puts P on.

theorem hasPropertyAfterSourceCover_of_afterTargetCover {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : HasPropertyAfterTargetCover B S hS C P f) :
    HasPropertyAfterSourceCover B S hS C P f

Tag 0ANH, a remark

Tag 0ANH in the Stacks Project.

TopologicalRing.propertyIsLocalAdicStar_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarChartCriteria.lean, line 142. The attribute's comment: “the first half, the definition of a local property of morphisms of WAdm^{adic}, with the three axioms of Situation 0CBA quantified over the diagrams and finite families of WAdm^{adic} exactly as in the source”.

The first half of Stacks 0ANH, in the source's words. A property P of morphisms of WAdm^{adic*} is a local property, TopologicalRing.PropertyIsLocalAdicStar P, exactly when the three axioms of Situation 0CBA hold for morphisms of WAdm^{adic*}:

for every diagram of Situation 0CBA with A and B in WAdm^{adic*}, P(φ) ⟹ P(φ');

for every such diagram with A → A' faithfully flat, P(φ') ⟹ P(φ);

if P(B → Aᵢ) for finitely many Aᵢ of WAdm^{adic*}, then P(B → ∏ᵢ Aᵢ).

TopologicalRing.PropertyIsLocal asks in addition that the two completions (A')^∧ and (B')^∧ of a diagram be in WAdm^{adic*}, and that the rings of axiom (3) be weakly admissible with a countable fundamental system of neighbourhoods of zero. Neither is an extra condition: the completions are in WAdm^{adic*} by Stacks 0ANB (4), AlgebraicGeometry.FormalSpace.classIsStableUnderEtaleCompletion_isAdicStar, and every ring of WAdm^{adic*} is weakly admissible and countably indexed. This equivalence records that TopologicalRing.PropertyIsLocalAdicStar is the source's notion.

theorem propertyIsLocalAdicStar_iff
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) :
    PropertyIsLocalAdicStar.{u} P ↔
      (∀ {A B A' B' : Type u}
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
        [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
        [CommRing A'] [CommRing B'] (D : LocalizationDiagram A B A' B'),
        IsAdicStar A → IsAdicStar B → P D.map → P D.completedMap) ∧
      (∀ {A B A' B' : Type u}
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
        [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
        [CommRing A'] [CommRing B'] (D : LocalizationDiagram A B A' B'),
        IsAdicStar A → IsAdicStar B → D.toA'.FaithfullyFlat → P D.completedMap → P D.map) ∧
      (∀ {B : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [IsLinearTopology B B] {ι : Type u} [Fintype ι] (A : ι → Type u)
        [∀ i, CommRing (A i)] [∀ i, TopologicalSpace (A i)]
        [∀ i, IsTopologicalRing (A i)] [∀ i, IsLinearTopology (A i) (A i)]
        (f : ∀ i, B →+* A i), (∀ i, Continuous (f i)) → IsAdicStar B →
        (∀ i, IsAdicStar (A i)) → (∀ i, P (f i)) → P (RingHom.pi f))

AlgebraicGeometry.FormalSpace.hasProperty_tfae_isAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarChartCriteria.lean, line 297. The attribute's comment: “the second half: the variant of Stacks 0ANG for morphisms between locally adic formal algebraic spaces over S, at a local property of morphisms of WAdm^{adic} invariant under isomorphism of source and target (the standing hypothesis of Situation 0CBA)”.

The second half of Stacks 0ANH: the variant of Stacks 0ANG for morphisms between locally adic* formal algebraic spaces. Let f : X ⟶ Y be a morphism of locally adic* formal algebraic spaces over S and let P be a local property of morphisms of WAdm^{adic*} (TopologicalRing.PropertyIsLocalAdicStar P), invariant under isomorphism of source and target as Situation 0CBA stipulates. The following are equivalent:

for every commutative diagram with U, V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a morphism of WAdm^{adic*} with property P;

there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM such that each Xⱼᵢ ⟶ Yⱼ corresponds to a morphism of WAdm^{adic*} with property P;

there are a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y with Yᵢ an affine formal algebraic space, Yᵢ ⟶ Y representable by algebraic spaces and étale, and Xᵢ ⟶ Yᵢ corresponding to a morphism of WAdm^{adic*} with property P.

This is AlgebraicGeometry.FormalSpace.hasProperty_tfae_isAdicStar_of_inputs with the étale case of Stacks 0AJH supplied by AlgebraicGeometry.FormalSpace.representableEtaleOverAffineIsFormal.

theorem hasProperty_tfae_isAdicStar
    (hP : TopologicalRing.PropertyIsLocalAdicStar.{u} P)
    (hsrc : PropertyIsInvariantUnderSourceIso.{u} TopologicalRing.IsAdicStar P)
    (htgt : PropertyIsInvariantUnderTargetIsoOn.{u} TopologicalRing.IsAdicStar P)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y) :
    List.TFAE
      [ HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P f ]

TopologicalRing.propertyIsLocalAdicStarUpToIso_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarChartCriteriaUpToIso.lean, line 83. The attribute's comment: “the first half, the definition of a local property of morphisms of WAdm^{adic}, in the source's words: axioms (1), (2), (3) of Situation 0CBA quantified over the diagrams and finite families of WAdm^{adic}, the completed corners being any limits”.

The first half of Stacks 0ANH, in the source's words. A property P of morphisms of WAdm^{adic*} is a local property, TopologicalRing.PropertyIsLocalAdicStarUpToIso P, exactly when the three axioms of Situation 0CBA hold for morphisms of WAdm^{adic*}:

for every diagram of Situation 0CBA with A and B in WAdm^{adic*}, and any rings Â, B̂ isomorphic to the limits lim A'/IA', lim B'/JB', P(φ) ⟹ P(φ');

for every such diagram with A → A' faithfully flat, P(φ') ⟹ P(φ);

if P(B → Aᵢ) for finitely many Aᵢ of WAdm^{adic*}, then P(B → ∏ᵢ Aᵢ).

The definition asks in addition that Â and B̂ be in WAdm^{adic*}, and that the rings of the third axiom be weakly admissible and countably indexed. Neither is an extra condition. The completions are in WAdm^{adic*} by Stacks 0ANB (4), AlgebraicGeometry.FormalSpace.classIsStableUnderEtaleCompletion_isAdicStar, and so are Â and B̂, which are isomorphic to them. Every ring of WAdm^{adic*} is weakly admissible and countably indexed.

theorem propertyIsLocalAdicStarUpToIso_iff
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) :
    PropertyIsLocalAdicStarUpToIso.{u} P ↔
      (∀ {A B A' B' Ahat Bhat : Type u}
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
        [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
        [CommRing A'] [CommRing B']
        [CommRing Ahat] [TopologicalSpace Ahat] [IsTopologicalRing Ahat]
        [IsLinearTopology Ahat Ahat]
        [CommRing Bhat] [TopologicalSpace Bhat] [IsTopologicalRing Bhat]
        [IsLinearTopology Bhat Bhat]
        (D : LocalizationDiagram A B A' B')
        (eA : CompletionOver D.toA' ≃+* Ahat) (eB : CompletionOver D.toB' ≃+* Bhat),
        Continuous eA → Continuous eA.symm → Continuous eB → Continuous eB.symm →
        IsAdicStar A → IsAdicStar B → P D.map →
          P ((eA.toRingHom.comp D.completedMap).comp eB.symm.toRingHom)) ∧
      (∀ {A B A' B' Ahat Bhat : Type u}
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
        [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
        [CommRing A'] [CommRing B']
        [CommRing Ahat] [TopologicalSpace Ahat] [IsTopologicalRing Ahat]
        [IsLinearTopology Ahat Ahat]
        [CommRing Bhat] [TopologicalSpace Bhat] [IsTopologicalRing Bhat]
        [IsLinearTopology Bhat Bhat]
        (D : LocalizationDiagram A B A' B')
        (eA : CompletionOver D.toA' ≃+* Ahat) (eB : CompletionOver D.toB' ≃+* Bhat),
        Continuous eA → Continuous eA.symm → Continuous eB → Continuous eB.symm →
        IsAdicStar A → IsAdicStar B → D.toA'.FaithfullyFlat →
          P ((eA.toRingHom.comp D.completedMap).comp eB.symm.toRingHom) → P D.map) ∧
      (∀ {B : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [IsLinearTopology B B] {ι : Type u} [Fintype ι] (A : ι → Type u)
        [∀ i, CommRing (A i)] [∀ i, TopologicalSpace (A i)]
        [∀ i, IsTopologicalRing (A i)] [∀ i, IsLinearTopology (A i) (A i)]
        (f : ∀ i, B →+* A i), (∀ i, Continuous (f i)) → IsAdicStar B →
        (∀ i, IsAdicStar (A i)) → (∀ i, P (f i)) → P (RingHom.pi f))

AlgebraicGeometry.FormalSpace.hasProperty_tfae_of_propertyIsLocalAdicStarUpToIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarChartCriteriaUpToIso.lean, line 170. The attribute's comment: “the second half: the variant of Stacks 0ANG for morphisms between locally adic formal algebraic spaces over S, at any local property of morphisms of WAdm^{adic}”.

The second half of Stacks 0ANH: the variant of Stacks 0ANG for morphisms between locally adic* formal algebraic spaces. Let f : X ⟶ Y be a morphism of locally adic* formal algebraic spaces over S and let P be a local property of morphisms of WAdm^{adic*} (TopologicalRing.PropertyIsLocalAdicStarUpToIso P). The following are equivalent:

for every commutative diagram with U, V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a morphism of WAdm^{adic*} with property P;

there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM such that each Xⱼᵢ ⟶ Yⱼ corresponds to a morphism of WAdm^{adic*} with property P;

there are a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y with Yᵢ an affine formal algebraic space, Yᵢ ⟶ Y representable by algebraic spaces and étale, and Xᵢ ⟶ Yᵢ corresponding to a morphism of WAdm^{adic*} with property P.

There is no hypothesis on P beyond locality. Its invariance under isomorphism of source and target, which the proof of Stacks 0ANG uses, is derived from axiom (1) of Situation 0CBA by propertyIsInvariantUnderSourceIso_of_propertyIsLocalAdicStarUpToIso and propertyIsInvariantUnderTargetIsoOn_of_propertyIsLocalAdicStarUpToIso. The equivalence is then AlgebraicGeometry.FormalSpace.hasProperty_tfae_isAdicStar.

theorem hasProperty_tfae_of_propertyIsLocalAdicStarUpToIso
    (hP : TopologicalRing.PropertyIsLocalAdicStarUpToIso.{u} P)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y) :
    List.TFAE
      [ HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P f ]

AlgebraicGeometry.FormalSpace.propertyIsInvariantUnderSourceIso_of_propertyIsLocalAdicStarUpToIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyUpToIsoInvariance.lean, line 184. The attribute's comment: “a local property of morphisms of WAdm^{adic*} is invariant under isomorphism of sources, by axiom (1), an isomorphism being etale; used by the variant of 0ANG”.

A local property of morphisms of WAdm^{adic*} is invariant under isomorphism of sources. The variant of Stacks 0ANG in Stacks 0ANH uses this, and it follows from axiom (1) of Situation 0CBA.

theorem propertyIsInvariantUnderSourceIso_of_propertyIsLocalAdicStarUpToIso
    (hP : TopologicalRing.PropertyIsLocalAdicStarUpToIso.{u} P) :
    PropertyIsInvariantUnderSourceIso.{u} TopologicalRing.IsAdicStar P

AlgebraicGeometry.FormalSpace.propertyIsInvariantUnderTargetIsoOn_of_propertyIsLocalAdicStarUpToIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyUpToIsoInvariance.lean, line 195. The attribute's comment: “a local property of morphisms of WAdm^{adic*} is invariant under isomorphism of targets, by axiom (1), an isomorphism being etale; used by the variant of 0ANG”.

A local property of morphisms of WAdm^{adic*} is invariant under isomorphism of targets. The variant of Stacks 0ANG in Stacks 0ANH uses this, and it follows from axiom (1) of Situation 0CBA.

theorem propertyIsInvariantUnderTargetIsoOn_of_propertyIsLocalAdicStarUpToIso
    (hP : TopologicalRing.PropertyIsLocalAdicStarUpToIso.{u} P) :
    PropertyIsInvariantUnderTargetIsoOn.{u} TopologicalRing.IsAdicStar P

TopologicalRing.AdicStarPropertyIsLocal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 178. The attribute's comment: “adic_star_local_property”.

A property of morphisms of weakly admissible adic-star rings is local when it satisfies the three locality axioms of TopologicalRing.PropertyIsLocal within that subcategory: the rings tested are those whose topology is the I-adic topology of a finitely generated ideal I.

public abbrev AdicStarPropertyIsLocal (P : ∀ {B A : Type u} [CommRing B]
    [TopologicalSpace B] [IsTopologicalRing B] [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A], (B →+* A) → Prop) : Prop

TopologicalRing.PropertyIsLocalAdicStar, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 202. The attribute's comment: “the first half, the definition, at the source's class of rings: the adic topological rings -- hence complete and separated -- possessing a finitely generated ideal of definition”.

A property of morphisms of WAdm^{adic*} is local when the three locality axioms of TopologicalRing.PropertyIsLocal hold for morphisms of that subcategory.

WAdm^{adic*} is the full subcategory of WAdm whose objects are the adic topological rings possessing a finitely generated ideal of definition. Its objects are complete and separated: TopologicalRing.IsAdic is pre-adicness together with TopologicalRing.IsComplete, which is completeness for the canonical uniformity together with the Hausdorff condition.

This agrees with TopologicalRing.AdicStarPropertyIsLocal, by TopologicalRing.adicStarPropertyIsLocal_iff_propertyIsLocalAdicStar.

public abbrev PropertyIsLocalAdicStar (P : ∀ {B A : Type u} [CommRing B]
    [TopologicalSpace B] [IsTopologicalRing B] [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A], (B →+* A) → Prop) : Prop

TopologicalRing.PropertyIsLocalAdicStarUpToIso, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalPropertiesUpToIso.lean, line 155. The attribute's comment: “the first half, the definition of a local property of morphisms of WAdm^{adic}: axioms (1), (2), (3) of Situation 0CBA for morphisms of WAdm^{adic}, the completed corners of the diagram being any limits lim A'/IA', lim B'/JB'”.

A property P of morphisms of WAdm^{adic*}, the adic topological rings possessing a finitely generated ideal of definition, is local when axioms (1), (2) and (3) of Situation 0CBA hold for morphisms of WAdm^{adic*}. The completed corners of the diagrams of axioms (1) and (2) are any rings isomorphic to the inverse limits.

public abbrev PropertyIsLocalAdicStarUpToIso (P : ∀ {B A : Type u} [CommRing B]
    [TopologicalSpace B] [IsTopologicalRing B] [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0ANI, a remark

Tag 0ANI in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasProperty_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianChartCriteria.lean, line 190. The attribute's comment: “the variant of Lemma 0ANG for morphisms between locally Noetherian formal algebraic spaces over S: the equivalence of its three conditions, for a local property of morphisms of WAdm^Noeth”.

Stacks 0ANI, the variant of Stacks 0ANG for locally Noetherian formal algebraic spaces. Let S be a scheme, let f : X ⟶ Y be a morphism of locally Noetherian formal algebraic spaces over S, and let P be a local property of morphisms of WAdm^{Noeth}: axioms (1), (2) and (3) of Situation 0CBA hold for morphisms of WAdm^{Noeth} (TopologicalRing.PropertyIsLocalNoetherianUpToIso). The following are equivalent:

for every commutative diagram with U and V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to a morphism of WAdm^{Noeth} with property P;

there is a covering {Yⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Xⱼᵢ ⟶ Yⱼ ×_Y X} as in Definition 0AIM such that each Xⱼᵢ ⟶ Yⱼ corresponds to a morphism of WAdm^{Noeth} with property P;

there are a covering {Xᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Xᵢ ⟶ Yᵢ ⟶ Y with Yᵢ an affine formal algebraic space, Yᵢ ⟶ Y representable by algebraic spaces and étale, and Xᵢ ⟶ Yᵢ corresponding to a morphism of WAdm^{Noeth} with property P.

"Corresponds to a morphism of WAdm^{Noeth} with property P" is AlgebraicGeometry.FormalSpace.HasPropertyOnAffineChartMap at the class TopologicalRing.IsNoetherianAdic. This is AlgebraicGeometry.FormalSpace.hasProperty_tfae_isNoetherianAdic_of_isInvariantUnderIso, with the invariance of P under isomorphism of source and of target derived from axiom (1).

theorem hasProperty_tfae_of_isLocallyNoetherian
    (hP : TopologicalRing.PropertyIsLocalNoetherianUpToIso.{u} P)
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y) :
    List.TFAE
      [ HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f,
        HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic P f,
        HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P f ]

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SourceCoverImpliesEveryDiagramNoetherian.lean, line 172. The attribute's comment: “the variant of Lemma 0ANG for morphisms of locally Noetherian formal algebraic spaces, condition (3) implies condition (1); hP and hPiso together are the local property of WAdm^Noeth”.

The variant of Stacks 0ANG for locally Noetherian formal algebraic spaces (Remark 0ANI), condition (3) implies condition (1). Let f : X ⟶ Y be a morphism of locally Noetherian formal algebraic spaces over S and let P be a local property of morphisms of WAdmᴺᵒᵉᵗʰ (Remark 0ANI: hP for the three axioms of Situation 0CBA on WAdmᴺᵒᵉᵗʰ and hPiso for "invariant under isomorphism of source and target in this category"). If there are an affine étale covering {Uᵢ ⟶ X} as in Definition 0AIM and factorizations Uᵢ ⟶ Vᵢ ⟶ Y through affine formal algebraic spaces representable étale over Y with P on each Uᵢ ⟶ Vᵢ, then for every commutative square with affine formal algebraic spaces U, V and representable étale maps U ⟶ X, V ⟶ Y, the morphism U ⟶ V has P.

This is AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_hasChartsPresentedByClass at the class WAdmᴺᵒᵉᵗʰ: its rings are weakly admissible with a countable fundamental system of open ideals, being adic; the class is closed under completion along an étale ring map by clause (5) of Stacks 0ANB, an étale algebra over a Noetherian ring being Noetherian; and it is closed under isomorphism of topological rings. The charts of X and Y are presented by rings of the class by AlgebraicGeometry.FormalSpace.hasChartsPresentedByClass_of_isLocallyNoetherian.

theorem hasPropertyOnEveryAffineEtaleDiagram_of_afterSourceCover_of_isLocallyNoetherian
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.PropertyIsLocalNoetherian P)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsNoetherianAdic B → TopologicalRing.IsNoetherianAdic A →
      TopologicalRing.IsNoetherianAdic B' → TopologicalRing.IsNoetherianAdic A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hf : HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P f) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f

TopologicalRing.PropertyIsLocalNoetherian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 219. The attribute's comment: “local_property_noetherian”.

A morphism property of Noetherian adic topological rings is local if it ascends along completed étale localization diagrams, descends along faithfully flat ones, and is preserved by finite products of targets.

public abbrev PropertyIsLocalNoetherian
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A],
      (B →+* A) → Prop) : Prop

TopologicalRing.PropertyIsLocalNoetherianUpToIso, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalPropertiesUpToIso.lean, line 168. The attribute's comment: “the definition of a local property of morphisms of WAdm^Noeth: axioms (1), (2), (3) of Situation 0CBA for morphisms of WAdm^Noeth, the completed corners of the diagram being any limits lim A'/IA', lim B'/JB'”.

A property P of morphisms of WAdm^{Noeth}, the adic topological rings whose underlying ring is Noetherian, is local when axioms (1), (2) and (3) of Situation 0CBA hold for morphisms of WAdm^{Noeth}. The completed corners of the diagrams of axioms (1) and (2) are any rings isomorphic to the inverse limits.

public abbrev PropertyIsLocalNoetherianUpToIso (P : ∀ {B A : Type u} [CommRing B]
    [TopologicalSpace B] [IsTopologicalRing B] [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBC, a situation

Tag 0GBC in the Stacks Project.

TopologicalRing.IsStableUnderBaseChange, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 237.

A local property of morphisms of countably indexed weakly admissible rings that is preserved by completed tensor-product base change.

public structure IsStableUnderBaseChange
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBD, a lemma

Tag 0GBD in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasProperty_pullback_snd_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedPullbackLocalProperty.lean, line 117.

Stacks 0GBD. Let S be a scheme. Let P be a local property of morphisms of WAdm^count which is stable under base change. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally countably indexed formal algebraic spaces over S. If f satisfies the equivalent conditions of Stacks 0ANG, then so does pr₂ : X ×_Y Z ⟶ Z.

P being local in the sense of Situation 0CBA is TopologicalRing.PropertyIsLocal P, which TopologicalRing.IsStableUnderBaseChange P (Stacks 0GBC) contains, together with the invariance under isomorphism of source and target with which Situation 0CBA opens, hsrc and htgt. The conditions of Stacks 0ANG for f are equivalent by hasProperty_tfae_of_isLocallyCountablyIndexed, and hf is condition (1). The conclusion is that X ×_Y Z is locally countably indexed (Stacks 0GBB, clause (1)), so that the conditions of Stacks 0ANG are equivalent for pr₂, and that pr₂ satisfies all three of them.

theorem hasProperty_pullback_snd_of_isLocallyCountablyIndexed
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.IsStableUnderBaseChange.{u} P)
    (hsrc : PropertyIsInvariantUnderSourceIso.{u}
      TopologicalRing.IsCountablyWeaklyAdmissible P)
    (htgt : PropertyIsInvariantUnderTargetIsoOn.{u}
      TopologicalRing.IsCountablyWeaklyAdmissible P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P f) :
    IsLocallyCountablyIndexed B S hS (pullback f g) ∧
      HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasProperty_pullback_snd_of_isLocalUpToIso_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedPullbackLocalPropertyUpToIso.lean, line 58.

Let S be a scheme. Let P be a local property of morphisms of WAdm^count which is stable under base change. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally countably indexed formal algebraic spaces over S. If f satisfies the equivalent conditions of Stacks 0ANG, then so does pr₂ : X ×_Y Z ⟶ Z.

Here hloc says that P is local in the sense of Situation 0CBA, hP that it is stable under base change (Situation 0GBC), and hf is condition (1) of Stacks 0ANG for f. The conclusion is that X ×_Y Z is locally countably indexed (Stacks 0GBB, clause (1)) and that pr₂ satisfies all three conditions of Stacks 0ANG.

theorem hasProperty_pullback_snd_of_isLocalUpToIso_of_isLocallyCountablyIndexed
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hloc : TopologicalRing.PropertyIsLocalUpToIso.{u} P)
    (hP : TopologicalRing.IsStableUnderBaseChange.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P f) :
    IsLocallyCountablyIndexed B S hS (pullback f g) ∧
      HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasProperty_tfae_pullback_snd_of_isLocalUpToIso_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedPullbackLocalPropertyUpToIso.lean, line 89. The attribute's comment: “the conditions of Stacks 0ANG for f taken as any one of them, and the conclusion including their equivalence for pr₂”.

Let S be a scheme. Let P be a local property of morphisms of WAdm^count which is stable under base change. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally countably indexed formal algebraic spaces over S. If f satisfies one, hence all, of the equivalent conditions of Stacks 0ANG, then X ×_Y Z is locally countably indexed, the conditions of Stacks 0ANG are equivalent for pr₂ : X ×_Y Z ⟶ Z, and pr₂ satisfies all three of them.

theorem hasProperty_tfae_pullback_snd_of_isLocalUpToIso_of_isLocallyCountablyIndexed
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hloc : TopologicalRing.PropertyIsLocalUpToIso.{u} P)
    (hP : TopologicalRing.IsStableUnderBaseChange.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
        TopologicalRing.IsCountablyWeaklyAdmissible P f ∨
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f ∨
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f) :
    IsLocallyCountablyIndexed B S hS (pullback f g) ∧
      List.TFAE
        [ HasPropertyOnEveryAffineEtaleDiagram B S hS
            TopologicalRing.IsCountablyWeaklyAdmissible P (pullback.snd f g),
          HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
            (pullback.snd f g),
          HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
            (pullback.snd f g) ] ∧
      HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P
        (pullback.snd f g)

Tag 0GBE, a remark

Tag 0GBE in the Stacks Project.

AlgebraicGeometry.FormalSpace.pullback_snd_hasProperty_of_isLocallyAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarBaseChangeVariant.lean, line 134. The attribute's comment: “the second half, the variant of Lemma 0GBD for morphisms between locally adic formal algebraic spaces: for a local property P of morphisms of WAdm^{adic} (Remark 0ANH, with the invariance under isomorphism of source and target that Situation 0CBA stipulates) which is stable under base change in the sense of the first half, TopologicalRing.PropertyIsStableUnderBaseChangeAdicStar, and morphisms f : X -> Y, g : Z -> Y of locally adic formal algebraic spaces, if f satisfies condition (1) of the equivalent conditions of Stacks 0ANG then X x_Y Z is locally adic and pr2 : X x_Y Z -> Z satisfies all three”.

Stacks 0GBE, second half: the variant of Lemma 0GBD for locally adic* formal algebraic spaces. Let P be a local property of morphisms of WAdm^{adic*} (Remark 0ANH), invariant under isomorphism of source and target as Situation 0CBA stipulates, and stable under base change in the sense of the first half of Remark 0GBE. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally adic* formal algebraic spaces over S. If f satisfies the equivalent conditions of Stacks 0ANG for P — here condition (1), that P holds on every affine étale diagram over f — then X ×_Y Z is again locally adic* (Stacks 0GBB (4)), so that the conditions of Stacks 0ANG make sense for pr₂ : X ×_Y Z ⟶ Z, and pr₂ satisfies all three of them.

theorem pullback_snd_hasProperty_of_isLocallyAdicStar
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.PropertyIsStableUnderBaseChangeAdicStar.{u} P)
    (hsrc : PropertyIsInvariantUnderSourceIso.{u} TopologicalRing.IsAdicStar P)
    (htgt : PropertyIsInvariantUnderTargetIsoOn.{u} TopologicalRing.IsAdicStar P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y)
    (hZ : IsLocallyAdicStar B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f) :
    IsLocallyAdicStar B S hS (pullback f g) ∧
      HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasProperty_pullback_snd_of_isLocalUpToIso_of_isLocallyAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarPullbackLocalPropertyUpToIso.lean, line 81. The attribute's comment: “the second half, the variant of Lemma 0GBD for morphisms between locally adic formal algebraic spaces: for a local property P of morphisms of WAdm^{adic} in the sense of Remark 0ANH (hloc, TopologicalRing.PropertyIsLocalAdicStarUpToIso) which is stable under base change in the sense of the first half (hP, TopologicalRing.PropertyIsStableUnderBaseChangeAdicStar), and morphisms f : X -> Y, g : Z -> Y of locally adic formal algebraic spaces, if f satisfies the equivalent conditions of the variant of Stacks 0ANG then X x_Y Z is locally adic and pr2 : X x_Y Z -> Z satisfies all three”.

Stacks 0GBE, second half: the variant of Lemma 0GBD for locally adic* formal algebraic spaces. Let P be a local property of morphisms of WAdm^{adic*} (Remark 0ANH) which is stable under base change in the sense of the first half of Remark 0GBE. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally adic* formal algebraic spaces over S. If f satisfies the equivalent conditions of the variant of Stacks 0ANG of Remark 0ANH for P, then so does pr₂ : X ×_Y Z ⟶ Z.

P being local in the sense of Remark 0ANH is hloc, and P being stable under base change is hP. The conditions for f are equivalent by AlgebraicGeometry.FormalSpace.hasProperty_tfae_isAdicStar, and hf is condition (1). The conclusion is that X ×_Y Z is again locally adic*, so that those conditions are equivalent for pr₂, and that pr₂ satisfies all three of them.

theorem hasProperty_pullback_snd_of_isLocalUpToIso_of_isLocallyAdicStar
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hloc : TopologicalRing.PropertyIsLocalAdicStarUpToIso.{u} P)
    (hP : TopologicalRing.PropertyIsStableUnderBaseChangeAdicStar.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y)
    (hZ : IsLocallyAdicStar B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f) :
    IsLocallyAdicStar B S hS (pullback f g) ∧
      HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P (pullback.snd f g)

TopologicalRing.AdicStarPropertyIsStableUnderBaseChange, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 264. The attribute's comment: “adic_star_base_change_stability”.

A local property of morphisms of weakly admissible adic-star rings that is preserved by completed tensor-product base change.

public structure AdicStarPropertyIsStableUnderBaseChange
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

TopologicalRing.PropertyIsStableUnderBaseChangeAdicStar, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 317. The attribute's comment: “the first half, the definition of stability under base change, at the source's class of rings: the morphisms range over WAdm^{adic}, the adic topological rings -- hence complete and separated -- possessing a finitely generated ideal of definition, and the locality of P is read in the same subcategory by TopologicalRing.PropertyIsLocalAdicStar. The well definedness the remark cites, that the completed tensor product is again an object of WAdm^{adic} by Lemma 87.4.12, is TopologicalRing.isAdicStar_completedTensorProduct”.

A local property P of morphisms of WAdm^{adic*} is stable under base change when, for every pair of morphisms B → A and B → C of WAdm^{adic*}, P (B → A) implies P (C → A ⊗̂_B C).

WAdm^{adic*} is the full subcategory of WAdm whose objects are the adic, hence complete and separated, topological rings possessing a finitely generated ideal of definition, and the locality of P is TopologicalRing.PropertyIsLocalAdicStar, read in the same subcategory. That A ⊗̂_B C lies in WAdm^{adic*} is TopologicalRing.isAdicStar_completedTensorProduct.

This agrees with TopologicalRing.AdicStarPropertyIsStableUnderBaseChange, by TopologicalRing.adicStarPropertyIsStableUnderBaseChange_iff.

public structure PropertyIsStableUnderBaseChangeAdicStar
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Declarations registered for the tag:

TopologicalRing.completedTensorProduct_isWeaklyAdmissible, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 287 (StacksFrontier): “completed_tensor_adic_star”.
TopologicalRing.completedTensorProduct_isAdic, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 289 (StacksFrontier): “completed_tensor_adic_star”.
TopologicalRing.exists_fg_ideal_of_definition, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 290 (StacksFrontier): “completed_tensor_adic_star”.
TopologicalRing.completedTensorProduct_isWeaklyAdmissible, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalPropertiesRefined.lean, line 277 (StacksFrontier): “completed_tensor_adic_star”.
TopologicalRing.completedTensorProduct_isAdic, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalPropertiesRefined.lean, line 279 (StacksFrontier): “completed_tensor_adic_star”.
TopologicalRing.exists_fg_ideal_of_definition, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/LocalPropertiesRefined.lean, line 280 (StacksFrontier): “completed_tensor_adic_star”.

Tag 0GBF, a remark

Tag 0GBF in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_pullback_snd_of_stableBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChange.lean, line 340. The attribute's comment: “the 0GBD variant for locally Noetherian formal algebraic spaces”.

Stacks 0GBF, the variant of Stacks 0GBD for locally Noetherian formal algebraic spaces: let P be stable under base change for Noetherian adic topological rings in the sense of Stacks 0GBF. If f : X ⟶ Y satisfies condition (1) of Stacks 0ANG for P, then for every g : Z ⟶ Y the second projection X ×_Y Z ⟶ Z satisfies condition (1) for P.

Nothing is asked of g, exactly as the definition of Stacks 0GBF imposes no condition on the morphism being based along: stability under base change is stability under base change by the property that holds of every morphism, and that property is local, so the statement is the one of Stacks 0GBG with Q instantiated there.

The three further hypotheses are those the Stacks 0GBG statements already carry, for the same reasons: hcover is the geometric input of Stacks 0GBD, h31 the implication (3) ⟹ (1) of Stacks 0ANG, and hiso the invariance of P under isomorphism of targets.

theorem hasPropertyOnEveryAffineEtaleDiagram_pullback_snd_of_stableBaseChange
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.IsStableUnderBaseChangeNoetherian.{u} P)
    (hiso : PropertyIsInvariantUnderTargetIso.{u} P)
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hcover : HasBaseChangeCoverOverPullbackSnd B S hS f g)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P f) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.conditions_pullback_snd_of_isStableUnderBaseChangeNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChangeNoetherian.lean, line 273. The attribute's comment: “the variant of Stacks 0GBD for morphisms between locally Noetherian formal algebraic spaces; the definition of stability under base change is TopologicalRing.IsStableUnderBaseChangeNoetherian”.

The variant of Stacks 0GBD for locally Noetherian formal algebraic spaces. Let P be a local property of morphisms of WAdm^{Noeth} (Remark 0ANI) which is stable under base change: given B → A and B → C in WAdm^{Noeth}, P (B → A) implies that A ⊗̂_B C is adic Noetherian and that P (C → A ⊗̂_B C) holds (TopologicalRing.IsStableUnderBaseChangeNoetherian, the definition of the remark). Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally Noetherian formal algebraic spaces over S. If f satisfies the equivalent conditions of Stacks 0ANG, then so does pr₂ : X ×_Y Z ⟶ Z; all three of them are concluded.

Being local in the sense of Remark 0ANI is hP.isLocal together with hPiso, the invariance of P under isomorphism of source and target that Situation 0CBA assumes. Nothing is asked of g.

theorem conditions_pullback_snd_of_isStableUnderBaseChangeNoetherian
    (P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hP : TopologicalRing.IsStableUnderBaseChangeNoetherian.{u} P)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsNoetherianAdic B → TopologicalRing.IsNoetherianAdic A →
      TopologicalRing.IsNoetherianAdic B' → TopologicalRing.IsNoetherianAdic A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic P (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P (pullback.snd f g)

TopologicalRing.IsStableUnderBaseChangeNoetherian, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 352. The attribute's comment: “the definition of stability under base change; not the 0GBD variant for spaces”.

A local property P of morphisms of Noetherian adic topological rings is stable under base change when, for every pair of continuous homomorphisms B →+* A and B →+* C of such rings, P (B →+* A) forces the completed tensor product A ⊗̂_B C to be adic Noetherian again and P to hold for C →+* A ⊗̂_B C. No condition is imposed on B →+* C.

public structure IsStableUnderBaseChangeNoetherian
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBG, a remark

Tag 0GBG in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyAfterSourceCover_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChange.lean, line 236. The attribute's comment: “condition (3) for pr₂, with the 0GBD cover and iso-invariance assumed”.

Stacks 0GBG, in the form that the argument of Stacks 0GBD produces: if P is stable under base change by Q and f : X ⟶ Y, g : Z ⟶ Y satisfy condition (1) of Stacks 0ANG for P and for Q, then the second projection X ×_Y Z ⟶ Z satisfies condition (3) of Stacks 0ANG for P.

The covering of X ×_Y Z by fibre products of charts, with the presentation of those fibre products by completed tensor products, is the hypothesis hcover; it mentions neither P nor Q. The isomorphism invariance of P implied by the locality of Stacks 0ANI is hiso.

theorem hasPropertyAfterSourceCover_pullback_snd
    (P Q : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hPQ : TopologicalRing.IsStableUnderBaseChangeBy.{u} P Q)
    (hiso : PropertyIsInvariantUnderTargetIso.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hcover : HasBaseChangeCoverOverPullbackSnd B S hS f g)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) Q g) :
    HasPropertyAfterSourceCover B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChange.lean, line 263. The attribute's comment: “condition (1) for pr₂, with the 0GBD cover, 0ANG (3) ⟹ (1) and iso-invariance”.

Stacks 0GBG. Let P be stable under base change by Q for Noetherian adic topological rings. If f : X ⟶ Y and g : Z ⟶ Y are morphisms of locally Noetherian formal algebraic spaces over S satisfying condition (1) of Stacks 0ANG for P and for Q respectively, then the second projection X ×_Y Z ⟶ Z satisfies condition (1) for P.

Condition (3) is what the argument of Stacks 0GBD gives; the passage back to condition (1) is the implication (3) ⟹ (1) of Stacks 0ANG, carried as the hypothesis h31.

theorem hasPropertyOnEveryAffineEtaleDiagram_pullback_snd
    (P Q : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hPQ : TopologicalRing.IsStableUnderBaseChangeBy.{u} P Q)
    (hiso : PropertyIsInvariantUnderTargetIso.{u} P)
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hcover : HasBaseChangeCoverOverPullbackSnd B S hS f g)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) Q g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS
      (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.transfersBaseChangeOnAffineEtaleDiagrams, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChange.lean, line 288. The attribute's comment: “the transfer for every property pair, on the same three hypotheses”.

Stacks 0GBG, uniformly over all pairs of properties: whenever P is stable under base change by Q for Noetherian adic topological rings, condition (1) of Stacks 0ANG transfers from (f, P) and (g, Q) to (X ×_Y Z ⟶ Z, P).

The three inputs of the single-pair statement are asked of every property local in the sense of Stacks 0ANI, which is how the stability bundle of Stacks 0GBG supplies locality, and of every pair of morphisms.

theorem transfersBaseChangeOnAffineEtaleDiagrams
    (hiso : ∀ P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop,
      TopologicalRing.PropertyIsLocalNoetherian.{u} P → PropertyIsInvariantUnderTargetIso.{u} P)
    (h31 : ∀ P : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop,
      TopologicalRing.PropertyIsLocalNoetherian.{u} P →
        SourceCoverImpliesEveryAffineEtaleDiagram B S hS
          (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P)
    (hcover : ∀ {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y),
      HasBaseChangeCoverOverPullbackSnd B S hS f g) :
    ∀ (P Q : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
        [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop),
      TopologicalRing.IsStableUnderBaseChangeBy.{u} P Q →
      ∀ {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y),
        HasPropertyOnEveryAffineEtaleDiagram B S hS
            (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P f →
          HasPropertyOnEveryAffineEtaleDiagram B S hS
              (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) Q g →
            HasPropertyOnEveryAffineEtaleDiagram B S hS
              (fun R ↦ TopologicalRing.IsAdic R ∧ IsNoetherianRing R) P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.conditions_pullback_snd_of_isStableUnderBaseChangeBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyBaseChangeNoetherian.lean, line 162. The attribute's comment: “the statement drawn there: the equivalent conditions of Stacks 0ANG pass from f and P and from g and Q to the second projection of X ×_Y Z and P, for locally Noetherian formal algebraic spaces; the notion of stability under base change by Q is TopologicalRing.IsStableUnderBaseChangeBy”.

Let P and Q be local properties of morphisms of WAdm^{Noeth} (Remark 0ANI), with P stable under base change by Q: given B → A and B → C in WAdm^{Noeth} with P (B → A) and Q (B → C), the completed tensor product A ⊗̂_B C is adic Noetherian and P (C → A ⊗̂_B C) holds (TopologicalRing.IsStableUnderBaseChangeBy). Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of locally Noetherian formal algebraic spaces over S such that the equivalent conditions of Stacks 0ANG hold for f and P and for g and Q. Then the equivalent conditions of Stacks 0ANG hold for pr₂ : X ×_Y Z ⟶ Z and P; all three of them are concluded.

Being local in the sense of Remark 0ANI is hPQ.isLocalP together with hPiso, the invariance of P under isomorphism of source and target that Situation 0CBA assumes of a property of arrows of the category.

theorem conditions_pullback_snd_of_isStableUnderBaseChangeBy
    (P Q : ∀ {R₁ R₂ : Type u} [CommRing R₁] [TopologicalSpace R₁] [IsTopologicalRing R₁]
      [CommRing R₂] [TopologicalSpace R₂] [IsTopologicalRing R₂], (R₁ →+* R₂) → Prop)
    (hPQ : TopologicalRing.IsStableUnderBaseChangeBy.{u} P Q)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsNoetherianAdic B → TopologicalRing.IsNoetherianAdic A →
      TopologicalRing.IsNoetherianAdic B' → TopologicalRing.IsNoetherianAdic A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Z ⟶ Y)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic Q g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P
        (pullback.snd f g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic P (pullback.snd f g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P (pullback.snd f g)

TopologicalRing.IsStableUnderBaseChangeBy, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 379. The attribute's comment: “stable_under_base_change_by_noetherian”.

A local morphism property of Noetherian adic rings is stable under completed tensor-product base change along morphisms satisfying another local property.

public structure IsStableUnderBaseChangeBy (P Q : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B]
    [IsTopologicalRing B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A],
    (B →+* A) → Prop) : Prop

Tag 0GBH, a situation

Tag 0GBH in the Stacks Project.

TopologicalRing.PropertyIsStableUnderComposition, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 439.

A local property of morphisms of countably indexed weakly admissible rings is stable under composition when two composable morphisms with the property have a composite with the property.

public structure PropertyIsStableUnderComposition
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBI, a lemma

Tag 0GBI in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyComposition.lean, line 261. The attribute's comment: “condition (1) for the composite, granting the composition axiom of Situation 0GBH read on charts through Stacks 0AN0 (hchart), the implication (3) ⟹ (1) of Stacks 0ANG (h31) and the fibre products of Stacks 0AJ3 (hpbf, hpbg)”.

Stacks 0GBI. Let P be a local property of arrows of the class C which is stable under composition. If f : X ⟶ Y and g : Y ⟶ Z are morphisms of formal algebraic spaces over S satisfying the equivalent conditions of Stacks 0ANG for P, then so does g ∘ f.

Condition (3) is what the covering of the proof gives; the passage back to condition (1) is the implication (3) ⟹ (1) of Stacks 0ANG, carried as the hypothesis h31.

theorem hasPropertyOnEveryAffineEtaleDiagram_comp
    (hchart : ChartPropertyIsStableUnderComposition B S hS C P)
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS C P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hZ : IsFormalAlgebraicSpace B S hS Z)
    (hpbg : HasFormalAlgebraicSpaceChartPullbacks B S hS g)
    (hpbf : HasFormalAlgebraicSpaceChartPullbacks B S hS f)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS C P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS C P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS C P (f ≫ g)

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCompositionPresented.lean, line 314.

Stacks 0GBI. Let P be a local property of morphisms of WAdm^{count} which is stable under composition, and let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally countably indexed formal algebraic spaces over S. If f and g satisfy the equivalent conditions of Stacks 0ANG, then so does g ∘ f: the conclusion lists all three of them. Being a local property in the sense of Situation 0CBA is hP.isLocal together with hPiso, the invariance of P under isomorphism of source and target that the situation assumes.

The covering of the proof is AlgebraicGeometry.FormalSpace.exists_affineEtaleCover_chartFactorization_comp_of_atlas, built on the countably indexed atlas of Y; its intermediate charts are countably indexed by clause (1) of Stacks 0AKQ, hence presented by rings of WAdm^{count} (Stacks 0AN1), and the composition axiom applies through Stacks 0AN0. That gives condition (3) for g ∘ f; condition (1) follows by the implication (3) ⟹ (1) of Stacks 0ANG, from the presented refinement of a covering of the source and the locality of P, and condition (2) by (1) ⟹ (2).

theorem hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyCountablyIndexed
    (hP : TopologicalRing.PropertyIsStableUnderComposition P)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsCountablyWeaklyAdmissible B →
      TopologicalRing.IsCountablyWeaklyAdmissible A →
      TopologicalRing.IsCountablyWeaklyAdmissible B' →
      TopologicalRing.IsCountablyWeaklyAdmissible A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS
        TopologicalRing.IsCountablyWeaklyAdmissible P (f ≫ g) ∧
      HasPropertyAfterTargetCover B S hS
        TopologicalRing.IsCountablyWeaklyAdmissible P (f ≫ g) ∧
      HasPropertyAfterSourceCover B S hS
        TopologicalRing.IsCountablyWeaklyAdmissible P (f ≫ g)

Tag 0GBJ, a remark

Tag 0GBJ in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarCompositionVariant.lean, line 234. The attribute's comment: “the second half, the variant of Lemma 0GBI for morphisms between locally adic formal algebraic spaces: for a local property P of morphisms of WAdm^{adic} (Remark 0ANH) which is stable under composition in the sense of the first half, TopologicalRing.PropertyIsStableUnderCompositionAdicStar, and morphisms f : X -> Y, g : Y -> Z of locally adic* formal algebraic spaces satisfying the equivalent conditions of Stacks 0ANG (condition (1)), the composite g o f satisfies all three; the invariance of P under isomorphism of Situation 0CBA is not used”.

Stacks 0GBJ, second half: the variant of Lemma 0GBI for locally adic* formal algebraic spaces. Let P be a local property of morphisms of WAdm^{adic*} (Remark 0ANH) which is stable under composition in the sense of the first half of Remark 0GBJ, TopologicalRing.PropertyIsStableUnderCompositionAdicStar. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally adic* formal algebraic spaces over S. If f and g satisfy the equivalent conditions of Stacks 0ANG for P (in the adic* reading of Remark 0ANH) — here condition (1), that P holds on every affine étale diagram, the strongest of the three — then so does g ∘ f: the conclusion lists all three conditions.

Condition (1) for g ∘ f is AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocal at the class WAdm^{adic*}: every affine formal algebraic space representable étale over Y is adic* by the implication (2) ⟹ (1) of Stacks 0AKX, hence presented by a ring of WAdm^{adic*}. Conditions (2) and (3) follow by the implications (1) ⟹ (2) ⟹ (3) of Stacks 0ANG. The invariance of P under isomorphism of source and target, which Situation 0CBA stipulates, is not needed.

theorem hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyAdicStar
    (hP : TopologicalRing.PropertyIsStableUnderCompositionAdicStar.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y)
    (hZ : IsLocallyAdicStar B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P (f ≫ g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P (f ≫ g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P (f ≫ g)

TopologicalRing.AdicStarPropertyIsStableUnderComposition, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 461. The attribute's comment: “stable_under_composition_for_adic_ring_map_properties”.

A local property of morphisms of weakly admissible adic-star rings is stable under composition if it is preserved by composition of continuous maps between such rings.

public structure AdicStarPropertyIsStableUnderComposition
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
      [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

TopologicalRing.PropertyIsStableUnderCompositionAdicStar, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 497. The attribute's comment: “the definition of stability under composition, at the source's class of rings: the morphisms range over WAdm^{adic*}, the adic topological rings -- hence complete and separated -- possessing a finitely generated ideal of definition, and the locality of P is read in the same subcategory by TopologicalRing.PropertyIsLocalAdicStar”.

A local property P of morphisms of WAdm^{adic*} is stable under composition when, for morphisms B → A and C → B of WAdm^{adic*}, P (B → A) and P (C → B) imply P (C → A).

WAdm^{adic*} is the full subcategory of WAdm whose objects are the adic, hence complete and separated, topological rings possessing a finitely generated ideal of definition, and the locality of P is TopologicalRing.PropertyIsLocalAdicStar, read in the same subcategory.

This agrees with TopologicalRing.AdicStarPropertyIsStableUnderComposition, by TopologicalRing.adicStarPropertyIsStableUnderComposition_iff.

public structure PropertyIsStableUnderCompositionAdicStar
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
      [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBK, a remark

Tag 0GBK in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCompositionPresented.lean, line 378. The attribute's comment: “the variant of Stacks 0GBI for morphisms between locally Noetherian formal algebraic spaces; the definition of stability under composition is TopologicalRing.PropertyIsStableUnderCompositionNoetherian”.

Stacks 0GBK. A local property P of morphisms of WAdm^{Noeth} is stable under composition when P(B → A) ∧ P(C → B) ⟹ P(C → A) for arrows of WAdm^{Noeth}: that is the structure TopologicalRing.PropertyIsStableUnderCompositionNoetherian, whose isLocal field together with hPiso (invariance under isomorphism of source and target, assumed by Situation 0CBA and hence by Remark 0ANI) make P local. The variant of Stacks 0GBI then holds for morphisms between locally Noetherian formal algebraic spaces: if f : X ⟶ Y and g : Y ⟶ Z satisfy the equivalent conditions of Stacks 0ANG for P on WAdm^{Noeth}, so does g ∘ f, and the conclusion lists all three of them.

The covering is AlgebraicGeometry.FormalSpace.exists_presentedSourceCover_comp_of_atlas built on the Noetherian atlases of X, Y and Z: its charts stay Noetherian along representable étale maps by clause (5) of Stacks 0AKQ and are then presented by their presenting rings, which are Noetherian and adic, so the composition axiom applies through Stacks 0AN0 and gives condition (3) on a covering with presented members. The implication (3) ⟹ (1) of Stacks 0ANG on such a covering is AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_presentedSourceCover, at the class WAdm^{Noeth}, whose closure conditions are clauses of Stacks 0ANB; condition (2) follows by (1) ⟹ (2).

theorem hasPropertyOnEveryAffineEtaleDiagram_comp_of_isLocallyNoetherian
    (hP : TopologicalRing.PropertyIsStableUnderCompositionNoetherian P)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsNoetherianAdic B → TopologicalRing.IsNoetherianAdic A →
      TopologicalRing.IsNoetherianAdic B' → TopologicalRing.IsNoetherianAdic A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f)
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P (f ≫ g) ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic P (f ≫ g) ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P (f ≫ g)

TopologicalRing.PropertyIsStableUnderCompositionNoetherian, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 525. The attribute's comment: “stable_under_composition_noetherian”.

A local property of morphisms of Noetherian adic rings is stable under composition when it holds for the composite of two continuous morphisms having the property.

public structure PropertyIsStableUnderCompositionNoetherian
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBL, a situation

Tag 0GBL in the Stacks Project.

TopologicalRing.PropertyIsLocalWithCancellation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 546.

A local property of morphisms of countably indexed weakly admissible rings with the cancellation property for composable morphisms.

public structure PropertyIsLocalWithCancellation
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBM, a lemma

Tag 0GBM in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCancellation.lean, line 182.

Let P be a local property of morphisms of WAdmᶜᵒᵘⁿᵗ which has the cancellation property, and let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally countably indexed formal algebraic spaces over S. If g ∘ f and g satisfy HasPropertyOnEveryAffineEtaleDiagram, then f satisfies HasPropertyOnEveryAffineEtaleDiagram, HasPropertyAfterTargetCover and HasPropertyAfterSourceCover.

Here P being local with the cancellation property is hP (the three axioms and the cancellation property) together with hPiso, the clause that P is "invariant under isomorphism of source and target in this category".

theorem hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyCountablyIndexed
    (hP : TopologicalRing.PropertyIsLocalWithCancellation P)
    (hPiso : ∀ {B A B' A' : Type u}
      [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
      [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
      [CommRing B'] [TopologicalSpace B'] [IsTopologicalRing B'] [IsLinearTopology B' B']
      [CommRing A'] [TopologicalSpace A'] [IsTopologicalRing A'] [IsLinearTopology A' A']
      (eB : B ≃+* B') (eA : A ≃+* A'), Continuous eB → Continuous eB.symm →
      Continuous eA → Continuous eA.symm → ∀ (f : B →+* A), Continuous f →
      TopologicalRing.IsCountablyWeaklyAdmissible B →
      TopologicalRing.IsCountablyWeaklyAdmissible A →
      TopologicalRing.IsCountablyWeaklyAdmissible B' →
      TopologicalRing.IsCountablyWeaklyAdmissible A' →
      (P f ↔ P ((eA.toRingHom.comp f).comp eB.symm.toRingHom)))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (hZ : IsLocallyCountablyIndexed B S hS Z)
    (hfg : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P (f ≫ g))
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS
      TopologicalRing.IsCountablyWeaklyAdmissible P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS
        TopologicalRing.IsCountablyWeaklyAdmissible P f ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsCountablyWeaklyAdmissible P f

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyComposition.lean, line 306. The attribute's comment: “condition (1) for the first factor, granting the cancellation axiom of Situation 0GBL read on charts through Stacks 0AN0 (hchart), the implication (3) ⟹ (1) of Stacks 0ANG (h31) and the fibre products of Stacks 0AJ3 (hpbf, hpbg)”.

Stacks 0GBM. Let P be a local property of arrows of the class C with the cancellation property. If g ∘ f and g : Y ⟶ Z satisfy the equivalent conditions of Stacks 0ANG for P, then so does f : X ⟶ Y.

Condition (3) is what the covering of the proof gives; the passage back to condition (1) is the implication (3) ⟹ (1) of Stacks 0ANG, carried as the hypothesis h31.

theorem hasPropertyOnEveryAffineEtaleDiagram_of_comp
    (hchart : ChartPropertyHasCancellation B S hS C P)
    (h31 : SourceCoverImpliesEveryAffineEtaleDiagram B S hS C P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hZ : IsFormalAlgebraicSpace B S hS Z)
    (hpbg : HasFormalAlgebraicSpaceChartPullbacks B S hS g)
    (hpbf : HasFormalAlgebraicSpaceChartPullbacks B S hS f)
    (hfg : HasPropertyOnEveryAffineEtaleDiagram B S hS C P (f ≫ g))
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS C P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS C P f

Tag 0GBN, a remark

Tag 0GBN in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarCancellationVariant.lean, line 102. The attribute's comment: “the second half: the variant of Lemma 0GBM (the remark's Lemma 0GBI is a slip for 0GBM, an erratum to the Stacks Project) for morphisms f : X -> Y, g : Y -> Z between locally adic formal algebraic spaces over S, for a local property P of WAdm^{adic} (Remark 0ANH: invariant under isomorphism of source and target and satisfying the three axioms of Situation 0CBA) having the cancellation property TopologicalRing.HasAdicStarCancellationProperty: if g o f and g satisfy the equivalent conditions of Stacks 0ANG then so does f”.

Stacks 0GBN, second half: the cancellation variant for locally adic* formal algebraic spaces. Let P be a local property of morphisms of WAdm^{adic*} in the sense of Remark 0ANH, hP: a property of arrows of WAdm^{adic*} invariant under isomorphism of source and target in that category and satisfying the three axioms of Situation 0CBA there. Suppose P has the cancellation property of the first half of the remark, hcancel: for B → A and C → B in WAdm^{adic*}, P(C → A) ∧ P(C → B) ⟹ P(B → A). Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of locally adic* formal algebraic spaces over S. If g ∘ f and g satisfy the equivalent conditions of Stacks 0ANG for P at WAdm^{adic*} — here condition (1), which is equivalent to the other two by the second half of Stacks 0ANH — then so does f; the conclusion lists all three.

The proof is that of Stacks 0GBM: on the covering Uᵢ ⟶ Vᵢ ⟶ Wᵢ of AlgebraicGeometry.FormalSpace.hasPropertyAfterSourceCover_of_comp_of_atlas, built on adic* atlases of X, Y, Z, the maps Vᵢ ⟶ Wᵢ and Uᵢ ⟶ Wᵢ correspond to arrows C → B and C → A of WAdm^{adic*} with P, so Uᵢ ⟶ Vᵢ, corresponding to B → A, has P.

theorem hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyAdicStar
    (hP : TopologicalRing.PropertyIsLocal'.{u} P TopologicalRing.IsAdicStar)
    (hcancel : TopologicalRing.HasAdicStarCancellationProperty.{u} P)
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y)
    (hZ : IsLocallyAdicStar B S hS Z)
    (hfg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P (f ≫ g))
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsAdicStar P f ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsAdicStar P f ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsAdicStar P f

TopologicalRing.HasAdicStarCancellationProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicStarCancellation.lean, line 48. The attribute's comment: “the cancellation property”.

Cancellation for a morphism property of WAdm^{adic*} (Stacks 0GBN). Given arrows f : B →+* A and g : C →+* B of WAdm^{adic*} — continuous homomorphisms of weakly admissible topological rings each carrying the adic topology of a finitely generated ideal — the property of the composite C → A and the property of C → B together imply the property of B → A.

public abbrev HasAdicStarCancellationProperty
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
      [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Tag 0GBP, a remark

Tag 0GBP in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocalPropertyCancellationPresented.lean, line 90. The attribute's comment: “the variant of Stacks 0GBM for morphisms between locally Noetherian formal algebraic spaces; the definition of the cancellation property is TopologicalRing.HasNoetherianCancellationProperty”.

Stacks 0GBP. Let P be a local property of morphisms of WAdm^{Noeth} in the sense of Remark 0ANI: it satisfies the three axioms of Situation 0CBA for morphisms of WAdm^{Noeth}, which is hP, and is invariant under isomorphism of source and target, which Situation 0CBA assumes and is hPiso. Suppose P has the cancellation property: for arrows B → A and C → B of WAdm^{Noeth}, P(C → B) ∧ P(C → A) ⟹ P(B → A), which is hcancel. Then the variant of Stacks 0GBM holds for morphisms between locally Noetherian formal algebraic spaces: if f : X ⟶ Y and g : Y ⟶ Z are such that g ∘ f and g satisfy the equivalent conditions of Stacks 0ANG for P on WAdm^{Noeth}, so does f, and the conclusion lists all three of them.

The covering is the one of the proof of Stacks 0GBM, AlgebraicGeometry.FormalSpace.exists_presentedSourceCover_of_comp_of_atlas, built on the Noetherian atlases of X, Y and Z: its charts stay Noetherian along representable étale maps by clause (5) of Stacks 0AKQ and are presented by their presenting rings, which are Noetherian and adic, so the cancellation property applies through Stacks 0AN0 and gives condition (3) for f on a covering with presented members. The implication (3) ⟹ (1) of Stacks 0ANG on such a covering is AlgebraicGeometry.FormalSpace.hasPropertyOnEveryAffineEtaleDiagram_of_presentedSourceCover, at the class WAdm^{Noeth}; condition (2) follows by (1) ⟹ (2).

theorem hasPropertyOnEveryAffineEtaleDiagram_of_comp_of_isLocallyNoetherian
    (hP : TopologicalRing.PropertyIsLocalNoetherian.{u} P)
    (hcancel : TopologicalRing.HasNoetherianCancellationProperty.{u} P)
    (hPiso : TopologicalRing.IsomorphismInvariant.{u} P
      (fun R _ _ _ _ ↦ TopologicalRing.IsNoetherianAdic R))
    {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hX : IsLocallyNoetherian B S hS X) (hY : IsLocallyNoetherian B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hfg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P
      (f ≫ g))
    (hg : HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P g) :
    HasPropertyOnEveryAffineEtaleDiagram B S hS TopologicalRing.IsNoetherianAdic P f ∧
      HasPropertyAfterTargetCover B S hS TopologicalRing.IsNoetherianAdic P f ∧
      HasPropertyAfterSourceCover B S hS TopologicalRing.IsNoetherianAdic P f

TopologicalRing.HasNoetherianCancellationProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/LocalProperties.lean, line 565. The attribute's comment: “noetherian_cancellation_property”.

Cancellation for a morphism property on Noetherian adic topological rings.

public abbrev HasNoetherianCancellationProperty
    (P : ∀ {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A], (B →+* A) → Prop) : Prop

Sources

LeanTopologicalRing.completionOver_isCountablyGenerated_nhds_zero · TopologicalRing.completionOver_isCountablyAdmissible · TopologicalRing.completionOver_isWeaklyAdic · TopologicalRing.completionOver_exists_fg_isAdic · TopologicalRing.completionOver_isNoetherianAdic · TopologicalRing.LocalizationDiagram · TopologicalRing.PropertyIsLocal · AlgebraicGeometry.FormalSpace.hasPropertyAfterTargetCover_of_everyAffineEtaleDiagram

Section87.22 Taut ring maps and representability by algebraic spaces #

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

Tag 0ANJ, a lemma

Tag 0ANJ in the Stacks Project.

RingHom.QuotientDiagram.isTaut_iff_hasQuotientDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/QuotientDiagram.lean, line 303. The attribute's comment: “taut_iff_quotient_diagram”.

A continuous arrow of weakly admissible linearly topologized rings is taut if and only if its canonical quotients along any chosen decreasing fundamental sequence form the quotient diagram whose topological inverse limit is the target.

public theorem isTaut_iff_hasQuotientDiagram {A B : Type*}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    (f : B →+* A) (hf : Continuous f)
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hB : TopologicalRing.IsWeaklyAdmissible B)
    (J : ℕ → Ideal B) (hJ : IsFundamentalSequence J) :
    RingHom.IsTaut f ↔ HasQuotientDiagram f J hJ.2.1

TopologicalRing.isTaut_localizationPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocal.lean, line 200. The attribute's comment: “taut_is_local_property”.

Tautness ascends along a completed étale localization diagram of countably indexed weakly admissible rings.

public theorem isTaut_localizationPreserves :
    LocalizationPreserves.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f)

TopologicalRing.isTaut_faithfullyFlatDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocal.lean, line 216. The attribute's comment: “taut_is_local_property”.

Tautness descends along a completed étale localization diagram whose upper horizontal ring map is faithfully flat.

public theorem isTaut_faithfullyFlatDescent :
    FaithfullyFlatDescent.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f)

TopologicalRing.isTaut_finiteProductPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocal.lean, line 251. The attribute's comment: “taut_is_local_property”.

Tautness is preserved by finite products of targets.

public theorem isTaut_finiteProductPreserves :
    FiniteProductPreserves.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f)

TopologicalRing.isTaut_isomorphismInvariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocalRefined.lean, line 69. The attribute's comment: “taut_is_local_property”.

Tautness does not depend on the chosen presentations of the source and the target of a continuous homomorphism: pre- and post-composing with bicontinuous ring isomorphisms preserves and reflects tautness.

public theorem isTaut_isomorphismInvariant :
    IsomorphismInvariant.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f)
      IsCountablyWeaklyAdmissible

TopologicalRing.isTaut_completedMap_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocalUnconditional.lean, line 59. The attribute's comment: “axiom 0AND for tautness, the completed corners in WAdm^count by 0ANB”.

Stacks 0ANJ, axiom 0AND for tautness, with the hypotheses of Situation 0CBA only. Given a diagram (0ANC) — A, B countably indexed weakly admissible, A → A' and B → B' étale, φ : B → A and φ' : (B')^∧ → (A')^∧ continuous and commuting with the canonical maps — if φ is taut then so is φ'. The completed corners (A')^∧ and (B')^∧ are objects of WAdm^{count} by Stacks 0ANB (isCountablyWeaklyAdmissible_completionOver), which is how the source reads the axiom.

public theorem isTaut_completedMap_of_isTaut {A B A' B' : Type u}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing A'] [CommRing B'] (D : LocalizationDiagram A B A' B')
    (h : RingHom.IsTaut D.map) : RingHom.IsTaut D.completedMap

TopologicalRing.isTaut_map_of_isTaut_completedMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocalUnconditional.lean, line 74. The attribute's comment: “axiom 0ANE for tautness, the completed corners in WAdm^count by 0ANB”.

Stacks 0ANJ, axiom 0ANE for tautness, with the hypotheses of Situation 0CBA only. Given a diagram (0ANC) whose map A → A' is faithfully flat, if φ' : (B')^∧ → (A')^∧ is taut then so is φ : B → A. The completed corners are objects of WAdm^{count} by Stacks 0ANB (isCountablyWeaklyAdmissible_completionOver).

public theorem isTaut_map_of_isTaut_completedMap {A B A' B' : Type u}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing A'] [CommRing B'] (D : LocalizationDiagram A B A' B')
    (hff : D.toA'.FaithfullyFlat) (h : RingHom.IsTaut D.completedMap) :
    RingHom.IsTaut D.map

TopologicalRing.isTaut_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautIsLocalUnconditional.lean, line 89. The attribute's comment: “axiom 0ANF for tautness”.

Stacks 0ANJ, axiom 0ANF for tautness, stated once: if B → A_i are taut arrows of WAdm^{count} for i in a finite index set, then B → ∏ A_i is taut.

public theorem isTaut_pi {B : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (hB : IsCountablyWeaklyAdmissible B)
    {ι : Type u} [Fintype ι] (A : ι → Type u)
    [∀ i, CommRing (A i)] [∀ i, TopologicalSpace (A i)]
    [∀ i, IsTopologicalRing (A i)] [∀ i, IsLinearTopology (A i) (A i)]
    (hA : ∀ i, IsCountablyWeaklyAdmissible (A i))
    (f : ∀ i, B →+* A i) (hf : ∀ i, Continuous (f i)) (h : ∀ i, RingHom.IsTaut (f i)) :
    RingHom.IsTaut (RingHom.pi f)

Tag 0ANK, a lemma

Tag 0ANK in the Stacks Project.

AlgebraicGeometry.FormalSpace.isTaut_tfae_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautMorphismRepresentability.lean, line 220. The attribute's comment: “the equivalence, with the five inputs this library does not carry as named hypotheses: Stacks 0AJ3 as h0AJ3, the implication (2) implies (1) of Stacks 0AKX for the countably indexed property as h0AKX, the equivalence of conditions (1) and (3) of Stacks 0AN5 read on countably indexed affine charts as h0AN5, Stacks 0AQ0 as h0AQ0, and the implication (5) implies (1) of Stacks 0AN4 as h0AN4”.

Stacks 0ANK. Let f : X ⟶ Y be a morphism of locally countably indexed formal algebraic spaces over S. The following are equivalent:

every commutative square with affine formal algebraic spaces U, V and representable étale maps U ⟶ X, V ⟶ Y has U ⟶ V given by a taut continuous homomorphism of countably indexed weakly admissible topological rings;

there is a covering {Vⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Uᵢ ⟶ Vⱼ ×_Y X} as in Definition 0AIM with each Uᵢ ⟶ Vⱼ given by such a taut map;

there is a covering {Uᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Uᵢ ⟶ Vᵢ ⟶ Y through an affine formal algebraic space representable étale over Y with Uᵢ ⟶ Vᵢ given by such a taut map;

f is representable by algebraic spaces.

The cycle runs (1) ⟹ (2) ⟹ (3) ⟹ (4) ⟹ (1): the first step is Stacks 0ANG, the second is proved here, and the last two pass between tautness and representability on charts through Stacks 0AN5 and between charts and f through Stacks 0AN4.

theorem isTaut_tfae_isRepresentableByAlgebraicSpaces {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (h0AJ3 : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
      IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
    (h0AKX : ∀ (Z : FppfSheaf B S hS), IsLocallyCountablyIndexed B S hS Z →
      ∀ (U : FppfSheaf B S hS) (a : U ⟶ Z), IsAffineFormalAlgebraicSpace B S hS U →
      IsRepresentableEtale B S hS a → IsCountablyIndexed B S hS U)
    (h0AN5 : ∀ {U V : FppfSheaf B S hS} (t : U ⟶ V),
      IsAffineFormalAlgebraicSpace B S hS U → IsAffineFormalAlgebraicSpace B S hS V →
      IsCountablyIndexed B S hS U → IsCountablyIndexed B S hS V →
      (Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS t.hom ↔
        HasPropertyOnAffineChartMap B S hS TopologicalRing.IsCountablyWeaklyAdmissible
          TautChartProperty t))
    (h0AQ0 : ∀ {A A' A'' : FppfSheaf B S hS} (s : A ⟶ A') (r : A' ⟶ A''),
      IsFormalAlgebraicSpace B S hS A → IsFormalAlgebraicSpace B S hS A' →
      IsFormalAlgebraicSpace B S hS A'' →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (s ≫ r).hom →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS s.hom)
    (h0AN4 : ∀ (I : Type (u + 1)) (U W : I → FppfSheaf B S hS) (a : ∀ i, U i ⟶ X)
      (b : ∀ i, W i ⟶ Y) (t : ∀ i, U i ⟶ W i), IsAffineEtaleCover B S hS U a →
      (∀ i, IsAffineFormalAlgebraicSpace B S hS (W i)) →
      (∀ i, Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (b i).hom) →
      (∀ i, Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (t i).hom) →
      (∀ i, a i ≫ f = t i ≫ b i) →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    List.TFAE
      [ IsTautOnEveryAffineEtaleDiagram B S hS f,
        IsTautAfterTargetCover B S hS f,
        IsTautAfterSourceCover B S hS f,
        Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom ]

AlgebraicGeometry.FormalSpace.tfae_isTautOnEveryAffineEtaleDiagram_isRepresentableByAlgebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautMorphismRepresentabilityUnconditional.lean, line 92.

Stacks 0ANK. Let f : X ⟶ Y be a morphism of locally countably indexed formal algebraic spaces over S. The following are equivalent:

every commutative square with affine formal algebraic spaces U, V and representable étale maps U ⟶ X, V ⟶ Y has U ⟶ V given by a taut continuous homomorphism of countably indexed weakly admissible topological rings;

there is a covering {Vⱼ ⟶ Y} as in Definition 0AIM and for each j a covering {Uᵢ ⟶ Vⱼ ×_Y X} as in Definition 0AIM with each Uᵢ ⟶ Vⱼ given by such a taut map;

there is a covering {Uᵢ ⟶ X} as in Definition 0AIM and for each i a factorization Uᵢ ⟶ Vᵢ ⟶ Y through an affine formal algebraic space representable étale over Y with Uᵢ ⟶ Vᵢ given by such a taut map;

f is representable by algebraic spaces.

theorem tfae_isTautOnEveryAffineEtaleDiagram_isRepresentableByAlgebraicSpaces
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y) :
    List.TFAE
      [ IsTautOnEveryAffineEtaleDiagram B S hS f,
        IsTautAfterTargetCover B S hS f,
        IsTautAfterSourceCover B S hS f,
        Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom ]

Sources

LeanRingHom.QuotientDiagram.isTaut_iff_hasQuotientDiagram · TopologicalRing.isTaut_localizationPreserves · TopologicalRing.isTaut_faithfullyFlatDescent · TopologicalRing.isTaut_finiteProductPreserves · TopologicalRing.isTaut_isomorphismInvariant · TopologicalRing.isTaut_completedMap_of_isTaut · TopologicalRing.isTaut_map_of_isTaut_completedMap · TopologicalRing.isTaut_pi

Section87.23 Adic morphisms #

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

Tag 0AQ2, the section

Tag 0AQ2 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAdicOnEveryAffineEtaleDiagram_iff_isTautAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMorphism.lean, line 197. The attribute's comment: “the footnote of the section: on WAdm^{adic*} the adic and the taut reading of the chart condition agree”.

Section 0AQ2, the footnote. On WAdm^{adic*} the chart condition of the section may be read with "adic" or with "taut": the two readings agree, by Stacks 0GBS.

theorem isAdicOnEveryAffineEtaleDiagram_iff_isTautAdicStar {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) :
    IsAdicOnEveryAffineEtaleDiagram B S hS f ↔
      IsTautOnEveryAffineEtaleDiagramAdicStar B S hS f

AlgebraicGeometry.FormalSpace.isAdicOnEveryAffineEtaleDiagram_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMorphism.lean, line 221. The attribute's comment: “the implication from representability by algebraic spaces to the chart condition, through Stacks 0ANK with the five hypotheses that lemma carries in this library; the converse is not proved, since it would need the chart condition at the wider countably indexed weakly admissible class that Stacks 0ANK is stated at”.

Section 0AQ2, condition (1) implies condition (2). A morphism of locally countably indexed formal algebraic spaces over S which is representable by algebraic spaces has every one of its chart maps in WAdm^{adic*} adic; this is the matching the section makes, and it is the content of Definition 0AQ3's reference to the discussion.

Stacks 0ANK turns representability into the taut reading of the chart condition at the countably indexed weakly admissible class, which contains WAdm^{adic*}; the footnote then turns taut into adic. The five hypotheses h0AJ3, h0AKX, h0AN5, h0AQ0 and h0AN4 are those of Stacks 0ANK in this library and are passed straight through.

theorem isAdicOnEveryAffineEtaleDiagram_of_isRepresentable {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y)
    (h0AJ3 : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
      IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
    (h0AKX : ∀ (Z : FppfSheaf B S hS), IsLocallyCountablyIndexed B S hS Z →
      ∀ (U : FppfSheaf B S hS) (a : U ⟶ Z), IsAffineFormalAlgebraicSpace B S hS U →
      IsRepresentableEtale B S hS a → IsCountablyIndexed B S hS U)
    (h0AN5 : ∀ {U V : FppfSheaf B S hS} (t : U ⟶ V),
      IsAffineFormalAlgebraicSpace B S hS U → IsAffineFormalAlgebraicSpace B S hS V →
      IsCountablyIndexed B S hS U → IsCountablyIndexed B S hS V →
      (Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS t.hom ↔
        HasPropertyOnAffineChartMap B S hS TopologicalRing.IsCountablyWeaklyAdmissible
          TautChartProperty t))
    (h0AQ0 : ∀ {A A' A'' : FppfSheaf B S hS} (s : A ⟶ A') (r : A' ⟶ A''),
      IsFormalAlgebraicSpace B S hS A → IsFormalAlgebraicSpace B S hS A' →
      IsFormalAlgebraicSpace B S hS A'' →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (s ≫ r).hom →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS s.hom)
    (h0AN4 : ∀ (I : Type (u + 1)) (U W : I → FppfSheaf B S hS) (a : ∀ i, U i ⟶ X)
      (b : ∀ i, W i ⟶ Y) (t : ∀ i, U i ⟶ W i), IsAffineEtaleCover B S hS U a →
      (∀ i, IsAffineFormalAlgebraicSpace B S hS (W i)) →
      (∀ i, Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (b i).hom) →
      (∀ i, Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (t i).hom) →
      (∀ i, a i ≫ f = t i ≫ b i) →
      Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) :
    IsAdicOnEveryAffineEtaleDiagram B S hS f

AlgebraicGeometry.FormalSpace.isAdicMorphism_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMorphismConverse.lean, line 250. The attribute's comment: “the equivalence of conditions (1) and (2) of the section for a morphism of locally adic* formal algebraic spaces, together with the footnote reading (2) with taut maps”.

Section 0AQ2. Let f : X ⟶ Y be a morphism of locally adic* formal algebraic spaces over S. The following are equivalent:
f is representable by algebraic spaces, that is, f is an adic morphism in the sense of Definition 0AQ3;
for every commutative square
U ⟶ V
↓     ↓
X ⟶ Y
with U and V affine formal algebraic spaces and U ⟶ X, V ⟶ Y representable by algebraic spaces and étale, the morphism U ⟶ V corresponds to an adic map in WAdm^{adic*};
the same with "adic" replaced by "taut", which is the footnote of the section.

theorem isAdicMorphism_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyAdicStar B S hS X) (hY : IsLocallyAdicStar B S hS Y) :
    List.TFAE
      [ IsAdicMorphism B S hS f,
        IsAdicOnEveryAffineEtaleDiagram B S hS f,
        IsTautOnEveryAffineEtaleDiagramAdicStar B S hS f ]

Tag 0GBS, a lemma

Tag 0GBS in the Stacks Project.

RingHom.isTaut_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 436. The attribute's comment: “part (1)”.

A continuous adic homomorphism of linearly topologized rings is taut.

public theorem isTaut_of_isAdic
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ) (hAdic : RingHom.IsAdic φ) :
    RingHom.IsTaut φ

RingHom.isAdic_iff_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 467. The attribute's comment: “on WAdm^{adic*}”.

Adicness and tautness are equivalent for a continuous homomorphism from a linearly topologized ring with a finitely generated ideal of definition to a complete separated linearly topologized ring. In particular, this applies to morphisms in WAdm^{adic*}.

public theorem isAdic_iff_isTaut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ)
    (hA : ∃ I : Ideal A, I.FG ∧ _root_.IsAdic I)
    [@CompleteSpace B (IsTopologicalAddGroup.rightUniformSpace B)] [T2Space B] :
    RingHom.IsAdic φ ↔ RingHom.IsTaut φ

Declarations registered for the tag:

RingHom.isAdic_of_isTaut, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 461 (StacksFrontier): “part (2)”.
RingHom.isAdic_of_isTaut, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMapRefined.lean, line 137 (StacksFrontier): “part (2)”.

Tag 0AQ3, a definition

Tag 0AQ3 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsAdicMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMorphism.lean, line 131.

Stacks 0AQ3. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S with X and Y locally adic*. Then f is an adic morphism when f is representable by algebraic spaces.

The locally adic* hypotheses on X and Y are the standing assumptions under which the source introduces the terminology; as for Stacks 0AQM they are imposed by the results that use the predicate rather than built into it, so that the predicate is the defining condition and nothing more.

abbrev IsAdicMorphism {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/RepresentableByAlgebraicSpaces.lean, line 85. The attribute's comment: “the defining condition of an adic morphism”.

Stacks Project, Tag 02YQ. A morphism of presheaves is representable by algebraic spaces if its pullback to every scheme over the base is an algebraic space.

abbrev IsRepresentableByAlgebraicSpaces (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) : Prop

Sources

LeanAlgebraicGeometry.FormalSpace.isAdicOnEveryAffineEtaleDiagram_iff_isTautAdicStar · AlgebraicGeometry.FormalSpace.isAdicOnEveryAffineEtaleDiagram_of_isRepresentable · AlgebraicGeometry.FormalSpace.isAdicMorphism_tfae · RingHom.isTaut_of_isAdic · RingHom.isAdic_iff_isTaut · RingHom.isAdic_of_isTaut · AlgebraicGeometry.FormalSpace.IsAdicMorphism · AlgebraicGeometry.Space.IsRepresentableByAlgebraicSpaces

Section87.24 Morphisms of finite type #

Section 87.24 of the Stacks Project, Tag 0AM3. 9 tags here are carried by 42 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AM4, a definition

Tag 0AM4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 82. The attribute's comment: “part (1): locally of finite type”.

A morphism of formal algebraic spaces over S is locally of finite type when it is representable by algebraic spaces and every base change of it along a scheme-valued point of its target is a morphism of algebraic spaces which is locally of finite type. The condition is stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsLocallyOfFiniteType {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.IsFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 94. The attribute's comment: “part (2): finite type”. References: EGA I (10.13.3), “representable morphisms”.

A morphism of formal algebraic spaces over S is of finite type when it is representable by algebraic spaces and every base change of it along a scheme-valued point of its target is a morphism of algebraic spaces which is of finite type. The condition is stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsFiniteType {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.IsFiniteType', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeQuasiCompact.lean, line 92. The attribute's comment: “part (2): finite type”. References: EGA I (10.13.3), “representable morphisms”.

Stacks 0AM4, part (2), which is Stacks 0AJJ, condition (1). A morphism of formal algebraic spaces over S is of finite type when it is locally of finite type, in the sense of Definition 0AM4, part (1), and quasi-compact, in the sense of Definition 0AJC. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsFiniteType' {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

Tag 0AJJ, a lemma

Tag 0AJJ in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 94. The attribute's comment: “representable plus Bootstrap finite type”. References: EGA I (10.13.3), “representable morphisms”.

A morphism of formal algebraic spaces over S is of finite type when it is representable by algebraic spaces and every base change of it along a scheme-valued point of its target is a morphism of algebraic spaces which is of finite type. The condition is stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsFiniteType {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.IsBootstrapFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 105. The attribute's comment: “condition (2): representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ”.

A morphism of formal algebraic spaces over S is representable by algebraic spaces and of finite type in the bootstrap sense of Stacks 03XZ when every base change of it along a scheme-valued point of its target is a morphism of algebraic spaces which is of finite type. The condition is stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsBootstrapFiniteType {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.IsFiniteType', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeQuasiCompact.lean, line 92. The attribute's comment: “condition (1): of finite type”. References: EGA I (10.13.3), “representable morphisms”.

Stacks 0AM4, part (2), which is Stacks 0AJJ, condition (1). A morphism of formal algebraic spaces over S is of finite type when it is locally of finite type, in the sense of Definition 0AM4, part (1), and quasi-compact, in the sense of Definition 0AJC. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsFiniteType' {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiCompactMorphismComparison.lean, line 185. The attribute's comment: “the equivalence of conditions (1) and (2), for an arbitrary morphism of fppf sheaves, representability by algebraic spaces being part of both conditions rather than a hypothesis”.

Stacks 0AJJ. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S. Then f is of finite type — locally of finite type and quasi-compact in the sense of Definition 0AJC — exactly when it is representable by algebraic spaces and of finite type in the Bootstrap sense of Stacks 03XZ.

Both conditions contain being locally of finite type: the Bootstrap condition for being of finite type is the conjunction of the Bootstrap condition for being locally of finite type with the Bootstrap condition for being quasi-compact, which is the content of Stacks 03XF, part (3), in the universe-lifted form of StacksFrontier.AlgebraicGeometry.Spaces.LargeValuedFiniteType. What is left is the comparison of Definition 0AJC with the Bootstrap condition for being quasi-compact, which is Stacks 0AM2 above. The witnesses that the source and the target are formal algebraic spaces are not used, so the statement is for an arbitrary morphism of fppf sheaves; each condition carries its own representability witness, so representability is not a hypothesis.

theorem isFiniteType_iff_isBootstrapFiniteType {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsFiniteType' B S hS f ↔ IsBootstrapFiniteType B S hS f

Tag 0AQ4, a lemma

Tag 0AQ4 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 162. The attribute's comment: “locally of finite type”.

A composition of morphisms of formal algebraic spaces over S which are locally of finite type is locally of finite type.

theorem IsLocallyOfFiniteType.comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g)

AlgebraicGeometry.FormalSpace.IsFiniteType.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 196. The attribute's comment: “finite type”.

A composition of morphisms of formal algebraic spaces over S which are of finite type is of finite type.

theorem IsFiniteType.comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsFiniteType B S hS f) (hg : IsFiniteType B S hS g) :
    IsFiniteType B S hS (f ≫ g)

AlgebraicGeometry.FormalSpace.IsBootstrapFiniteType.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 237. The attribute's comment: “finite type, proved for condition (2) of Stacks 0AJJ — representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ — rather than for Definition 0AM4, part (2), verbatim, which is defined further up the import order: the two are identified unconditionally by Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType”.

A composition of morphisms of formal algebraic spaces over S which are representable by algebraic spaces and of finite type in the bootstrap sense of Stacks 03XZ is again such.

theorem IsBootstrapFiniteType.comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsBootstrapFiniteType B S hS f) (hg : IsBootstrapFiniteType B S hS g) :
    IsBootstrapFiniteType B S hS (f ≫ g)

Tag 0AQ5, a lemma

Tag 0AQ5 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 127. The attribute's comment: “locally of finite type”.

A base change of a morphism of formal algebraic spaces over S which is locally of finite type is locally of finite type.

theorem IsLocallyOfFiniteType.of_isPullback {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteType B S hS p

AlgebraicGeometry.FormalSpace.IsFiniteType.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 140. The attribute's comment: “finite type”.

A base change of a morphism of formal algebraic spaces over S which is of finite type is of finite type.

theorem IsFiniteType.of_isPullback {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsFiniteType B S hS f) :
    IsFiniteType B S hS p

AlgebraicGeometry.FormalSpace.IsFiniteType.of_isPullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeQuasiCompact.lean, line 99. The attribute's comment: “finite type”.

Stacks 0AQ5, the global half. A base change of a morphism of formal algebraic spaces over S which is of finite type is of finite type: both halves of the condition are stable under base change.

theorem IsFiniteType.of_isPullback' {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsFiniteType' B S hS f) :
    IsFiniteType' B S hS p

Tag 0AQ6, a lemma

Tag 0AQ6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 341. The attribute's comment: “stated for arbitrary fppf sheaves, only the source of the second morphism being assumed a formal algebraic space”.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Y a formal algebraic space. If f ≫ g is locally of finite type then so is f.

theorem IsLocallyOfFiniteType.of_comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g)) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.of_comp_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteType.lean, line 377. The attribute's comment: “for a second morphism whose source is an affine formal algebraic space”.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of fppf sheaves on the big fppf site of S with Y an affine formal algebraic space. If f ≫ g is locally of finite type then so is f.

theorem IsLocallyOfFiniteType.of_comp_of_isAffineFormal {X Y Z : FppfSheaf B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hY : IsAffineFormalAlgebraicSpace B S hS Y)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g)) :
    IsLocallyOfFiniteType B S hS f

Tag 0ANL, a lemma

Tag 0ANL in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_square_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeAfterTargetCover.lean, line 70. The attribute's comment: “condition (1) implies condition (3), for a square whose chart of the target is an affine formal algebraic space: the general implication needs the locally of finite type assertion of Stacks 0AN2 for the relative diagonal of a morphism of formal algebraic spaces, which this library has only for a morphism whose source is an affine formal algebraic space, and that is the case the source's own proof of condition (4) uses”.

Stacks 0ANL, condition (1) implies condition (3), for a square whose chart of the target is an affine formal algebraic space. If f is locally of finite type and the square

p ≫ f = t ≫ q

has p representable étale and V, the source of its target column, an affine formal algebraic space, then t is locally of finite type.

This is the implication the general (1) ⟹ (3) is blocked on, in the generality the source's own proof of condition (4) uses it: there the chart Vⱼ of the target is affine. The two steps are both unconditional. First t ≫ q = p ≫ f is locally of finite type, p being locally of finite type by Stacks 0AJG and composition being Stacks 0AQ4. Then the cancellation of Stacks 0AQ6 removes q: it needs the locally-of-finite-type assertion of Stacks 0AN2 for the relative diagonal of q, which AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType .of_comp_of_isAffineFormal supplies from affineness of V.

Neither column of the square is asked to be surjective, q is not asked to be representable étale, and U and V are not asked to be formal algebraic spaces beyond affineness of V.

theorem isLocallyOfFiniteType_square_of_isAffineFormal {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (U V : FppfSheaf B S hS) (p : U ⟶ X) (q : V ⟶ Y)
    (t : U ⟶ V) (hV : IsAffineFormalAlgebraicSpace B S hS V)
    (hp : IsRepresentableEtale B S hS p) (hsq : p ≫ f = t ≫ q) :
    IsLocallyOfFiniteType B S hS t

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAfterTargetCover_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeAfterTargetCover.lean, line 98. The attribute's comment: “condition (1) implies condition (4), for a morphism of formal algebraic spaces, with nothing assumed: the fibre product of a chart of the target with the morphism is a formal algebraic space by the étale case of Stacks 0AJ3, isFormalAlgebraicSpace_pullback_of_isRepresentableEtale”.

Stacks 0ANL, condition (1) implies condition (4). The atlas of the target and the atlases of the fibre products of its members with the source witness condition (4) directly, without going through condition (3): the chart Vⱼ of the target is an affine formal algebraic space, so isLocallyOfFiniteType_square_of_isAffineFormal applies to the square the chart Uⱼᵢ of Vⱼ ×_Y X forms with f and Vⱼ ⟶ Y.

This is the implication the proof of Stacks 0GBB clause (5) consumes, where f is the morphism X_red ⟶ Y_red on the reductions. Previously only condition (3) implied condition (4), and condition (3) was reachable from nothing.

The fibre product Vⱼ ×_Y X is a formal algebraic space by the étale case of Stacks 0AJ3, AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_pullback_of_isRepresentableEtale, since X is a formal algebraic space and the chart Vⱼ ⟶ Y is representable étale.

theorem isLocallyOfFiniteTypeAfterTargetCover_of_isLocallyOfFiniteType {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteTypeAfterTargetCover B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnSomeSquare_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTarget.lean, line 151. The attribute's comment: “condition (1) implies condition (2), reading surjectivity of the source column as surjectivity of the morphism of sheaves”.

Stacks 0ANL, condition (1) implies condition (2). The square formed by the identities of X and of Y witnesses condition (2): both columns are identities, hence representable étale and surjective, and the upper horizontal map is f itself.

theorem isLocallyOfFiniteTypeOnSomeSquare_of_isLocallyOfFiniteType {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteTypeOnSomeSquare B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_of_onEverySquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTarget.lean, line 164. The attribute's comment: “condition (3) implies condition (1), by instantiating condition (3) at the square formed by the identities”.

Stacks 0ANL, condition (3) implies condition (1). Condition (3), instantiated at the square formed by the identities of X and of Y, asserts that f itself is locally of finite type.

theorem isLocallyOfFiniteType_of_onEverySquare {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteTypeOnEverySquare B S hS f) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnSomeSquare_of_onEverySquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTarget.lean, line 174. The attribute's comment: “condition (3) implies condition (2)”.

Stacks 0ANL, condition (3) implies condition (2). Condition (3) gives that f is locally of finite type, and the identity square then witnesses condition (2).

theorem isLocallyOfFiniteTypeOnSomeSquare_of_onEverySquare {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteTypeOnEverySquare B S hS f) :
    IsLocallyOfFiniteTypeOnSomeSquare B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAfterTargetCover_of_onEverySquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTarget.lean, line 192. The attribute's comment: “condition (3) implies condition (4), with Stacks 0AJ3 — that the fibre product of a chart of the target with the morphism is a formal algebraic space — carried as the hypothesis h0AJ3, since this library does not have it”.

Stacks 0ANL, condition (3) implies condition (4). The atlas of the target and the atlases of the fibre products of its members with the source witness condition (4): a chart Uⱼᵢ of Vⱼ ×_Y X maps to X by a representable étale morphism, because the second projection is a base change of Vⱼ ⟶ Y, and the square it forms with f and Vⱼ ⟶ Y commutes by the universal property of the fibre product.

The hypothesis h0AJ3 is the assertion of Stacks 0AJ3 that Vⱼ ×_Y X is a formal algebraic space, which this library does not carry.

theorem isLocallyOfFiniteTypeAfterTargetCover_of_onEverySquare {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hY : IsFormalAlgebraicSpace B S hS Y)
    (h0AJ3 : ∀ (V : FppfSheaf B S hS) (v : V ⟶ Y), IsAffineFormalAlgebraicSpace B S hS V →
      IsRepresentableEtale B S hS v → IsFormalAlgebraicSpace B S hS (pullback v f))
    (hf : IsLocallyOfFiniteTypeOnEverySquare B S hS f) :
    IsLocallyOfFiniteTypeAfterTargetCover B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnFactoredAtlas_of_afterTargetCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTarget.lean, line 223. The attribute's comment: “condition (4) implies condition (5), with the assertion that the composite of a covering of the target with coverings of the fibre products is again a covering as in Definition 0AIM carried as the hypothesis h0AIM”.

Stacks 0ANL, condition (4) implies condition (5). Composing the coverings of the fibre products Vⱼ ×_Y X with the second projections gives a covering of X indexed by the pairs (j, i), and the member Uⱼᵢ ⟶ X of it factors as Uⱼᵢ ⟶ Vⱼ ⟶ Y over f through the first projection, which condition (4) asserts to be locally of finite type.

The hypothesis h0AIM is that the composite family is again a covering as in Definition 0AIM. Its affineness clause is inherited from the given coverings and its representable étaleness clause follows from AlgebraicGeometry.FormalSpace.IsRepresentableEtale.comp together with AlgebraicGeometry.FormalSpace.isRepresentableEtale_pullback_snd; what the library does not carry is the joint surjectivity of the composite family.

theorem isLocallyOfFiniteTypeOnFactoredAtlas_of_afterTargetCover {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y)
    (h0AIM : ∀ (J : Type (u + 1)) (V : J → FppfSheaf B S hS) (v : ∀ j, V j ⟶ Y),
      IsAffineEtaleCover B S hS V v → ∀ (I : J → Type (u + 1))
        (U : ∀ j, I j → FppfSheaf B S hS) (w : ∀ j i, U j i ⟶ pullback (v j) f),
        (∀ j, IsAffineEtaleCover B S hS (U j) (w j)) →
        IsAffineEtaleCover B S hS (fun ji : Σ j, I j ↦ U ji.1 ji.2)
          (fun ji ↦ w ji.1 ji.2 ≫ pullback.snd (v ji.1) f))
    (hf : IsLocallyOfFiniteTypeAfterTargetCover B S hS f) :
    IsLocallyOfFiniteTypeOnFactoredAtlas B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnEverySquare_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 61. The attribute's comment: “condition (1) implies condition (3)”.

A morphism f : X ⟶ Y locally of finite type is locally of finite type on every square: for representable étale p : U ⟶ X and q : V ⟶ Y from formal algebraic spaces and t : U ⟶ V with p ≫ f = t ≫ q, the map t is locally of finite type.

theorem isLocallyOfFiniteTypeOnEverySquare_of_isLocallyOfFiniteType {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteTypeOnEverySquare B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeOnFactoredAtlas_of_afterTargetCover', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 76. The attribute's comment: “condition (4) implies condition (5)”.

If f : X ⟶ Y is locally of finite type after a target cover, then it is locally of finite type on a factored atlas: there is an affine étale covering of X each member of which factors through an affine formal algebraic space representable étale over Y by a map locally of finite type.

theorem isLocallyOfFiniteTypeOnFactoredAtlas_of_afterTargetCover' {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteTypeAfterTargetCover B S hS f) :
    IsLocallyOfFiniteTypeOnFactoredAtlas B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAfterTargetCover_of_onEverySquare', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 98. The attribute's comment: “condition (3) implies condition (4)”.

Let X, Y be formal algebraic spaces. If f : X ⟶ Y is locally of finite type on every square, then it is locally of finite type after a target cover: there is an affine étale covering {Vⱼ ⟶ Y} and, for each j, an affine étale covering of Vⱼ ×_Y X whose members are locally of finite type over Vⱼ.

theorem isLocallyOfFiniteTypeAfterTargetCover_of_onEverySquare' {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteTypeOnEverySquare B S hS f) :
    IsLocallyOfFiniteTypeAfterTargetCover B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_of_onSomeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 161. The attribute's comment: “condition (2) implies condition (1), reading surjectivity of the source column as surjectivity of the morphism of sheaves”.

A morphism f : X ⟶ Y which is locally of finite type on some square is locally of finite type: it suffices that p ≫ f = t ≫ q for a surjective representable étale p : U ⟶ X, a representable étale q : V ⟶ Y from formal algebraic spaces and t : U ⟶ V locally of finite type.

theorem isLocallyOfFiniteType_of_onSomeSquare {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteTypeOnSomeSquare B S hS f) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_of_onFactoredAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 174. The attribute's comment: “condition (5) implies condition (1), reading the covering of Definition 0AIM as a jointly surjective family of morphisms of sheaves”.

Let X, Y be formal algebraic spaces and f : X ⟶ Y. If there is an affine étale covering {Uᵢ ⟶ X} each member of which factors as Uᵢ ⟶ Vᵢ ⟶ Y through an affine formal algebraic space representable étale over Y by a map locally of finite type, then f is locally of finite type.

theorem isLocallyOfFiniteType_of_onFactoredAtlas {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteTypeOnFactoredAtlas B S hS f) :
    IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_tfae_squares, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeLocalOnSourceAndTargetRefined.lean, line 188. The attribute's comment: “the equivalence of conditions (1), (2) and (3)”.

For a morphism f : X ⟶ Y of formal algebraic spaces, the following are equivalent: f is locally of finite type; f is locally of finite type on some square; f is locally of finite type on every square.

theorem isLocallyOfFiniteType_tfae_squares {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    List.TFAE [IsLocallyOfFiniteType B S hS f,
      IsLocallyOfFiniteTypeOnSomeSquare B S hS f,
      IsLocallyOfFiniteTypeOnEverySquare B S hS f]

Tag 0ANM, an example

Tag 0ANM in the Stacks Project.

AlgebraicGeometry.FormalSpace.existsUnique_quotientCompletionEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteType.lean, line 86. The attribute's comment: “the quotient of the relative completion at a weak ideal of definition”.

The quotient of the relative completion A^ by the kernel of its projection to A / JA is canonically A / JA, by the unique isomorphism compatible with that projection.

theorem existsUnique_quotientCompletionEquiv
    {B A : Type u} [CommRing B] [TopologicalSpace B] [CommRing A] (f : B →+* A)
    (J : TopologicalRing.WeakIdealOfDefinitionIndex B) :
    ∃! e : (TopologicalRing.CompletionOver f ⧸
        RingHom.ker (TopologicalRing.CompletionOver.projection f J)) ≃+*
          (A ⧸ TopologicalRing.extendedIdeal f J),
      ∀ x : TopologicalRing.CompletionOver f,
        e (Ideal.Quotient.mk _ x) = TopologicalRing.CompletionOver.projection f J x

AlgebraicGeometry.FormalSpace.exists_completionOver_quotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteType.lean, line 375. The attribute's comment: “the induced quotient system and continuous map of the relative completion”.

Stacks 0ANM. A finite type ring map out of a weakly admissible topological ring over S gives the relative completion a quotient system over S and a continuous map from the base whose underlying ring map is the canonical one.

theorem exists_completionOver_quotientSystem
    [IsTopologicalRing B] [IsLinearTopology B B]
    (f : B →+* A) (hf : letI : Algebra B A := f.toAlgebra; Algebra.FiniteType B A)
    (hB : TopologicalRing.IsWeaklyAdmissible B)
    (D : QuotientSystem 𝔅 S hS B) (hD : D.HasLargeSite) :
    ∃ (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
      (g : ContinuousHom D E),
      g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f

AlgebraicGeometry.FormalSpace.ker_projection_eq_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteType.lean, line 572. The attribute's comment: “the affine base change of the completion along a quotient stage”.

For an open ideal L of the relative completion inside the kernel of the projection at J, that kernel is the sum of L and the ideal generated by the image of J. This is the identity ker (A^ → A / JA) = J·A^ + L, which holds because the kernel is the closure of J·A^ and L is open.

theorem ker_projection_eq_sup {B A : Type u} [CommRing B] [TopologicalSpace B]
    [CommRing A] (f : B →+* A) (J : TopologicalRing.WeakIdealOfDefinitionIndex B)
    (L : Ideal (TopologicalRing.CompletionOver f))
    (hLopen : IsOpen (L : Set (TopologicalRing.CompletionOver f)))
    (hL : L ≤ RingHom.ker (TopologicalRing.CompletionOver.projection f J)) :
    RingHom.ker (TopologicalRing.CompletionOver.projection f J) =
      J.1.map (TopologicalRing.CompletionOver.canonicalMap f) ⊔ L

AlgebraicGeometry.FormalSpace.isPullback_specMap_kerProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteType.lean, line 675. The attribute's comment: “the affine base change of the completion along a quotient stage”.

Stacks 0ANM. The affine base change of the relative completion along a quotient stage: Spec (A / JA) = Spec (B / J) ×_{Spec (B / M)} Spec (A^ / L), for an open ideal L of A^ inside ker (A^ → A / JA) and an ideal M ⊆ J of B whose image lies in L.

theorem isPullback_specMap_kerProjection {B A : Type u} [CommRing B]
    [TopologicalSpace B] [CommRing A] (f : B →+* A)
    (J : TopologicalRing.WeakIdealOfDefinitionIndex B)
    {M : Ideal B} {L : Ideal (TopologicalRing.CompletionOver f)}
    (hMJ : M ≤ J.1) (hLopen : IsOpen (L : Set (TopologicalRing.CompletionOver f)))
    (hLK : L ≤ RingHom.ker (TopologicalRing.CompletionOver.projection f J))
    (hML : M ≤ Ideal.comap (TopologicalRing.CompletionOver.canonicalMap f) L) :
    IsPullback
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor hLK)))
      (Spec.map (CommRingCat.ofHom (Ideal.quotientMap
        (RingHom.ker (TopologicalRing.CompletionOver.projection f J))
        (TopologicalRing.CompletionOver.canonicalMap f) (le_comap_ker_projection f J))))
      (Spec.map (CommRingCat.ofHom (Ideal.quotientMap L
        (TopologicalRing.CompletionOver.canonicalMap f) hML)))
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor hMJ)))

AlgebraicGeometry.FormalSpace.isPullback_formalSpectrumMap_kerProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteType.lean, line 1032. The attribute's comment: “the base change of the completion along a quotient stage”.

Stacks 0ANM. The base change of the formal spectrum of the relative completion along a quotient stage of the base is the spectrum of the corresponding quotient of A, that is Spec (A / JA) = Spec (B / J) ×_{Spf B} Spf A^.

theorem isPullback_formalSpectrumMap_kerProjection
    (hB : TopologicalRing.IsWeaklyAdmissible B) (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f)
    (J : TopologicalRing.WeakIdealOfDefinitionIndex B)
    (hJK : J.1 ≤ Ideal.comap g.toRingHom (kerProjectionIdeal f J).1) :
    IsPullback
      ((Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).map
        ((BigAffineFppf.inclusion 𝔅 S hS).map
          (g.stageMap J (kerProjectionIdeal f J) hJK)))
      (formalSpectrumInclusion E (OrderDual.toDual (kerProjectionIdeal f J)))
      (formalSpectrumInclusion D (OrderDual.toDual J))
      (formalSpectrumMap hB g)

TopologicalRing.finiteTypeModuloEveryWeakIdeal_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 147. The attribute's comment: “the relative completion along a finite type ring map is taut and of finite type modulo every weak ideal of definition of the base, which is the ring-theoretic content of the identification T ×_{Spf A} Spf ((A')^) = T ×_{Spec (A / I)} Spec (A' / IA')”.

Stacks 0ANM. Let B be a weakly pre-admissible linearly topologized ring and let f : B →+* A be a finite type ring map. The canonical map from B to the relative completion A^ = lim_J A ⧸ JA is taut, and for every weak ideal of definition J of B the induced map B ⧸ J → A^ ⧸ J A^ is of finite type; indeed A^ ⧸ J A^ = A ⧸ JA. This is condition (a) of Stacks 0ANU for the canonical map.

theorem finiteTypeModuloEveryWeakIdeal_canonicalMap [IsTopologicalRing B]
    [IsLinearTopology B B] (f : B →+* A) (hB : IsWeaklyPreAdmissible B) (hf : f.FiniteType) :
    FiniteTypeModuloEveryWeakIdeal (CompletionOver.canonicalMap f)

AlgebraicGeometry.FormalSpace.exists_isPullback_isFiniteType_formalSpectrumMap_completionOver_of_compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 313. The attribute's comment: “the base change identification: for a point of Spf A out of a quasi-compact scheme T of the site, T ×_{Spf A} Spf ((A')^) is represented by the object T ×_{Spec (A / I)} Spec (A' / IA') of the site, and its projection to T is of finite type”.

Stacks 0ANM, the representability and the finite type assertions, at a point of Spf B out of a quasi-compact scheme. Let B be a weakly admissible topological ring over S, let f : B →+* A be a finite type ring map and let g present the canonical map B ⟶ A^ to the relative completion as a morphism of quotient systems over S. For every point T ⟶ Spf B whose source is a quasi-compact object of the site, the base change T ×_{Spf B} Spf A^ is represented by an object V of the site — the source's T ×_{Spec (B / I)} Spec (A / IA) — and the projection V ⟶ T is of finite type.

This is the source's own argument: the point factors through a stage Spec (B / I) ⟶ Spf B by Stacks 0AIA, the base change along the factorisation is T ×_{Spec (B / I)} Spec (A / IA), and Spec (A / IA) ⟶ Spec (B / I) is of finite type because B / I → A / IA is.

theorem exists_isPullback_isFiniteType_formalSpectrumMap_completionOver_of_compactSpace
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyAdmissible B) (hf : f.FiniteType)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E) (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f)
    (U : BigFppfOver 𝔅 S hS) (hU : CompactSpace ((BigFppfOver.toScheme 𝔅 S hS).obj U))
    (a : (Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).obj U ⟶ formalSpectrum D) :
    ∃ (V : BigFppfOver 𝔅 S hS) (q : V ⟶ U)
      (r : (Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).obj V ⟶ formalSpectrum E),
      IsPullback r ((Sheaf.sheafifiedYoneda (BigFppfOver.topology 𝔅 S hS)).map q)
        (formalSpectrumMap hB g) a ∧
      Space.IsFiniteTypeULift.{u + 1} 𝔅 S hS ((uliftYoneda.{u + 1}).map q)

AlgebraicGeometry.FormalSpace.isRepresentableByAlgebraicSpacesULift_formalSpectrumMap_completionOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 367. The attribute's comment: “representability of Spf ((A')^) → Spf A: the morphism is representable by algebraic spaces over S, with no restriction on the scheme-valued point of Spf A along which the base change is taken”.

Stacks 0ANM, the representability assertion. Let B be a weakly admissible topological ring over S, let f : B →+* A be a finite type ring map and let g present the canonical map B ⟶ A^ to the relative completion as a morphism of quotient systems over S. Then Spf A^ ⟶ Spf B is representable by algebraic spaces, which is condition (1) of Stacks 0AN5 and the assertion Stacks 0AN6 makes about this morphism.

theorem isRepresentableByAlgebraicSpacesULift_formalSpectrumMap_completionOver
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyAdmissible B) (hf : f.FiniteType)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f) :
    Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} 𝔅 S hS
      (formalSpectrumMap hB g).hom

AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_completionOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 393. The attribute's comment: “finite type of Spf ((A')^) → Spf A: the morphism is of finite type, with no restriction on the scheme-valued point of Spf A along which the base change is taken. The base change along a point out of a quasi-compact scheme T is the source's T ×_{Spec (A / I)} Spec (A' / IA')”.

Stacks 0ANM, the finite type assertion. With B, f and g as above, Spf A^ ⟶ Spf B is of finite type: it is representable by algebraic spaces and every base change of it along a scheme-valued point of Spf B is a morphism of algebraic spaces which is of finite type.

The source's argument is the quasi-compact one — a point out of a quasi-compact scheme factors through a thickening stage by Stacks 0AIA, and the base change along the factorisation is T ×_{Spec (B / I)} Spec (A / IA). The passage from there to an arbitrary scheme-valued point is the locality of the two halves of being of finite type on the target, AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeULift_pullback_of_compact_pullback and AlgebraicGeometry.FormalSpace.isQuasiCompactULift_of_compact_pullback.

theorem isFiniteType_formalSpectrumMap_completionOver
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyAdmissible B) (hf : f.FiniteType)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f) :
    IsFiniteType 𝔅 S hS (formalSpectrumMap hB g)

AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_completionOver', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExampleUnconditional.lean, line 120. The attribute's comment: “finite type of Spf ((A')^) → Spf A: the morphism is of finite type as Definition 0AM4, part (2), verbatim. What the argument produces is condition (2) of Stacks 0AJJ — representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ — and Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, carries it to Definition 0AM4, part (2), unconditionally. With no restriction on the scheme-valued point of Spf A along which the base change is taken; the base change along a point out of a quasi-compact scheme T is the source's T ×_{Spec (A / I)} Spec (A' / IA')”.

Let f : B →+* A be a finite type ring map over a weakly admissible topological ring B, and g a continuous homomorphism whose underlying ring map is the canonical map B → A^ to the relative completion. Then Spf A^ ⟶ Spf B is of finite type in the sense of Definition 0AM4, part (2): locally of finite type — representable by algebraic spaces, with every base change of it along a scheme-valued point of Spf B a morphism of algebraic spaces which is locally of finite type — and quasi-compact in the sense of Definition 0AJC.

theorem isFiniteType_formalSpectrumMap_completionOver'
    (f : B →+* A) (hB : TopologicalRing.IsWeaklyAdmissible B) (hf : f.FiniteType)
    (D : QuotientSystem 𝔅 S hS B)
    (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
    (g : ContinuousHom D E)
    (hg : g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f) :
    IsFiniteType' 𝔅 S hS (formalSpectrumMap hB g)

AlgebraicGeometry.FormalSpace.exists_completionOver_quotientSystem_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeQuotientSystem.lean, line 154. The attribute's comment: “the induced quotient system and continuous map of the relative completion, with no size hypothesis on the site”.

Stacks 0ANM, with no size hypothesis on the site. A finite type ring map out of a weakly admissible topological ring over S gives the relative completion a quotient system over S and a continuous map from the base whose underlying ring map is the canonical one. The stages Spec (A / JA) lie in the site because Spec (B / J) does and B / J → A / JA is of finite type.

theorem exists_completionOver_quotientSystem_of_finiteType
    [IsTopologicalRing B] [IsLinearTopology B B]
    (f : B →+* A) (hf : letI : Algebra B A := f.toAlgebra; Algebra.FiniteType B A)
    (hB : TopologicalRing.IsWeaklyAdmissible B) (D : QuotientSystem 𝔅 S hS B) :
    ∃ (E : QuotientSystem 𝔅 S hS (TopologicalRing.CompletionOver f))
      (g : ContinuousHom D E),
      g.toRingHom = TopologicalRing.CompletionOver.canonicalMap f

Declarations registered for the tag:

completionOver_isWeaklyAdmissible registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 156 (StacksFrontier): “the relative completion of a ring map over a weakly admissible topological ring is weakly admissible; no finite type hypothesis is needed”.
isTopologicallyOfFiniteType_canonicalMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExample.lean, line 160 (StacksFrontier): “the relative completion along a finite type ring map is topologically of finite type over the base, which is the ring-theoretic form of the finite type assertion”.
completionOver_isWeaklyAdmissible registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExampleUnconditional.lean, line 39 (StacksFrontier): “the relative completion of a ring map over a weakly admissible topological ring is weakly admissible; no finite type hypothesis is needed”.
isTopologicallyOfFiniteType_canonicalMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/CompletionFiniteTypeExampleUnconditional.lean, line 43 (StacksFrontier): “the relative completion along a finite type ring map is topologically of finite type over the base, which is the ring-theoretic form of the finite type assertion”.

Tag 0AQ7, a lemma

Tag 0AQ7 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_source_of_isLocallyOfFiniteType', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeNoetherianRefined.lean, line 44.

Stacks 0AQ7. If Y is a locally Noetherian formal algebraic space over S and f : X ⟶ Y is a morphism of formal algebraic spaces over S which is locally of finite type, then X is locally Noetherian.

The atlas of Y by Noetherian affine formal algebraic spaces base changes to a family of fibre products covering X, and the atlases of those fibre products assemble into an atlas of X. Its members are locally of finite type over the members of the atlas of Y by Stacks 0ANL, condition (1) implies condition (3), hence Noetherian by clause (5) of Stacks 0AKQ, which Stacks 0AKN makes unconditional.

The fibre products Vⱼ ×_Y X are formal algebraic spaces by Stacks 0AJ3, which this library proves outright for a base which is a formal algebraic space.

theorem isLocallyNoetherian_source_of_isLocallyOfFiniteType'
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsLocallyNoetherian B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyNoetherian B S hS X

Tag 0AQ8, a lemma

Tag 0AQ8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_of_isPullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeNoetherianRefined.lean, line 104. The attribute's comment: “stated for an arbitrary cartesian square over Y rather than for the chosen fibre product Z ×_Y X”.

Stacks 0AQ8. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of formal algebraic spaces over S. If Z is locally Noetherian and f is locally of finite type, then Z ×_Y X is locally Noetherian.

The projection p : Z ×_Y X ⟶ Z is a base change of f, so it is locally of finite type by Stacks 0AQ5, and Z ×_Y X is a formal algebraic space by Stacks 0AJ3; Stacks 0AQ7 applies to p. The fibre product is presented as an arbitrary cartesian square, so the statement covers either order of its two legs.

theorem isLocallyNoetherian_of_isPullback'
    {W X Y Z : FppfSheaf B S hS} {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y}
    (sq : IsPullback p q g f)
    (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyNoetherian B S hS W

AlgebraicGeometry.FormalSpace.isLocallyNoetherian_of_isPullback_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LocallyNoetherianSource.lean, line 92.

Stacks 0AQ8. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of fppf sheaves over S. If Z is a locally Noetherian formal algebraic space and f is locally of finite type, then Z ×_Y X is locally Noetherian.

The projection p : Z ×_Y X ⟶ Z is a base change of f, so it is locally of finite type by Stacks 0AQ5; being representable by algebraic spaces it makes Z ×_Y X a formal algebraic space by Stacks 0AJI, and Stacks 0AQ7 applies to p. The fibre product is presented as an arbitrary cartesian square, so the statement covers either order of its two legs; X and Y need not be formal algebraic spaces.

theorem isLocallyNoetherian_of_isPullback_of_isLocallyOfFiniteType
    {W X Y Z : FppfSheaf B S hS} {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y}
    (sq : IsPullback p q g f)
    (hZ : IsLocallyNoetherian B S hS Z)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyNoetherian B S hS W

Sources

LeanAlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType · AlgebraicGeometry.FormalSpace.IsFiniteType · AlgebraicGeometry.FormalSpace.IsFiniteType' · AlgebraicGeometry.FormalSpace.IsBootstrapFiniteType · AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType · AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.comp · AlgebraicGeometry.FormalSpace.IsFiniteType.comp · AlgebraicGeometry.FormalSpace.IsBootstrapFiniteType.comp

Section87.25 Surjective morphisms #

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

Tag 0GHP, a definition

Tag 0GHP in the Stacks Project.

AlgebraicGeometry.FormalSpace.isSurjective_iff_isSurjectiveULift_red, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 97. The attribute's comment: “the definition, identified with the source's condition on the morphism of underlying reduced algebraic spaces”.

Surjectivity on points of a morphism of formal algebraic spaces over S is the condition of Stacks 0GHP on it: the morphism between any two reductions of its source and target compatible with it is a surjective morphism of algebraic spaces exactly when the morphism itself is surjective on points.

theorem isSurjective_iff_isSurjectiveULift_red {X Y Xred Yred : FppfSheaf B S hS}
    {iX : Xred ⟶ X} {iY : Yred ⟶ Y}
    (hiX : IsReduction B S hS X Xred iX) (hiY : IsReduction B S hS Y Yred iY)
    {f : X ⟶ Y} {fred : Xred ⟶ Yred} (hfred : fred ≫ iY = iX ≫ f) :
    IsSurjective B S hS f ↔ Space.IsSurjectiveULift.{u + 1} B S hS fred.hom

Tag 0GHQ, a lemma

Tag 0GHQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsSurjective.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 128.

The composition of two surjective morphisms of fppf sheaves on the big fppf site of S is surjective.

theorem IsSurjective.comp {X Y Z : FppfSheaf B S hS} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsSurjective B S hS f) (hg : IsSurjective B S hS g) :
    IsSurjective B S hS (f ≫ g)

Tag 0GHR, a lemma

Tag 0GHR in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsSurjective.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 143.

A base change of a surjective morphism of fppf sheaves on the big fppf site of S is surjective.

theorem IsSurjective.of_isPullback {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsSurjective B S hS f) : IsSurjective B S hS p

Tag 0GHS, a lemma

Tag 0GHS in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsSurjective.hasSurjectiveFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 306. The attribute's comment: “condition (1) implies condition (4)”.

Stacks 0GHS, condition (1) implies condition (4). If f : X ⟶ Y is surjective and Y is a formal algebraic space over S, then the atlas of Y furnished by Stacks 0AIM is a covering {Y_j ⟶ Y} as in Definition 0AIM along which every base change of f is surjective.

theorem IsSurjective.hasSurjectiveFormalAtlas {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : IsSurjective B S hS f) :
    HasSurjectiveFormalAtlas B S hS f

AlgebraicGeometry.FormalSpace.isSurjective_of_hasSurjectiveFormalAtlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 317. The attribute's comment: “condition (4) implies condition (1)”.

Stacks 0GHS, condition (4) implies condition (1). If a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S admits a covering {Y_j ⟶ Y} of its target as in Definition 0AIM along which every base change of f is surjective, then f is surjective.

theorem isSurjective_of_hasSurjectiveFormalAtlas {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : HasSurjectiveFormalAtlas B S hS f) : IsSurjective B S hS f

AlgebraicGeometry.FormalSpace.isSurjective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Surjective.lean, line 338. The attribute's comment: “conditions (1), (2), (3), (4) and (5)”.

For a morphism f : X ⟶ Y of formal algebraic spaces over S the following are equivalent:

f is surjective;

for every scheme T over S in the site and every T ⟶ Y the projection X ×_Y T ⟶ T is surjective;

the same for every affine scheme T over S in the site;

there is a covering {Y_j ⟶ Y} as in Definition 0AIM such that each projection X ×_Y Y_j ⟶ Y_j is surjective;

there is a surjective morphism Z ⟶ Y of formal algebraic spaces over S such that X ×_Y Z ⟶ Z is surjective.

theorem isSurjective_tfae {X Y : FppfSheaf B S hS} (hY : IsFormalAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsSurjective B S hS f,
        IsSurjectiveOnSchemeBaseChanges B S hS f,
        IsSurjectiveOnAffineBaseChanges B S hS f,
        HasSurjectiveFormalAtlas B S hS f,
        HasSurjectiveFormalCover B S hS f]

Sources

LeanAlgebraicGeometry.FormalSpace.isSurjective_iff_isSurjectiveULift_red · AlgebraicGeometry.FormalSpace.IsSurjective.comp · AlgebraicGeometry.FormalSpace.IsSurjective.of_isPullback · AlgebraicGeometry.FormalSpace.IsSurjective.hasSurjectiveFormalAtlas · AlgebraicGeometry.FormalSpace.isSurjective_of_hasSurjectiveFormalAtlas · AlgebraicGeometry.FormalSpace.isSurjective_tfae

Section87.26 Monomorphisms #

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

Tag 0AQB, a definition

Tag 0AQB in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Mono registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/Defs.lean, line 63 (StacksFrontier): “monomorphism of the underlying sheaves”. References: EGA IV (8.11.5.1); SGA 1 V (3.6); SGA 3 VIIB (2.4.1); SGA 3 VIII (3.4); SGA 4 I (10.4); SGA 4 II (3.2).

Tag 0GHT, a lemma

Tag 0GHT in the Stacks Project.

AlgebraicGeometry.FormalSpace.mono_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Monomorphism.lean, line 67.

The composition of two monomorphisms of formal algebraic spaces over S is a monomorphism.

theorem mono_comp {X Y Z : FppfSheaf B S hS} {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : Mono f) (hg : Mono g) : Mono (f ≫ g)

Tag 0GHU, a lemma

Tag 0GHU in the Stacks Project.

AlgebraicGeometry.FormalSpace.Mono.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Monomorphism.lean, line 75.

A base change of a monomorphism of formal algebraic spaces over S is a monomorphism: in the cartesian square with f on the right and p on the left, if f is a monomorphism then so is p.

theorem Mono.of_isPullback {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : Mono f) : Mono p

Tag 0GHV, a lemma

Tag 0GHV in the Stacks Project.

AlgebraicGeometry.FormalSpace.mono_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Monomorphism.lean, line 250. The attribute's comment: “conditions (1), (2), (3), (4) and (5)”.

For a morphism f : X ⟶ Y of formal algebraic spaces over S, with Y a formal algebraic space, the following are equivalent:

f is a monomorphism;

for every scheme T over S in the site and every T ⟶ Y the projection X ×_Y T ⟶ T is a monomorphism;

the same for every affine scheme T over S in the site;

there is a covering {Y_j ⟶ Y} as in Definition 0AIM such that each X ×_Y Y_j ⟶ Y_j is a monomorphism;

there is a family {Y_j ⟶ Y} with ∐ Y_j ⟶ Y a surjection of sheaves such that each X ×_Y Y_j ⟶ Y_j is a monomorphism.

theorem mono_tfae {X Y : FppfSheaf B S hS} (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [Mono f,
        IsMonoOnSchemeBaseChanges B S hS f,
        IsMonoOnAffineBaseChanges B S hS f,
        HasMonoFormalAtlas B S hS f,
        HasMonoLocallySurjectiveFamily B S hS f]

AlgebraicGeometry.FormalSpace.mono_tfae', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Monomorphism.lean, line 273. The attribute's comment: “conditions (1), (2), (3) and (5)”.

For an arbitrary morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S, conditions (1), (2), (3) and (5) of AlgebraicGeometry.FormalSpace.mono_tfae are equivalent.

theorem mono_tfae' {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    List.TFAE
      [Mono f,
        IsMonoOnSchemeBaseChanges B S hS f,
        IsMonoOnAffineBaseChanges B S hS f,
        HasMonoLocallySurjectiveFamily B S hS f]

AlgebraicGeometry.FormalSpace.mono_tfae_flatCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MonomorphismFlatCover.lean, line 426. The attribute's comment: “condition (6), and its equivalence with the conditions (1), (2), (3), (4) and (5)”.

Stacks 0GHV, its condition (6) together with the conditions (1), (2), (3), (4) and (5). For a morphism f : X ⟶ Y of formal algebraic spaces over S, with Y a formal algebraic space, the following are equivalent:

f is a monomorphism;

for every scheme T over S in the site and every T ⟶ Y the projection X ×_Y T ⟶ T is a monomorphism;

the same for every affine scheme T over S in the site;

there is a covering {Y_j ⟶ Y} as in Definition 0AIM such that each X ×_Y Y_j ⟶ Y_j is a monomorphism;

there is a family {Y_j ⟶ Y} with ∐ Y_j ⟶ Y a surjection of sheaves such that each X ×_Y Y_j ⟶ Y_j is a monomorphism;

there is a morphism Z ⟶ Y of formal algebraic spaces over S which is representable by algebraic spaces, surjective, flat and locally of finite presentation such that X ×_Y Z ⟶ Z is a monomorphism.

The equivalence of the first five conditions is AlgebraicGeometry.FormalSpace.mono_tfae; condition (6) is absorbed into it by the identity of Y, which is such a cover, and by the fact that such a cover is a surjection of sheaves.

theorem mono_tfae_flatCover {X Y : FppfSheaf B S hS} (hY : IsFormalAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [Mono f,
        IsMonoOnSchemeBaseChanges B S hS f,
        IsMonoOnAffineBaseChanges B S hS f,
        HasMonoFormalAtlas B S hS f,
        HasMonoLocallySurjectiveFamily B S hS f,
        HasMonoFlatCover B S hS f]

Sources

LeanCategoryTheory.Mono · AlgebraicGeometry.FormalSpace.mono_comp · AlgebraicGeometry.FormalSpace.Mono.of_isPullback · AlgebraicGeometry.FormalSpace.mono_tfae · AlgebraicGeometry.FormalSpace.mono_tfae' · AlgebraicGeometry.FormalSpace.mono_tfae_flatCover

Section87.27 Closed immersions #

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

Tag 0ANP, a definition

Tag 0ANP in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsClosedImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersion.lean, line 59.

A morphism of formal algebraic spaces over S is a closed immersion when it is representable by algebraic spaces and every base change of it along a scheme-valued point of its target is a closed immersion of schemes. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsClosedImmersion {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

Tag 0GHW, a lemma

Tag 0GHW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosedImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersion.lean, line 120. References: EGA I (4.2.5), “closed immersions”.

A composite of two closed immersions of formal algebraic spaces over S is a closed immersion.

theorem isClosedImmersion_comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsClosedImmersion B S hS f) (hg : IsClosedImmersion B S hS g) :
    IsClosedImmersion B S hS (f ≫ g)

Tag 0GHX, a lemma

Tag 0GHX in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosedImmersion_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersion.lean, line 176.

A base change of a closed immersion of formal algebraic spaces over S is a closed immersion: in a cartesian square of fppf sheaves on the big fppf site of S whose right-hand column f is a closed immersion, the left-hand column snd is a closed immersion.

theorem isClosedImmersion_of_isPullback {X Y Y' P : FppfSheaf B S hS}
    {fst : P ⟶ X} {snd : P ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback fst snd f g)
    (hf : IsClosedImmersion B S hS f) : IsClosedImmersion B S hS snd

Tag 0GHY, a lemma

Tag 0GHY in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_forall_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCriteria.lean, line 147. The attribute's comment: “conditions (1) and (2)”.

Stacks 0GHY, the equivalence of conditions (1) and (2): a morphism f : X ⟶ Y of formal algebraic spaces over S is a closed immersion if and only if for every scheme T over the big fppf site of S and every morphism T ⟶ Y the projection X ×_Y T ⟶ T is a closed immersion. As with the definition of a closed immersion, no hypothesis that X and Y are formal algebraic spaces is needed.

theorem isClosedImmersion_iff_forall_scheme {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsClosedImmersion B S hS f ↔
      ∀ (T : BigFppfOver B S hS) (g : yonedaSheaf B S hS T ⟶ Y),
        IsClosedImmersion B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isClosedImmersion_of_locallySurjectiveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionDescent.lean, line 413. The attribute's comment: “the descent step along a surjection of sheaves, which is the sufficiency in conditions (4) and (5)”.

Stacks 0GHY, the descent step along a surjection of sheaves: a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S is a closed immersion as soon as there is a family {Y_i ⟶ Y} whose induced map from the coproduct is a surjection of sheaves with every base change X ×_Y Y_i ⟶ Y_i a closed immersion.

A scheme-valued point of Y lies, locally on the point, in the image of a single member of the family; over that covering sieve the base change of f is a base change of one of the given closed immersions, so the base change of f along the point is a closed immersion by effective fppf descent of closed immersions.

Representability of f by algebraic spaces is not assumed: it is part of the conclusion, and it is produced by the same descent. The base change of f along a point of Y is a sheaf, and being represented by a closed immersion of the site after a covering sieve of that point already makes it pointwise u-small, which is all the descent step needs; the representing objects it returns then exhibit the base changes as algebraic spaces.

This is the sufficiency in both descent conditions of the source. For condition (4) the family is the étale atlas of the target, and Definition 0AIM asks of it exactly that it be a surjection of sheaves, so this is condition (4) implies condition (1): AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_exists_affineEtaleCover. For condition (5) the family has one member, but the source asks only that it be surjective on points, so the hypothesis must be upgraded first; that is done in AlgebraicGeometry.FormalSpace.isClosedImmersion_of_hasFlatClosedImmersionCover, which is condition (5) implies condition (1).

theorem isClosedImmersion_of_locallySurjectiveFamily {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (I : Type (u + 1)) (Yi : I → FppfSheaf B S hS) (c : ∀ i, Yi i ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc c))
    (hci : ∀ i, IsClosedImmersion B S hS (pullback.snd f (c i))) :
    IsClosedImmersion B S hS f

AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_forall_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionTfae.lean, line 221. The attribute's comment: “conditions (1) and (3)”.

Stacks 0GHY, the equivalence of conditions (1) and (3): a morphism f : X ⟶ Y of formal algebraic spaces over S is a closed immersion if and only if for every affine scheme T over the big fppf site of S and every morphism T ⟶ Y the projection X ×_Y T ⟶ T is a closed immersion. As with the definition of a closed immersion, no hypothesis that X and Y are formal algebraic spaces is needed.

theorem isClosedImmersion_iff_forall_affine {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsClosedImmersion B S hS f ↔
      ∀ (T : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj T) →
        ∀ (g : yonedaSheaf B S hS T ⟶ Y),
          IsClosedImmersion B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_exists_affineEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionTfae.lean, line 240. The attribute's comment: “conditions (1) and (4)”.

Stacks 0GHY, the equivalence of conditions (1) and (4): a morphism f : X ⟶ Y of formal algebraic spaces over S is a closed immersion if and only if there is a covering {Y_j ⟶ Y} as in Definition 0AIM with every base change X ×_Y Y_j ⟶ Y_j a closed immersion.

Necessity takes the atlas of Y furnished by its being a formal algebraic space; sufficiency is the descent step, which asks nothing of f, so in particular does not assume f representable by algebraic spaces.

theorem isClosedImmersion_iff_exists_affineEtaleCover {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) :
    IsClosedImmersion B S hS f ↔
      ∃ (I : Type (u + 1)) (Yi : I → FppfSheaf B S hS) (g : ∀ i, Yi i ⟶ Y),
        IsAffineEtaleCover B S hS Yi g ∧
          ∀ i, IsClosedImmersion B S hS (pullback.snd f (g i))

AlgebraicGeometry.FormalSpace.hasFlatClosedImmersionCover_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionTfae.lean, line 506. The attribute's comment: “condition (1) implies condition (5)”.

Stacks 0GHY, condition (1) implies condition (5): a closed immersion f : X ⟶ Y of formal algebraic spaces over S admits a morphism Z ⟶ Y of formal algebraic spaces, representable by algebraic spaces, surjective, flat and locally of finite presentation, along which the base change of f is a closed immersion.

The identity of Y serves: it is representable by algebraic spaces and étale, hence surjective on points, and each of its base changes along a scheme-valued point of Y is an isomorphism onto that point, so flatness and local finite presentation hold on every étale chart of it. The base change of f along the identity is f itself up to the canonical isomorphism.

theorem hasFlatClosedImmersionCover_of_isClosedImmersion {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : IsClosedImmersion B S hS f) :
    HasFlatClosedImmersionCover B S hS f

AlgebraicGeometry.FormalSpace.isClosedImmersion_of_hasFlatClosedImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionTfae.lean, line 535. The attribute's comment: “condition (5) implies condition (1)”.

Stacks 0GHY, condition (5) implies condition (1): if there is a morphism Z ⟶ Y of formal algebraic spaces representable by algebraic spaces, surjective, flat and locally of finite presentation along which the base change of f is a closed immersion, then f is a closed immersion.

Surjectivity here is the source's, surjectivity on points; it is upgraded to a surjection of sheaves by AlgebraicGeometry.FormalSpace.isLocallySurjective_of_isSurjective_of_flat, and the descent step then applies to the one-member family {Z ⟶ Y}.

theorem isClosedImmersion_of_hasFlatClosedImmersionCover {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : HasFlatClosedImmersionCover B S hS f) : IsClosedImmersion B S hS f

AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_hasFlatClosedImmersionCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionTfae.lean, line 555. The attribute's comment: “conditions (1) and (5)”.

Stacks 0GHY, the equivalence of conditions (1) and (5): a morphism f : X ⟶ Y of formal algebraic spaces over S is a closed immersion if and only if there is a morphism Z ⟶ Y of formal algebraic spaces, representable by algebraic spaces, surjective, flat and locally of finite presentation, with X ×_Y Z ⟶ Z a closed immersion.

theorem isClosedImmersion_iff_hasFlatClosedImmersionCover {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) :
    IsClosedImmersion B S hS f ↔ HasFlatClosedImmersionCover B S hS f

Tag 0ANQ, a lemma

Tag 0ANQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 129. The attribute's comment: “the source is McQuillan”.

Stacks 0ANQ, the McQuillan property of the source. The source of a closed immersion of formal algebraic spaces over S whose target is a McQuillan affine formal algebraic space is again a McQuillan affine formal algebraic space.

theorem hasSomeSurjectivePresentation_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (hX : HasSomeSurjectivePresentation B S hS X)
    (_hY : IsFormalAlgebraicSpace B S hS Y) (f : Y ⟶ X)
    (hf : IsClosedImmersion B S hS f) :
    HasSomeSurjectivePresentation B S hS Y

AlgebraicGeometry.FormalSpace.isClosed_ker_toRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 322. The attribute's comment: “closed kernel”.

Stacks 0ANQ, the closed-kernel assertion. The continuous homomorphism presenting a morphism of formal spectra of weakly admissible topological rings over S has closed kernel, its target being separated.

theorem isClosed_ker_toRingHom {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {A C : Type u} [CommRing A] [TopologicalSpace A] [CommRing C] [TopologicalSpace C]
    [IsTopologicalRing C] [IsLinearTopology C C]
    (hC : TopologicalRing.IsWeaklyAdmissible C) {D : QuotientSystem B S hS A}
    {E : QuotientSystem B S hS C} (g : ContinuousHom D E) :
    IsClosed (RingHom.ker g.toRingHom : Set A)

AlgebraicGeometry.FormalSpace.denseRange_of_isClosedImmersion_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 357. The attribute's comment: “dense image”.

Stacks 0ANQ, the dense-image assertion. The continuous homomorphism presenting a closed immersion of formal spectra of weakly admissible topological rings over S has dense image.

theorem denseRange_of_isClosedImmersion_formalSpectrumMap
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S} {A C : Type u} [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A] [CommRing C]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (g : ContinuousHom D E)
    (hg : IsClosedImmersion B S hS (formalSpectrumMap hA g)) :
    DenseRange g.toRingHom

AlgebraicGeometry.FormalSpace.isTaut_of_isClosedImmersion_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 89. The attribute's comment: “tautness”.

Stacks 0ANQ, the tautness assertion. The continuous homomorphism presenting a closed immersion of formal spectra of weakly admissible topological rings over S is taut. A closed immersion is representable by objects of the site, which is condition (2) of Stacks 0AN5, and condition (2) of that lemma gives tautness.

theorem isTaut_of_isClosedImmersion_formalSpectrumMap
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S} {A C : Type u} [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A] [CommRing C]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (g : ContinuousHom D E)
    (hg : IsClosedImmersion B S hS (formalSpectrumMap hA g)) :
    RingHom.IsTaut g.toRingHom

AlgebraicGeometry.FormalSpace.exists_formalSpectrumMap_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 174. The attribute's comment: “presenting homomorphism”.

Stacks 0ANQ, the presenting homomorphism. A closed immersion into the formal spectrum of a weakly admissible topological ring A over S, from a formal algebraic space Y, is the formal spectrum of a continuous homomorphism A ⟶ C of weakly admissible topological rings over S, for a ring C presenting Y.

The source carries the pullback of the canonical presentation of the target by its quotient spectra, whose transition morphisms are thickenings and whose section-ring projections are surjective; C is the limit of those section rings, weakly admissible because the transitions have locally nilpotent kernels. The recognition statement of AlgebraicGeometry.FormalSpace.DirectedQuotients identifies Y with Spf C, and the full faithfulness of Spf, Stacks 0AN0, turns the resulting morphism of formal spectra into the homomorphism.

theorem exists_formalSpectrumMap_of_isClosedImmersion
    (hA : TopologicalRing.IsWeaklyAdmissible A) (D : QuotientSystem B S hS A)
    {Y : FppfSheaf B S hS} (_hY : IsFormalAlgebraicSpace B S hS Y)
    (f : Y ⟶ formalSpectrum D) (hf : IsClosedImmersion B S hS f) :
    ∃ (C : Type u) (_ : CommRing C) (_ : TopologicalSpace C) (_ : IsTopologicalRing C)
      (_ : IsLinearTopology C C) (E : QuotientSystem B S hS C),
      TopologicalRing.IsWeaklyAdmissible C ∧
        ∃ (e : Y ≅ formalSpectrum E) (g : ContinuousHom D E),
          f = e.hom ≫ formalSpectrumMap hA g

Tag 0ANR, an example

Tag 0ANR in the Stacks Project.

AlgebraicGeometry.FormalSpace.isPullback_baseChange_quotientCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuotientCompletionBaseChange.lean, line 261. The attribute's comment: “base change”.

Stacks 0ANR, the base-change identification. Let T be an fppf sheaf over S and let t : T ⟶ Spec (A/I) be a morphism to a quotient stage of Spf A. Then the fibre product of Spf ((A/K)^∧) ⟶ Spf A with the induced morphism T ⟶ Spf A is T ×_{Spec (A/I)} Spec (A/(K + I)):
T ×_{Spec (A/I)} Spec (A/(K + I)) ⟶ Spf ((A/K)^∧)
               ↓                           ↓
               T                   ⟶     Spf A
is cartesian. A morphism to Spf A out of a quasi-compact scheme admits such a factorisation by Stacks 0AIA, which is the shape in which the source states this.

theorem isPullback_baseChange_quotientCompletion
    (I : TopologicalRing.WeakIdealOfDefinitionIndex A) (T : FppfSheaf B S hS)
    (t : T ⟶ (formalSpectrumDiagram D).obj (OrderDual.toDual I)) :
    IsPullback
      (pullback.fst
        ((Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map
          ((BigAffineFppf.inclusion B S hS).map
            (φ.stageMap I (quotientCompletionStageIdeal K I)
              (continuousHom_le_comap_quotientCompletionStageIdeal B S hS D E φ hφ I)))) t ≫
        formalSpectrumInclusion E (OrderDual.toDual (quotientCompletionStageIdeal K I)))
      (pullback.snd
        ((Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map
          ((BigAffineFppf.inclusion B S hS).map
            (φ.stageMap I (quotientCompletionStageIdeal K I)
              (continuousHom_le_comap_quotientCompletionStageIdeal B S hS D E φ hφ I)))) t)
      (formalSpectrumMap hA φ)
      (t ≫ formalSpectrumInclusion D (OrderDual.toDual I))

AlgebraicGeometry.FormalSpace.isClosedImmersion_formalSpectrumMap_quotientCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuotientCompletionBaseChange.lean, line 487. The attribute's comment: “closed immersion”.

Stacks 0ANR. The morphism Spf ((A/K)^∧) ⟶ Spf A induced by the canonical map A → (A/K)^∧ is a closed immersion of formal algebraic spaces over S, in the sense of Stacks 0ANP.

The stage inclusions Spec (A/I) ⟶ Spf A are jointly surjective with each base change of it along them the closed immersion Spec (A/(K + I)) ⟶ Spec (A/I); the descent step of Stacks 0GHY concludes, representability by algebraic spaces being part of what that step returns rather than a hypothesis of it.

theorem isClosedImmersion_formalSpectrumMap_quotientCompletion :
    AlgebraicGeometry.FormalSpace.IsClosedImmersion B S hS (formalSpectrumMap hA φ)

TopologicalRing.ker_canonicalMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/ClosedImmersion.lean, line 91. The attribute's comment: “kernel”.

The kernel of the canonical map to the completion of a quotient by a closed ideal is that ideal.

public theorem ker_canonicalMap_eq {A : Type u} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (K : Ideal A)
    (hK : IsClosed (K : Set A)) :
    RingHom.ker
      (TopologicalRing.CompletionOver.canonicalMap (Ideal.Quotient.mk K)) = K

TopologicalRing.exists_not_surjective_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/ClosedImmersion.lean, line 1073. The attribute's comment: “nonsurjectivity”.

For some weakly admissible ring and closed ideal, the map to the completed quotient is not surjective.

theorem exists_not_surjective_canonicalMap :
    ∃ D : TopologicalRing.ClosedIdealQuotientCompletionSituation.{u},
      ¬ Function.Surjective D.canonicalMap

Tag 0GHZ, a lemma

Tag 0GHZ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isClosedImmersion_of_mono_of_reduction_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MonomorphismClosedImmersion.lean, line 770. The attribute's comment: “the reduction, its inclusion and the factorisation are data, as in Stacks 0GB8”.

Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces and a monomorphism, and through which the inclusion iY : Yred ⟶ Y of a reduction of Y factors. If f is locally of finite type, or Y is locally Noetherian, then f is a closed immersion.

theorem isClosedImmersion_of_mono_of_reduction_factors {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom) (hmono : Mono f)
    {Yred : FppfSheaf B S hS} {iY : Yred ⟶ Y} (hiY : IsReduction B S hS Y Yred iY)
    (r : Yred ⟶ X) (hr : r ≫ f = iY)
    (hfin : IsLocallyOfFiniteType B S hS f ∨ IsLocallyNoetherian B S hS Y) :
    IsClosedImmersion B S hS f

Sources

LeanAlgebraicGeometry.FormalSpace.IsClosedImmersion · AlgebraicGeometry.FormalSpace.isClosedImmersion_comp · AlgebraicGeometry.FormalSpace.isClosedImmersion_of_isPullback · AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_forall_scheme · AlgebraicGeometry.FormalSpace.isClosedImmersion_of_locallySurjectiveFamily · AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_forall_affine · AlgebraicGeometry.FormalSpace.isClosedImmersion_iff_exists_affineEtaleCover · AlgebraicGeometry.FormalSpace.hasFlatClosedImmersionCover_of_isClosedImmersion

Section87.28 Restricted power series #

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

Tag 0AJM, a remark

Tag 0AJM in the Stacks Project.

RestrictedPowerSeries.existsUnique_continuousAlgHom_extends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RestrictedPowerSeries.lean, line 650. References: EGA 0 (7.5.3).

The universal property of restricted power series: every polynomial algebra map into a complete linearly topologized algebra extends by a unique continuous algebra map.

public theorem existsUnique_continuousAlgHom_extends
    {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    {C : Type x} [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    [IsLinearTopology C C] [Algebra A C]
    {ι : Type w} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
    (J : ι → Ideal A) (hJ : Antitone J)
    (_ : ∀ i, IsOpen (J i : Set A))
    (hfund : ∀ U ∈ nhds (0 : A), ∃ i, (J i : Set A) ⊆ U)
    (hAC : Continuous (algebraMap A C))
    (hC : TopologicalRing.IsComplete C)
    {σ : Type v} (f : MvPolynomial σ A →ₐ[A] C) :
    ∃! g : RestrictedPowerSeriesOfIdeals J hJ σ →ₐ[A] C,
      Continuous g ∧ g.comp (idealSystemPolynomialAlgHom J hJ σ) = f

Tag 0AL0, a remark

Tag 0AL0 in the Stacks Project.

RestrictedPowerSeries.limitCompleteSpace, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RestrictedPowerSeries.lean, line 799. The attribute's comment: “limit_completeness”.

Restricted power series are complete for their inverse-limit topology.

public instance limitCompleteSpace {A : Type u} [CommRing A]
    (I : Ideal A) (σ : Type v) :
    let _ : UniformSpace (RestrictedPowerSeries I σ) :=
      limitUniformSpace I σ
    CompleteSpace (RestrictedPowerSeries I σ)

RestrictedPowerSeries.isHomeomorph_adicCompletionEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RestrictedPowerSeries.lean, line 969. The attribute's comment: “finite_generation_topology”.

The canonical completion equivalence is an isomorphism of topological rings when the coefficient ideal is finitely generated.

public theorem isHomeomorph_adicCompletionEquiv {A : Type u} [CommRing A]
    (I : Ideal A) (σ : Type v) (hI : I.FG) :
    let _ : TopologicalSpace (RestrictedPowerSeries I σ) :=
      limitTopology I σ
    let _ : TopologicalSpace
      (AdicCompletion (I.map (MvPolynomial.C : A →+* MvPolynomial σ A))
        (MvPolynomial σ A)) := polynomialCompletionAdicTopology I σ
    IsHomeomorph (adicCompletionEquiv I σ)

Declarations registered for the tag:

RestrictedPowerSeries.adicCompletionEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/RingTheory/RestrictedPowerSeries.lean, line 787 (StacksFrontier): “ring_identification”.

Sources

LeanRestrictedPowerSeries.existsUnique_continuousAlgHom_extends · RestrictedPowerSeries.limitCompleteSpace · RestrictedPowerSeries.isHomeomorph_adicCompletionEquiv · RestrictedPowerSeries.adicCompletionEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

87.21 Morphisms and continuous… to 87.28 Restricted power series

Section87.21 Morphisms and continuous ring maps#

Tag 0ANB, a lemma

Tag 0CBA, a situation

Tag 0ANG, a lemma

Tag 0ANH, a remark

Tag 0ANI, a remark

Tag 0GBC, a situation

Tag 0GBD, a lemma

Tag 0GBE, a remark

Tag 0GBF, a remark

Tag 0GBG, a remark

Tag 0GBH, a situation

Tag 0GBI, a lemma

Tag 0GBJ, a remark

Tag 0GBK, a remark

Tag 0GBL, a situation

Tag 0GBM, a lemma

Tag 0GBN, a remark

Tag 0GBP, a remark

Sources

Section87.22 Taut ring maps and representability by algebraic spaces#

Tag 0ANJ, a lemma

Tag 0ANK, a lemma

Sources

Section87.23 Adic morphisms#

Tag 0AQ2, the section

Tag 0GBS, a lemma

Tag 0AQ3, a definition

Sources

Section87.24 Morphisms of finite type#

Tag 0AM4, a definition

Tag 0AJJ, a lemma

Tag 0AQ4, a lemma

Tag 0AQ5, a lemma

Tag 0AQ6, a lemma

Tag 0ANL, a lemma

Tag 0ANM, an example

Tag 0AQ7, a lemma

Tag 0AQ8, a lemma

Sources

Section87.25 Surjective morphisms#

Tag 0GHP, a definition

Tag 0GHQ, a lemma

Tag 0GHR, a lemma

Tag 0GHS, a lemma

Sources

Section87.26 Monomorphisms#

Tag 0AQB, a definition

Tag 0GHT, a lemma

Tag 0GHU, a lemma

Tag 0GHV, a lemma

Sources

Section87.27 Closed immersions#

Tag 0ANP, a definition

Tag 0GHW, a lemma

Tag 0GHX, a lemma

Tag 0GHY, a lemma

Tag 0ANQ, a lemma

Tag 0ANR, an example

Tag 0GHZ, a lemma

Sources

Section87.28 Restricted power series#

Tag 0AJM, a remark

Tag 0AL0, a remark

Sources

Section87.21 Morphisms and continuous ring maps #

Section87.22 Taut ring maps and representability by algebraic spaces #

Section87.23 Adic morphisms #

Section87.24 Morphisms of finite type #

Section87.25 Surjective morphisms #

Section87.26 Monomorphisms #

Section87.27 Closed immersions #

Section87.28 Restricted power series #