NYLL
Module

Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
15 declarations indexed from sourceView source ↗

Module documentation

Fibrewise invertibility of a zero ideal

For an invertible module on a flat locally finite-type scheme, invertibility of the section zero ideal in every geometric fibre implies global invertibility and flatness of the zero subscheme over the base.

Imports22
Imported by4

Declarations

theorem

ker_algebraMap_eq_map_ker

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.Algebra.IsPushout.ker_algebraMap_eq_map_ker
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace Algebra
open _root_.Algebra
namespace IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra
Lean source · statement
theorem ker_algebraMap_eq_map_ker
    (R B C P : Type*) [CommRing R] [CommRing B] [CommRing C] [CommRing P]
    [Algebra R B] [Algebra R C] [Algebra B P] [Algebra C P] [Algebra R P]
    [IsScalarTower R B P] [IsScalarTower R C P] [Algebra.IsPushout R B C P]
    (hC : Function.Surjective (algebraMap R C)) :
    RingHom.ker (algebraMap B P) = (RingHom.ker (algebraMap R C)).map (algebraMap R B)
theorem

ker_eq_map_ker_of_isPushout

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.CommRingCat.ker_eq_map_ker_of_isPushout
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace CommRingCat
open _root_.CommRingCat
open _root_.CommRingCat
Lean source · statement
theorem ker_eq_map_ker_of_isPushout {R B C P : CommRingCat.{u}} {f : R ⟶ B} {g : R ⟶ C}
    {inl : B ⟶ P} {inr : C ⟶ P} (h : IsPushout f g inl inr)
    (hg : Function.Surjective g.hom) :
    RingHom.ker inl.hom = (RingHom.ker g.hom).map f.hom
theorem

ideal_comap_top

L133 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_top
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData hiding ideal_comap_of_le
open _root_.AlgebraicGeometry.Scheme hiding IdealSheafData.ideal_comap_of_le
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_top [IsAffine X] [IsAffine Y] (I : X.IdealSheafData) (f : Y ⟶ X) :
    (I.comap f).ideal ⟨⊤, isAffineOpen_top Y⟩ =
      (I.ideal ⟨⊤, isAffineOpen_top X⟩).map f.appTop.hom
theorem

ideal_comap_of_le

L144 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData hiding ideal_comap_of_le
open _root_.AlgebraicGeometry.Scheme hiding IdealSheafData.ideal_comap_of_le
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_of_le (I : X.IdealSheafData) (f : Y ⟶ X) (U : X.affineOpens)
    (V : Y.affineOpens) (hVU : (V : Y.Opens) ≤ f ⁻¹ᵁ (U : X.Opens)) :
    (I.comap f).ideal V = (I.ideal U).map (f.appLE U V hVU).hom
theorem

ideal_comap_of_isAffineHom

L180 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isAffineHom
Source context 20 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData hiding ideal_comap_of_le
open _root_.AlgebraicGeometry.Scheme hiding IdealSheafData.ideal_comap_of_le
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_of_isAffineHom (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f]
    (U : X.affineOpens) :
    (I.comap f).ideal ⟨f ⁻¹ᵁ U, U.2.preimage f⟩ = (I.ideal U).map (f.app U).hom
theorem

mem_nonZeroDivisors_of_span_eq_span

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.mem_nonZeroDivisors_of_span_eq_span
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem mem_nonZeroDivisors_of_span_eq_span {R : Type*} [CommRing R] {a b : R}
    (h : Ideal.span {a} = Ideal.span {b}) (hb : b ∈ nonZeroDivisors R) : a ∈ nonZeroDivisors R
theorem

mem_nonZeroDivisors_of_ideal_eq_span

L203 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.mem_nonZeroDivisors_of_ideal_eq_span
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem mem_nonZeroDivisors_of_ideal_eq_span {Y : Scheme.{u}} {J : Y.IdealSheafData}
    (hJ : J.IsInvertible) (W : Y.affineOpens) (γ : Γ(Y, W)) (hW : J.ideal W = Ideal.span {γ}) :
    γ ∈ nonZeroDivisors Γ(Y, W)
theorem

isInvertible_of_forall_exists

L251 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.isInvertible_of_forall_exists
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem isInvertible_of_forall_exists {X : Scheme.{u}} (I : X.IdealSheafData)
    (h : ∀ x : X, ∃ (U : X.affineOpens) (g : Γ(X, U)),
      x ∈ U.1 ∧ g ∈ nonZeroDivisors Γ(X, U) ∧ I.ideal U = Ideal.span {g}) :
    I.IsInvertible
theorem

flat_subschemeι_comp_of_forall_exists

L265 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.flat_subschemeι_comp_of_forall_exists
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem flat_subschemeι_comp_of_forall_exists {X T : Scheme.{u}} (q : X ⟶ T) (I : X.IdealSheafData)
    (h : ∀ x : X, ∃ (V : T.affineOpens) (U : X.affineOpens) (hUV : U.1 ≤ q ⁻¹ᵁ V.1),
      x ∈ U.1 ∧ ((Ideal.Quotient.mk (I.ideal U)).comp (q.appLE V U hUV).hom).Flat) :
    Flat (I.subschemeι ≫ q)
