AlgebraicGeometry.SmallExtension.IsFibreReading.eq_zero_of_isFibreReading_zero_of_flat
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace SmallExtension_IsFibreReading_eq_zero_of_isFibreReading_zero_of_flat
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
universe uLean source · statement
theorem
_root_.AlgebraicGeometry.SmallExtension.IsFibreReading.eq_zero_of_isFibreReading_zero_of_flat
{B₁ : Type u} [CommRing B₁] [IsLocalRing B₁]
(V : Type u) [AddCommGroup V] [Module (ResidueField B₁) V] [Module.Finite (ResidueField B₁) V]
[Module B₁ V] [IsScalarTower B₁ (ResidueField B₁) V] (ι : V →ₗ[B₁] B₁)
{X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁)) [Flat f]
{Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of (ResidueField B₁))) (i : Xk ⟶ X)
(hi : IsPullback i fk f (Spec.map (CommRingCat.ofHom (residue B₁))))
(U : X.Opens) (hU : IsAffineOpen U) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (hW' : i ⁻¹ᵁ U ≤ W)
(δ : Γ(X, U)) (hδ : IsFibreReading V ι f fk i U W hW δ 0) :
δ = 0