110.33 A finite flat module… to 110.52 A torsor which is not an…
Section110.33 A finite flat module which is not projective#
Section 110.33 of the Stacks Project, Tag 052H. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05FY, a lemma
Tag 05FY in the Stacks Project.
Stacks.Examples.exists_flat_closedImmersion_not_isOpenMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/StrangeFlatModules.lean, line 119. The attribute's comment: “part (2)”.
A flat closed immersion of schemes need not be an open map.
theorem exists_flat_closedImmersion_not_isOpenMap :
∃ (X Y : Scheme.{u}) (f : X ⟶ Y),
IsClosedImmersion f ∧ Flat f ∧ ¬ IsOpenMap f
Declarations registered for the tag:
Module.Finite.quotientregistered withadd_to_stacksin StacksFrontier/Examples/Flatness/StrangeFlatModules.lean, line 53 (StacksFrontier): “part (1): finite”. References: EGA 0 (5.2.1), “special case”; SGA 6 I (3.2), “special case”.Stacks.FiniteFlatNotProjective.quotientModule_flat, declared in the repository, registered withadd_to_stacksin StacksFrontier/Examples/Flatness/StrangeFlatModules.lean, line 54 (StacksFrontier): “part (1): flat”.Stacks.FiniteFlatNotProjective.quotientModule_not_projective, declared in the repository, registered withadd_to_stacksin StacksFrontier/Examples/Flatness/StrangeFlatModules.lean, line 55 (StacksFrontier): “part (1): not projective”.
Sources
Section110.34 A projective module which is not locally free#
Section 110.34 of the Stacks Project, Tag 05WG. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05WH, a lemma
Tag 05WH in the Stacks Project.
Stacks.Examples.projective_of_eq_span_countable_idempotents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/ProjectiveIdealNotLocallyFree.lean, line 231.
Stacks 05WH. An ideal generated by a countable set of idempotent elements is projective as a module.
theorem projective_of_eq_span_countable_idempotents
{R : Type u} [CommRing R] (I : Ideal R) (s : Set R)
(hs : s.Countable) (hidem : ∀ e ∈ s, IsIdempotentElem e)
(hI : I = Ideal.span s) : Module.Projective R I
Tag 05WJ, a lemma
Tag 05WJ in the Stacks Project.
Stacks.Examples.exists_projective_ideal_not_locallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/ProjectiveIdealNotLocallyFree.lean, line 356.
Stacks 05WJ. Some projective ideal of a commutative ring is not locally free as a module.
theorem exists_projective_ideal_not_locallyFree :
∃ (R : Type u) (_ : CommRing R) (I : Ideal R),
Module.Projective R I ∧ ¬ Module.IsLocallyFree R I
Tag 05WK, a lemma
Tag 05WK in the Stacks Project.
Stacks.Chow.chowClass_overProdOpens_section_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/Degrees/ProductOfPuncturedSchemes.lean, line 455.
Stacks 05WK. Let the base be a situation for Chow homology with vanishing dimension function, the case of the spectrum of a field. Let
X ibe proper over the base, each with a sectionP iand a pointQ iwhose residue field has degree two over the base, and letU ibe the complement ofQ i. The sections assemble into a section of the product of theU iover the base, and the prime cycle of each of its points is not rationally equivalent to zero: the class ofP 1 × ⋯ × P nis nonzero in the zeroth Chow group ofU 1 ×_S ⋯ ×_S U n.
theorem chowClass_overProdOpens_section_ne_zero (C : ChowSituation.{u})
(hδ : ∀ s : C.S, C.dimensionFunction s = 0) {n : ℕ} {X : Fin n → Scheme.{u}}
(f : ∀ i, X i ⟶ C.S) [∀ i, IsProper (f i)] (P : ∀ i, C.S ⟶ X i)
(hP : ∀ i, P i ≫ f i = 𝟙 C.S) (Q : ∀ i, X i) (hQ : ∀ i, (f i).residueDegree (Q i) = 2)
(U : ∀ i, (X i).Opens) (hU : ∀ i, (U i : Set (X i)) = {Q i}ᶜ) :
∃ σ : C.S ⟶ (overProd fun i ↦ (U i).ι ≫ f i).left,
σ ≫ (overProd fun i ↦ (U i).ι ≫ f i).hom = 𝟙 C.S ∧
(∀ i, σ ≫ overProdπ (fun i ↦ (U i).ι ≫ f i) i ≫ (U i).ι = P i) ∧
∀ s₀ : C.S, ∃ α : CycleGroup C (overProd fun i ↦ (U i).ι ≫ f i).hom 0,
α.1 = @Function.locallyFinsuppWithin.single _ _ ℤ
(Classical.decEq (overProd fun i ↦ (U i).ι ≫ f i).left) _ (σ.base s₀) (1 : ℤ) ∧
QuotientAddGroup.mk' (rationalEquivalences C
(overProd fun i ↦ (U i).ι ≫ f i).hom 0) α ≠ 0
Tag 05WL, a lemma
Tag 05WL in the Stacks Project.
Stacks.Examples.exists_countable_projective_directSum_isFiniteLocallyFree_not_isLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/CountableProjectiveNotLocallyFree.lean, line 319. The attribute's comment: “the summands are finite locally free but NOT of rank one, which is the one way this is weaker than the tag; the countability of the ring and the direct-sum presentation are as the tag states them. The rank-one case is unreachable from this construction: the summands εₙ R localize to zero at every prime containing εₙ, a Boolean ring of 𝔽₂-sequences has no invertible ideals at all, and the mechanism that defeats local freeness here — every element of a localization of the direct sum is annihilated by a nonzero scalar — is incompatible with rank-one summands, which are faithful at every prime; by Bass's theorem on big projective modules a rank-one example needs a non-noetherian ring of unbounded dimension. It therefore requires the source's own second construction, B_∞ = colim (A_1 ⊗_ℚ ⋯ ⊗_ℚ A_n) with the invertible L_i = Γ(U_i, ℒ_i), whose failure of local freeness is read off from the vanishing of higher Chern classes of a direct sum of invertible sheaves on a product of curves — the machinery of Stacks 02TA, 02TH, 02TJ and 02TM, of which only 02TH is available unconditionally in this repository”.
Stacks 05WL, with finite locally free summands in place of rank one. There is a countable ring
Rand a projectiveR-module which is a direct sum of countably many finite locally free modules but is not itself locally free.The summands
εₙ Rhave rank one at the primes avoidingεₙand rank zero at the others, so they are finite locally free but not of rank one as the tag asks; the rank-one case belongs to the source's second construction and is not formalized here. See the implementation notes ofStacksFrontier.Examples.Algebra.CountableProjectiveNotLocallyFree.
theorem exists_countable_projective_directSum_isFiniteLocallyFree_not_isLocallyFree :
∃ (R : Type u) (hR : CommRing R),
letI : CommRing R := hR
Countable R ∧
∃ L : ℕ → ModuleCat.{u} R,
(∀ n, Module.IsFiniteLocallyFree R (L n)) ∧
Module.Projective R (DirectSum ℕ fun n => L n) ∧
¬ Module.IsLocallyFree R (DirectSum ℕ fun n => L n)
Sources
Section110.35 Zero dimensional local ring with nonzero flat ideal#
Section 110.35 of the Stacks Project, Tag 05FZ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05G0, a lemma
Tag 05G0 in the Stacks Project.
Stacks.Examples.exists_local_ring_unique_prime_nonzero_flat_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/ZeroDimensionalFlatIdeal.lean, line 483.
Stacks 05G0. There is a local ring with a unique prime ideal and a nonzero proper flat ideal.
theorem exists_local_ring_unique_prime_nonzero_flat_ideal :
∃ (R : Type u) (_ : CommRing R) (_ : IsLocalRing R) (I : Ideal R),
(∃! p : Ideal R, p.IsPrime) ∧ I ≠ ⊥ ∧ I ≠ ⊤ ∧ Module.Flat R I
Sources
Section110.36 An epimorphism of zero-dimensional rings which is not surjective#
Section 110.36 of the Stacks Project, Tag 06RH. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06RI, a lemma
Tag 06RI in the Stacks Project.
Stacks.Examples.exists_epi_localRing_not_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/EpiNotSurjective.lean, line 625.
Stacks 06RI. There is a nonsurjective epimorphism of zero-dimensional local rings.
theorem exists_epi_localRing_not_surjective :
∃ (A B : Type u) (_ : CommRing A) (_ : CommRing B)
(_ : IsLocalRing A) (_ : IsLocalRing B) (f : A →+* B),
ringKrullDim A = 0 ∧
ringKrullDim B = 0 ∧
IsLocalHom f ∧
Epi (CommRingCat.ofHom f) ∧
¬ Function.Surjective f
Sources
Section110.37 Finite type, not finitely presented, flat at prime#
Section 110.37 of the Stacks Project, Tag 05G1. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05G2, a lemma
Tag 05G2 in the Stacks Project.
Stacks.Examples.RaynaudGruson.exists_flat_at_prime_not_flat_on_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/RaynaudGruson/NoFlatNeighborhood.lean, line 275.
The Raynaud--Gruson example. There is a local ring
A, a finite type ring mapA → Band a primeqofBover the maximal ideal ofAsuch thatB_qis flat overAwhile for everyg ∈ Boutsideqthe ringB_gis neither of finite presentation nor flat overA.
theorem exists_flat_at_prime_not_flat_on_neighborhood :
∃ (A B : Type) (_ : CommRing A) (_ : CommRing B) (_ : IsLocalRing A) (φ : A →+* B)
(q : Ideal B) (_ : q.IsPrime),
φ.FiniteType ∧ q.comap φ = IsLocalRing.maximalIdeal A ∧
((algebraMap B (Localization.AtPrime q)).comp φ).Flat ∧
∀ g : B, g ∉ q →
¬ ((algebraMap B (Localization.Away g)).comp φ).FinitePresentation ∧
¬ ((algebraMap B (Localization.Away g)).comp φ).Flat
Sources
Section110.38 Finite type, flat and not of finite presentation#
Section 110.38 of the Stacks Project, Tag 05LB. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05LC, a lemma
Tag 05LC in the Stacks Project.
Stacks.Examples.exists_flat_finiteType_not_finitePresentation_of_curve_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/AffineCurveNotFinitePresentation.lean, line 226. The attribute's comment: “(2)”.
A flat algebra of finite type with geometrically connected and geometrically reduced one-dimensional complete-intersection fibres need not be of finite presentation.
theorem exists_flat_finiteType_not_finitePresentation_of_curve_fibers :
∃ (R : Type u) (A : Type v) (_ : CommRing R) (_ : CommRing A)
(_ : Algebra R A),
Module.Flat R A ∧ Algebra.FiniteType R A ∧ ¬ Algebra.FinitePresentation R A ∧
(∀ (p : Ideal R) [p.IsPrime],
Algebra.IsGeometricallyConnected p.ResidueField (p.Fiber A) ∧
Algebra.IsGeometricallyReduced p.ResidueField (p.Fiber A) ∧
ringKrullDim (p.Fiber A) = 1 ∧
IsGlobalCompleteIntersection p.ResidueField (p.Fiber A))
Stacks.Examples.exists_proper_flat_not_finitePresentation_with_nodal_or_line_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/ProjFamilyNotFinitePresentation.lean, line 338. The attribute's comment: “(3)”.
There is a proper flat morphism of schemes, not locally of finite presentation, each of whose fibres is either a projective line or the vanishing locus of
X₁X₂in the projective plane over the residue field of its point.
theorem exists_proper_flat_not_finitePresentation_with_nodal_or_line_fibers :
∃ (R : Type u) (_ : CommRing R) (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of R)),
IsProper f ∧ AlgebraicGeometry.Flat f ∧ ¬ LocallyOfFinitePresentation f ∧
∀ (p : Ideal R) [p.IsPrime],
(∃ g : projectiveSpaceOverRing 1 (CommRingCat.of p.ResidueField) ⟶ X,
IsPullback g
(projectiveSpaceOverRing 1 (CommRingCat.of p.ResidueField) ↘
Spec (CommRingCat.of p.ResidueField))
f (Spec.map (CommRingCat.ofHom (algebraMap R p.ResidueField)))) ∨
(∃ g : monomialPairLocus p.ResidueField 2 1 (Fin.last 2) ⟶ X,
IsPullback g (monomialPairLocusToSpec p.ResidueField 2 1 (Fin.last 2)) f
(Spec.map (CommRingCat.ofHom (algebraMap R p.ResidueField))))
Stacks.Examples.exists_proper_flat_not_finitePresentation_with_projectiveSpace_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/ProjFamilyNotFinitePresentation.lean, line 370. The attribute's comment: “(4)”.
There is a proper flat morphism of schemes, not locally of finite presentation, each of whose fibres is either a projective line or a projective plane over the residue field of its point.
theorem exists_proper_flat_not_finitePresentation_with_projectiveSpace_fibers :
∃ (R : Type u) (_ : CommRing R) (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of R)),
IsProper f ∧ AlgebraicGeometry.Flat f ∧ ¬ LocallyOfFinitePresentation f ∧
∀ (p : Ideal R) [p.IsPrime],
(∃ g : projectiveSpaceOverRing 1 (CommRingCat.of p.ResidueField) ⟶ X,
IsPullback g
(projectiveSpaceOverRing 1 (CommRingCat.of p.ResidueField) ↘
Spec (CommRingCat.of p.ResidueField))
f (Spec.map (CommRingCat.ofHom (algebraMap R p.ResidueField)))) ∨
(∃ g : projectiveSpaceOverRing 2 (CommRingCat.of p.ResidueField) ⟶ X,
IsPullback g
(projectiveSpaceOverRing 2 (CommRingCat.of p.ResidueField) ↘
Spec (CommRingCat.of p.ResidueField))
f (Spec.map (CommRingCat.ofHom (algebraMap R p.ResidueField))))
Stacks.Examples.exists_flat_finiteType_not_finitePresentation_with_completeIntersection_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/SquareZeroNotFinitePresentation.lean, line 219. The attribute's comment: “(1)”.
A flat ring map of finite type can have geometrically irreducible complete-intersection fibres without being of finite presentation.
theorem exists_flat_finiteType_not_finitePresentation_with_completeIntersection_fibers :
∃ (R S : Type u) (_ : CommRing R) (_ : CommRing S) (f : R →+* S),
f.Flat ∧ f.FiniteType ∧ ¬ f.FinitePresentation ∧
(letI := f.toAlgebra
∀ (p : Ideal R) [p.IsPrime],
letI : Algebra p.ResidueField (S ⊗[R] p.ResidueField) :=
Algebra.TensorProduct.rightAlgebra
Algebra.IsGeometricallyIrreducible p.ResidueField
(S ⊗[R] p.ResidueField) ∧
IsGlobalCompleteIntersection p.ResidueField
(S ⊗[R] p.ResidueField))
Sources
Section110.39 Topology of a finite type ring map#
Section 110.39 of the Stacks Project, Tag 05JH. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05JI, a lemma
Tag 05JI in the Stacks Project.
Stacks.Examples.exists_localHom_no_quasiFinite_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FiniteTypeTopology.lean, line 101.
A local map of local domains, essentially of finite type with finite residue extension, whose target has a nonmaximal prime but no quotient by such a prime is a localization of a quasi-finite algebra.
public theorem exists_localHom_no_quasiFinite_quotient :
∃ (A B : Type u) (_ : CommRing A) (_ : CommRing B)
(_ : IsDomain A) (_ : IsDomain B) (_ : IsLocalRing A) (_ : IsLocalRing B)
(f : A →+* B) (hf : IsLocalHom f),
IsEssentiallyOfFiniteType A B f ∧
(letI : IsLocalHom f := hf
letI := (IsLocalRing.ResidueField.map f).toAlgebra
Module.Finite (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) ∧
(∃ q : PrimeSpectrum B, q.asIdeal ≠ IsLocalRing.maximalIdeal B) ∧
(∀ q : PrimeSpectrum B, q.asIdeal ≠ IsLocalRing.maximalIdeal B →
¬ (letI := f.toAlgebra
∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C)
(_ : Algebra.FiniteType A C) (_ : Algebra.QuasiFinite A C)
(M : Submonoid C) (_ : Algebra C (B ⧸ q.asIdeal)),
IsScalarTower A C (B ⧸ q.asIdeal) ∧ IsLocalization M (B ⧸ q.asIdeal)))
Sources
Section110.40 Pure not universally pure#
Section 110.40 of the Stacks Project, Tag 05JJ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 05JK, a lemma
Tag 05JK in the Stacks Project.
Stacks.Examples.exists_isPureRelative_not_isUniversallyPureRelative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Flatness/PureNotUniversallyPure.lean, line 828.
There is a morphism of affine schemes of finite presentation and a module of finite presentation on its source which is pure relative to the base, but not universally pure relative to it.
theorem exists_isPureRelative_not_isUniversallyPureRelative :
∃ (X S : Scheme.{u}) (_ : IsAffine X) (_ : IsAffine S) (f : X ⟶ S)
(hf : FinitePresentation f) (F : X.Modules)
(hF : SheafOfModules.IsFinitePresentation.{u, u, u} F)
(hFT : SheafOfModules.IsFiniteType.{u, u, u} F)
(hQC : SheafOfModules.IsQuasicoherent.{u, u, u} F),
letI : LocallyOfFinitePresentation f := hf.1
letI : LocallyOfFiniteType f := inferInstance
letI : QuasiCompact f := hf.2.1
letI : SheafOfModules.IsFinitePresentation.{u, u, u} F := hF
letI : SheafOfModules.IsFiniteType.{u, u, u} F := hFT
letI : SheafOfModules.IsQuasicoherent.{u, u, u} F := hQC
IsPureRelative f F ∧ ¬ IsUniversallyPureRelative f F
Sources
Section110.41 A formally smooth non-flat ring map#
Section 110.41 of the Stacks Project, Tag 057V. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 057W, a lemma
Tag 057W in the Stacks Project.
Stacks.Examples.exists_formallySmooth_not_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FormallySmoothNotFlat.lean, line 202.
There exists a formally smooth ring map which is not flat.
public theorem exists_formallySmooth_not_flat :
∃ (R S : Type*) (_ : CommRing R) (_ : CommRing S) (f : R →+* S),
f.FormallySmooth ∧ ¬ f.Flat
Sources
Section110.42 A formally étale non-flat ring map#
Section 110.42 of the Stacks Project, Tag 060H. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 060I, a lemma
Tag 060I in the Stacks Project.
Stacks.Examples.exists_formallyEtale_not_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FormallyEtaleNotFlat.lean, line 180.
There exists a formally étale map of commutative rings which is not flat.
public theorem exists_formallyEtale_not_flat :
∃ (R S : Type*) (_ : CommRing R) (_ : CommRing S) (f : R →+* S),
f.FormallyEtale ∧ ¬ f.Flat
Sources
Section110.43 A formally étale ring map with nontrivial cotangent complex#
Section 110.43 of the Stacks Project, Tag 06E5. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06E6, a lemma
Tag 06E6 in the Stacks Project.
Stacks.Examples.exists_formallyEtale_surjective_mulKernel_ne_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FormallyEtaleNontrivialCotangent.lean, line 245. The attribute's comment: “the example: a formally étale surjection with Ker(J ⊗_A J → J²) ≠ 0”.
Stacks 06E6, the example. There is a formally étale surjective map of commutative rings
A → Bwhose kernelJhasKer(J ⊗_A J → J²) ≠ 0; equivalently,Jis idempotent but not weakly regular.
theorem exists_formallyEtale_surjective_mulKernel_ne_bot :
∃ (A : Type u) (_ : CommRing A) (B : Type u) (_ : CommRing B) (_ : Algebra A B),
Algebra.FormallyEtale A B ∧ Function.Surjective (algebraMap A B) ∧
LinearMap.ker (Submodule.mulMap' (RingHom.ker (algebraMap A B))
(RingHom.ker (algebraMap A B))) ≠ ⊥
Stacks.Examples.exists_formallyEtale_surjective_not_isZero_torTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/FormallyEtaleNontrivialCotangent.lean, line 261. The attribute's comment: “the example: a formally étale surjection with Tor₂^A(B, B) ≠ 0”.
Stacks 06E6, the example, with the nonvanishing read on
Tor₂. There is a formally étale surjective map of commutative ringsA → BwithTor₂^A(B, B) ≠ 0. By Tag 09D6 this is the same statement asexists_formallyEtale_surjective_mulKernel_ne_bot; it is the input from which the source deduces, via the five-term exact sequence of Quillen's spectral sequence, thatL_{B/A} ≠ 0.
theorem exists_formallyEtale_surjective_not_isZero_torTwo :
∃ (A : Type u) (_ : CommRing A) (B : Type u) (_ : CommRing B) (_ : Algebra A B),
Algebra.FormallyEtale A B ∧ Function.Surjective (algebraMap A B) ∧
¬ IsZero (((Tor' (ModuleCat.{u} A) 2).obj (ModuleCat.of A B)).obj
(ModuleCat.of A B))
Sources
Section110.44 Flat and formally unramified is not formally étale#
Section 110.44 of the Stacks Project, Tag 0G64. 3 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0G65, a lemma
Tag 0G65 in the Stacks Project.
Stacks.Examples.flat_perfectClosure_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/PerfectClosureNotFormallyEtale.lean, line 295. The attribute's comment: “flatness of the example F_p[T] into its perfect closure”.
Flat and formally unramified is not formally étale, flatness: the perfect closure of
𝔽ₚ[T]is flat over𝔽ₚ[T].
public theorem flat_perfectClosure_polynomial (p : ℕ) [Fact p.Prime] :
Module.Flat (Polynomial (ZMod p)) (PerfectClosure (Polynomial (ZMod p)) p)
Stacks.Examples.formallyUnramified_perfectClosure_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/PerfectClosureNotFormallyEtale.lean, line 302. The attribute's comment: “formal unramifiedness of the example F_p[T] into its perfect closure”.
Flat and formally unramified is not formally étale, formal unramifiedness: the perfect closure of
𝔽ₚ[T]is formally unramified over𝔽ₚ[T].
public theorem formallyUnramified_perfectClosure_polynomial (p : ℕ) [Fact p.Prime] :
Algebra.FormallyUnramified (Polynomial (ZMod p)) (PerfectClosure (Polynomial (ZMod p)) p)
Stacks.Examples.not_formallyEtale_perfectClosure_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/PerfectClosureNotFormallyEtale.lean, line 309. The attribute's comment: “the example F_p[T] into its perfect closure is not formally etale”.
Flat and formally unramified is not formally étale, the negative conjunct: the perfect closure of
𝔽ₚ[T]is not formally étale over𝔽ₚ[T].
public theorem not_formallyEtale_perfectClosure_polynomial (p : ℕ) [Fact p.Prime] :
¬ Algebra.FormallyEtale (Polynomial (ZMod p)) (PerfectClosure (Polynomial (ZMod p)) p)
Tag 0G66, a lemma
Tag 0G66 in the Stacks Project.
Stacks.Examples.flat_formallyUnramified_adicCompletion_and_not_formallyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ExcellentCompletionFormallyEtale.lean, line 325.
Let
(A, 𝔪, κ)be a Noetherian local ring of prime characteristicpwith[κ : κᵖ] < ∞. Then the canonical mapA → A^∧to the𝔪-adic completion is flat and formally unramified; if moreoverAis regular but not excellent, it is not formally étale.
public theorem flat_formallyUnramified_adicCompletion_and_not_formallyEtale
(A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (p : ℕ) [Fact p.Prime]
[CharP A p]
[Module.Finite (frobenius (ResidueField A) (ringExpChar (ResidueField A))).fieldRange
(ResidueField A)] :
Module.Flat A (AdicCompletion (maximalIdeal A) A) ∧
Algebra.FormallyUnramified A (AdicCompletion (maximalIdeal A) A) ∧
(IsRegularLocalRing A → ¬ IsExcellent A →
¬ Algebra.FormallyEtale A (AdicCompletion (maximalIdeal A) A))
Tag 0G68, a lemma
Tag 0G68 in the Stacks Project.
Stacks.Examples.formallyEtale_adicCompletion_of_isExcellent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ExcellentCompletionFormallyEtale.lean, line 346. The attribute's comment: “the forward implication, with no carried hypotheses; see the module docstring”.
The forward implication of Stacks
0G68: for a regular local ring of characteristicp > 0whose residue field has finite imperfection degree, excellence makes the canonical map to the maximal-ideal-adic completion formally étale.This needs none of Lemma
0G66: excellence makes the map regular, Néron–Popescu writes the completion as a filtered colimit of smooth algebras, and formal unramifiedness upgrades that to formal smoothness.
public theorem formallyEtale_adicCompletion_of_isExcellent
(A : Type u) [CommRing A] [IsRegularLocalRing A] (p : ℕ) [Fact p.Prime] [CharP A p]
[Module.Finite (frobenius (ResidueField A) (ringExpChar (ResidueField A))).fieldRange
(ResidueField A)] (excellent : IsExcellent A) :
Algebra.FormallyEtale A (AdicCompletion (maximalIdeal A) A)
Stacks.Examples.isExcellent_iff_formallyEtale_adicCompletion_maximalIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/ExcellentCompletionFormallyEtale.lean, line 363. The attribute's comment: “both directions, with no carried hypotheses”.
A regular local ring of characteristic
p > 0whose residue field has finite imperfection degree is excellent if and only if the canonical map to its maximal-ideal-adic completion is formally étale.
public theorem isExcellent_iff_formallyEtale_adicCompletion_maximalIdeal
(A : Type u) [CommRing A] [IsRegularLocalRing A] (p : ℕ) [Fact p.Prime] [CharP A p]
[Module.Finite (frobenius (ResidueField A) (ringExpChar (ResidueField A))).fieldRange
(ResidueField A)] :
IsExcellent A ↔ Algebra.FormallyEtale A (AdicCompletion (maximalIdeal A) A)
Sources
Section110.45 Ideals generated by sets of idempotents and localization#
Section 110.45 of the Stacks Project, Tag 04QK. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04QL, a lemma
Tag 04QL in the Stacks Project.
Stacks.Examples.exists_ideal_locally_span_idempotents_not_globally, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Schemes/IdealLocallyGeneratedByIdempotents.lean, line 521.
Stacks 04QL. A closed subscheme of an affine scheme can be locally, but not globally, cut out by ideals generated by idempotents.
theorem exists_ideal_locally_span_idempotents_not_globally :
∃ (R : Type u) (_ : CommRing R) (I : Ideal R),
(∀ p : PrimeSpectrum R,
∃ f : R, f ∉ p.asIdeal ∧
∃ s : Set (Localization.Away f),
(∀ e ∈ s, IsIdempotentElem e) ∧
Ideal.map (algebraMap R (Localization.Away f)) I = Ideal.span s) ∧
¬ ∃ s : Set R, (∀ e ∈ s, IsIdempotentElem e) ∧ I = Ideal.span s
Sources
Section110.46 A ring map which identifies local rings which is not ind-étale#
Section 110.46 of the Stacks Project, Tag 09AN. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09AP, a lemma
Tag 09AP in the Stacks Project.
Stacks.Examples.exists_identifiesLocalRings_not_indEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Schemes/LocalRingPreservingNotIndEtale.lean, line 436.
Stacks 09AP. A ring map can identify local rings without being ind-étale or ind-Zariski.
theorem exists_identifiesLocalRings_not_indEtale :
∃ (A : Type u) (_ : CommRing A) (B : Type v) (_ : CommRing B) (_ : Algebra A B),
Algebra.IdentifiesLocalRings A B ∧
¬ StacksDraft.IndEtale A B ∧
¬ AlgebraicGeometry.ProEtale.IsIndZariski.{u, v, w} A B
Sources
Section110.47 Non flasque quasi-coherent sheaf associated to injective module#
Section 110.47 of the Stacks Project, Tag 0273. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0274, a lemma
Tag 0274 in the Stacks Project.
Stacks.Examples.InjectiveTilde.exists_injective_tilde_not_flasque, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/NotFlasque.lean, line 248. The attribute's comment: “nonflasque associated sheaf”. References: SGA 6 II (AppI.0.1), “not flasque”; SGA 6 II (AppI.1.2), “Ĩ not flasque”.
Stacks Project, Tag 0274. An injective module can have a nonflasque associated sheaf on its affine spectrum.
theorem exists_injective_tilde_not_flasque :
∃ (A : CommRingCat) (J : ModuleCat A),
Injective J ∧ ¬ TopCat.Presheaf.IsFlasque (tilde J).presheaf
Stacks.Examples.InjectiveTilde.exists_injective_tilde_basicOpen_restriction_not_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/NotFlasque.lean, line 260. The attribute's comment: “basic-open restriction not surjective”. References: SGA 6 II (AppI.0.1), “not flasque (std open)”; SGA 6 II (AppI.1.2), “Ĩ not flasque”.
Stacks Project, Tag 0274. Even restriction to a standard open can fail to be surjective for the associated sheaf of an injective module.
theorem exists_injective_tilde_basicOpen_restriction_not_surjective :
∃ (A : CommRingCat) (J : ModuleCat A) (f : A),
Injective J ∧
¬ Function.Surjective
((tilde J).presheaf.map
(homOfLE (le_top : PrimeSpectrum.basicOpen f ≤ ⊤)).op)
Tag 0CRZ, a lemma
Tag 0CRZ in the Stacks Project.
Stacks.Examples.InjectiveTilde.exists_injective_tilde_nonzero_firstCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/QuasiCoherentPushforward/NonvanishingCohomology.lean, line 641. References: SGA 6 II (AppI.0.1), “noetherian space case”; SGA 6 II (AppI.1.2), “H¹(U,Ĩ)≠0”.
Stacks Project, Tag 0CRZ. An injective module on an affine scheme with Noetherian underlying space can have nonzero first cohomology on a quasi-compact open.
theorem exists_injective_tilde_nonzero_firstCohomology :
∃ (A : CommRingCat.{u}) (I : ModuleCat.{u} A) (U : (Spec A).Opens),
NoetherianSpace (Spec A) ∧ Injective I ∧
IsCompact (U : Set (Spec A)) ∧
¬ IsZero (Hgroup (Spec A).ringCatSheaf U 1 (tilde I))
Sources
Section110.48 A non-separated flat group scheme#
Section 110.48 of the Stacks Project, Tag 06E7. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06E8, a lemma
Tag 06E8 in the Stacks Project.
Stacks.Examples.exists_flat_finiteType_groupScheme_not_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/GroupSchemes/NonSeparated.lean, line 83. References: SGA 3 VIB (5.6.4), “base = affine line”.
Stacks Project, Tag 06E8. There is a flat group scheme of finite type over the affine line that is not separated.
public theorem exists_flat_finiteType_groupScheme_not_isSeparated (k : Type u) [Field k] :
∃ G : CategoryTheory.Over (Spec (.of (Polynomial k))),
Nonempty (GrpObj G) ∧ Flat G.hom ∧ LocallyOfFiniteType G.hom ∧
QuasiCompact G.hom ∧ ¬ IsSeparated G.hom
Tag 08IX, a lemma
Tag 08IX in the Stacks Project.
AlgebraicGeometry.exists_flat_finiteType_groupScheme_not_quasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ObstructionIX/NonQuasiSeparatedGroupScheme.lean, line 609.
Stacks Project, Tag 08IX. A flat finite-type group scheme over infinite-dimensional affine space need not be quasi-separated.
public theorem exists_flat_finiteType_groupScheme_not_quasiSeparated
(k : Type u) [Field k] :
∃ G : Grp (Over (Spec (.of (MvPolynomial ℕ k)))),
Flat G.X.hom ∧ LocallyOfFiniteType G.X.hom ∧
QuasiCompact G.X.hom ∧ ¬ QuasiSeparated G.X.hom
Sources
Section110.49 A non-flat group scheme with flat identity component#
Section 110.49 of the Stacks Project, Tag 06RJ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06RK, a lemma
Tag 06RK in the Stacks Project.
Stacks.Examples.exists_groupScheme_flat_identityComponent_not_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/GroupSchemes/NonFlatFlatIdentityComponent.lean, line 365. References: EGA IV (17.12.8), “non-flat example”.
Stacks Project, Tag 06RK. A group scheme can fail to be flat over its base even when its identity component is flat over the base.
public theorem exists_groupScheme_flat_identityComponent_not_flat :
∃ (S : Scheme.{u}) (G : CategoryTheory.Over S) (hG : GrpObj G),
letI : GrpObj G := hG
¬ Flat G.hom ∧
∃ U : G.left.Opens,
Flat (U.ι ≫ G.hom) ∧
IsClosed (U : Set G.left) ∧
Set.range (η[G]).left = (U : Set G.left) ∧
∀ s : S,
_root_.IsConnected {g : {g : G.left // G.hom g = s} |
(g.1 : G.left) ∈ (U : Set G.left)}
Sources
Section110.50 A non-separated group algebraic space over a field#
Section 110.50 of the Stacks Project, Tag 06E9. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06EA, a lemma
Tag 06EA in the Stacks Project.
Stacks.Examples.NonSeparatedGroupSpace.exists_isFiniteType_groupAlgebraicSpace_not_isSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/NonSeparatedGroupSpace.lean, line 823.
Stacks Project, Tag 06EA. Over a field of characteristic zero there is a group algebraic space of finite type over the field which is neither separated, nor quasi-separated, nor locally separated.
The witness is the quotient
𝔸¹_k/ℤof the affine line by the integer translations, realized as the fppf sheafification of the presheaf of global sections modulo the integers: addition of sections makes that sheafification a group object, while the quotient fails to be decent, and a quasi-separated or locally separated algebraic space is decent.
theorem exists_isFiniteType_groupAlgebraicSpace_not_isSeparatedOver
(k : Type u) [Field k] [CharZero k] (B : BigFppfSite.{u})
(hS : B.Contains (Spec (.of k))) (hG : B.Contains (Spec (.of (RatFunc k)))) :
∃ G : Space.GroupAlgebraicSpace B (Spec (.of k)) hS
(yoneda.obj (Over.mk (𝟙 (B.obj hS))))
(isAlgebraicSpace_yoneda B (Spec (.of k)) hS (Over.mk (𝟙 (B.obj hS)))),
Space.IsFiniteType B (Spec (.of k)) hS G.obj.X.hom ∧
¬ Space.IsSeparatedOver B (Spec (.of k)) hS G.obj.X.left ∧
¬ Space.IsQuasiSeparatedOver B (Spec (.of k)) hS G.obj.X.left ∧
¬ Space.IsLocallySeparatedOver B (Spec (.of k)) hS G.obj.X.left
Sources
Section110.51 Specializations between points in fibre étale morphism#
Section 110.51 of the Stacks Project, Tag 06UJ. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 06UK, a lemma
Tag 06UK in the Stacks Project.
Stacks.Examples.EtaleSpecialization.exists_isEtale_specializes_pointsMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/EtaleSpecializationInFibre.lean, line 149. The attribute's comment: “a specialization inside a fibre of an étale morphism of algebraic spaces”.
Stacks 06UK. There is an étale morphism of algebraic spaces
f : X ⟶ Yand a nontrivial specialization of pointsx ⤳ x'in|X|withf x = f x'in|Y|.The witness is the chart
X = Spec K[y, x_n : n ∈ ℤ]of its own quotientY = X/ℤby the integer shift, at the tail pointsx = p_1andx' = p_0: the shift carriesp_0top_1, so the two have the same image inY, whilep_1 ⊂ p_0gives the specialization.That
Yis an algebraic space is the algebraicity half of Stacks 02WW,AlgebraicGeometry.Space.isAlgebraicSpace_quotient_unconditional, which is a theorem.
theorem exists_isEtale_specializes_pointsMap_eq :
∃ (X Y : (BigFppfOver B (Spec (.of K)) hS)ᵒᵖ ⥤ Type u)
(_ : IsAlgebraicSpace B (Spec (.of K)) hS X)
(_ : IsAlgebraicSpace B (Spec (.of K)) hS Y)
(f : X ⟶ Y) (x x' : Space.points B (Spec (.of K)) hS X),
Space.IsEtale B (Spec (.of K)) hS f ∧ x ≠ x' ∧ x ⤳ x' ∧
Space.pointsMap B (Spec (.of K)) hS X f x =
Space.pointsMap B (Spec (.of K)) hS X f x'
Sources
Section110.52 A torsor which is not an fppf torsor#
Section 110.52 of the Stacks Project, Tag 04AF. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 077B, a lemma
Tag 077B in the Stacks Project.
Stacks.Examples.RadicalTower.fpqcTorsor_not_isomorphic_fppfTorsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/GroupSchemes/PrincipalNotFppf/Torsor.lean, line 222. The attribute's comment: “counterexample: for S = Spec ℚ and G = ∏ᵢ μ_{i+2} a principal homogeneous G-space is exhibited that is isomorphic to no fppf G-torsor, which is the failure of essential surjectivity the source's proof invokes; the two stacks G-Principal and G-Torsors are not themselves constructed here”.
Stacks Project, Tag 077B. Over
S = Spec ℚthe group schemeG = ∏ᵢ μ_{i+2}has a principal homogeneous space, namelyP = Spec ℚ[x₀, x₁, …]/(xᵢ ^ (i + 2) - 2), which is isomorphic to no fppfG-torsor. Hence the inclusion of the fppfG-torsors into the principal homogeneousG-spaces is not essentially surjective, so the two stacks they form are not equivalent in general.
theorem fpqcTorsor_not_isomorphic_fppfTorsor :
IsFpqcTorsor base groupObj torsorObj ∧
∀ (Y : Over base) (_ : ModObj groupObj Y),
IsFppfTorsor base groupObj Y → ¬ Nonempty (torsorObj ≅ Y)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.