theorem

mem_nonZeroDivisors_of_injective

L304 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.mem_nonZeroDivisors_of_injective
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem mem_nonZeroDivisors_of_injective {R S F : Type*} [CommRing R] [CommRing S]
    [FunLike F R S] [MulHomClass F R S] [ZeroHomClass F R S] (e : F) (he : Function.Injective e)
    {r : R} (h : e r ∈ nonZeroDivisors S) : r ∈ nonZeroDivisors R
theorem

tmul_one_mem_nonZeroDivisors_of_isPushout

L311 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.tmul_one_mem_nonZeroDivisors_of_isPushout
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · full declaration
theorem tmul_one_mem_nonZeroDivisors_of_isPushout {R B C P : CommRingCat.{u}} {f : R ⟶ B}
    {g : R ⟶ C} {inl : B ⟶ P} {inr : C ⟶ P} (h : IsPushout f g inl inr) (b : B)
    (hb : inl b ∈ nonZeroDivisors P) :
    letI := f.hom.toAlgebra
    letI := g.hom.toAlgebra
    (b ⊗ₜ[R] (1 : C)) ∈ nonZeroDivisors (B ⊗[R] C) := by
  algebraize [f.hom, g.hom, inl.hom, inr.hom, inl.hom.comp f.hom]
  have hw : inl.hom.comp f.hom = inr.hom.comp g.hom := by
    simpa only [CommRingCat.hom_comp] using congr(($(h.w)).hom)
  have : IsScalarTower R C P := .of_algebraMap_eq' hw
  have : Algebra.IsPushout R B C P := CommRingCat.isPushout_iff_isPushout.mp h
  let e : B ⊗[R] C ≃ₐ[B] P := Algebra.IsPushout.equiv R B C P
  refine mem_nonZeroDivisors_of_injective e e.injective ?_
  have he : e (b ⊗ₜ[R] (1 : C)) = inl b := by
    change Algebra.IsPushout.equiv R B C P (b ⊗ₜ[R] (1 : C)) = _
    rw [Algebra.IsPushout.equiv_tmul, map_one, mul_one]
    rfl
  rwa [he]
theorem

appLE_SpecMap_fromSpec_comp_ΓSpecIso

L330 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.appLE_SpecMap_fromSpec_comp_ΓSpecIso
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem appLE_SpecMap_fromSpec_comp_ΓSpecIso {T : Scheme.{u}} (V : T.affineOpens)
    (K : Type u) [CommRing K] [Algebra Γ(T, V) K]
    (h : (⊤ : (Spec (CommRingCat.of K)).Opens) ≤
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(T, V) K)) ≫ V.2.fromSpec) ⁻¹ᵁ V.1) :
    (Spec.map (CommRingCat.ofHom (algebraMap Γ(T, V) K)) ≫ V.2.fromSpec).appLE V ⊤ h ≫
      (Scheme.ΓSpecIso (CommRingCat.of K)).hom = CommRingCat.ofHom (algebraMap Γ(T, V) K)
theorem

tmul_one_mem_nonZeroDivisors_of_isInvertible_comap

L378 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.tmul_one_mem_nonZeroDivisors_of_isInvertible_comap
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · full declaration
theorem tmul_one_mem_nonZeroDivisors_of_isInvertible_comap
    {X T : Scheme.{u}} (q : X ⟶ T) (I : X.IdealSheafData) (V : T.affineOpens) (U : X.affineOpens)
    (hUV : U.1 ≤ q ⁻¹ᵁ V.1) (g : Γ(X, U)) (hI : I.ideal U = Ideal.span {g})
    (K : Type u) [CommRing K] [Algebra Γ(T, V) K]
    (hinv : (I.comap (pullback.fst q
      (Spec.map (CommRingCat.ofHom (algebraMap Γ(T, V) K)) ≫ V.2.fromSpec))).IsInvertible) :
    letI := (q.appLE V U hUV).hom.toAlgebra
    (g ⊗ₜ[Γ(T, V)] (1 : K)) ∈ nonZeroDivisors (Γ(X, U) ⊗[Γ(T, V)] K) := by
  set ψ : CommRingCat.of ↑Γ(T, V) ⟶ CommRingCat.of K :=
    CommRingCat.ofHom (algebraMap Γ(T, V) K) with hψ
  set xbar : Spec (CommRingCat.of K) ⟶ T := Spec.map ψ ≫ V.2.fromSpec with hxbar
  have hUST : (⊤ : (Spec (CommRingCat.of K)).Opens) ≤ xbar ⁻¹ᵁ V.1 := by
    rintro p -
    change xbar.base p ∈ V.1
    have hp : V.2.fromSpec.base ((Spec.map ψ).base p) ∈ Set.range V.2.fromSpec.base := ⟨_, rfl⟩
    rw [V.2.range_fromSpec] at hp
    simpa [hxbar] using hp
  have H : IsPullback (pullback.fst q xbar) (pullback.snd q xbar) q xbar :=
    IsPullback.of_hasPullback q xbar
  let UY : (pullback q xbar).Opens := pullback.fst q xbar ⁻¹ᵁ U.1 ⊓ pullback.snd q xbar ⁻¹ᵁ ⊤
  have hpo := (isIso_pushoutSection_iff H hUST hUV (UY := UY) rfl).mp
    (isIso_pushoutSection_of_isAffineOpen H hUST hUV rfl V.2 (isAffineOpen_top _) U.2)
  have hUY : IsAffineOpen UY := by
    have : IsAffine (V.1 : Scheme.{u}) := V.2
    have : IsAffine ((⊤ : (Spec (CommRingCat.of K)).Opens) : Scheme.{u}) := isAffineOpen_top _
    have : IsAffine (U.1 : Scheme.{u}) := U.2
    exact .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUV (UY := UY) rfl).isoPullback.hom
  have hle : UY ≤ pullback.fst q xbar ⁻¹ᵁ U.1 := inf_le_left
  have hideal := AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le I (pullback.fst q xbar)
    U ⟨UY, hUY⟩ hle
  rw [hI, Ideal.map_span, Set.image_singleton] at hideal
  have hγ : ((pullback.fst q xbar).appLE U UY hle).hom g ∈
      nonZeroDivisors Γ(pullback q xbar, UY) :=
    mem_nonZeroDivisors_of_ideal_eq_span hinv ⟨UY, hUY⟩ _ hideal
  have h1 := tmul_one_mem_nonZeroDivisors_of_isPushout hpo g hγ
  let := (q.appLE V U hUV).hom.toAlgebra
  let algC : Algebra Γ(T, V) Γ(Spec (CommRingCat.of K), ⊤) := (xbar.appLE V ⊤ hUST).hom.toAlgebra
  have hcompat := appLE_SpecMap_fromSpec_comp_ΓSpecIso V K hUST
  let θ : Γ(Spec (CommRingCat.of K), ⊤) ≃ₐ[Γ(T, V)] K :=
    AlgEquiv.ofRingEquiv (f := (Scheme.ΓSpecIso (CommRingCat.of K)).commRingCatIsoToRingEquiv)
      (fun a => by
        change (Scheme.ΓSpecIso (CommRingCat.of K)).hom ((xbar.appLE V ⊤ hUST) a) = algebraMap _ K a
        rw [← CommRingCat.comp_apply, hcompat]
        rfl)
  let E : Γ(X, U) ⊗[Γ(T, V)] Γ(Spec (CommRingCat.of K), ⊤) ≃ₐ[Γ(T, V)] Γ(X, U) ⊗[Γ(T, V)] K :=
    Algebra.TensorProduct.congr AlgEquiv.refl θ
  refine mem_nonZeroDivisors_of_injective E.symm E.symm.injective ?_
  have hE : E (g ⊗ₜ[Γ(T, V)] (1 : Γ(Spec (CommRingCat.of K), ⊤))) = g ⊗ₜ[Γ(T, V)] (1 : K) := by
    change Algebra.TensorProduct.congr AlgEquiv.refl θ (g ⊗ₜ 1) = _
    rw [Algebra.TensorProduct.congr_apply, Algebra.TensorProduct.map_tmul, map_one]
    rfl
  rw [← hE, AlgEquiv.symm_apply_apply]
  exact h1
theorem

isInvertible_and_flat_of_locally_principal

L436 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat.ZDFlatG.isInvertible_and_flat_of_locally_principal
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
namespace ZDFlatG
Lean source · statement
theorem isInvertible_and_flat_of_locally_principal
    {X T : Scheme.{u}} (q : X ⟶ T) [Flat q] [LocallyOfFiniteType q] [IsLocallyNoetherian T]
    (Z : X.IdealSheafData)
    (hloc : ∀ (x : X) (W : X.Opens), x ∈ W →
      ∃ (U : X.affineOpens) (g : Γ(X, U)), x ∈ U.1 ∧ U.1 ≤ W ∧ Z.ideal U = Ideal.span {g})
    (hfib : ∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ T),
      (Z.comap (pullback.fst q x)).IsInvertible) :
    Z.IsInvertible ∧ Flat (Z.subschemeι ≫ q)
theorem

isInvertible_zeroSchemeIdeal_and_flat

L477 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.isInvertible_zeroSchemeIdeal_and_flat
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isInvertible_zeroSchemeIdeal_and_flat
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry hiding Scheme.IdealSheafData.ideal_comap_of_le
open _root_.TensorProduct
open _root_.nonZeroDivisors
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.isInvertible_zeroSchemeIdeal_and_flat
    {X T : Scheme.{u}} (q : X ⟶ T) [Flat q] [LocallyOfFiniteType q] [IsLocallyNoetherian T]
    {M : X.Modules} (hM : Scheme.Modules.IsInvertible M) (s : 𝟙_ X.Modules ⟶ M)
    (hfib : ∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ T),
      ((Scheme.Modules.zeroSchemeIdeal s).comap (pullback.fst q x)).IsInvertible) :
    (Scheme.Modules.zeroSchemeIdeal s).IsInvertible ∧
      Flat ((Scheme.Modules.zeroSchemeIdeal s).subschemeι ≫ q)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.