Module

Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap

20 declarations indexed from sourceView source ↗

Module documentation

Descent of invertible ideal sheaves

An ideal sheaf is invertible if its inverse image is invertible under a finite, flat, surjective scheme morphism.

Imports14

Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.Localization.Free
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.Finiteness.Descent
Mathlib.RingTheory.Localization.Algebra
Mathlib.RingTheory.LocalRing.Module
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.IsTensorProduct
Nyll.AlgebraicCurves.RelativeDivisors.Cartier

Imported by2

def

equivSpanSingletonOfMemNonZeroDivisors

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.equivSpanSingletonOfMemNonZeroDivisors

Documentation

Multiplication identifies the ring with the ideal generated by a non-zero-divisor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section FreeIdeal
variable {R : Type*} [CommRing R]
open scoped _root_.Ideal in

Lean source · statement

def Ideal.equivSpanSingletonOfMemNonZeroDivisors {g : R}
    (hg : g ∈ nonZeroDivisors R) : R ≃ₗ[R] (Ideal.span {g} : Ideal R)

theorem

free_span_singleton_of_mem_nonZeroDivisors

L66 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.free_span_singleton_of_mem_nonZeroDivisors

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section FreeIdeal
variable {R : Type*} [CommRing R]
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.free_span_singleton_of_mem_nonZeroDivisors {g : R} (hg : g ∈ nonZeroDivisors R) :
    Module.Free R (Ideal.span {g} : Ideal R)

theorem

eq_bot_or_exists_span_singleton_nonZeroDivisor_of_free

L71 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.eq_bot_or_exists_span_singleton_nonZeroDivisor_of_free

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section FreeIdeal
variable {R : Type*} [CommRing R]
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.eq_bot_or_exists_span_singleton_nonZeroDivisor_of_free (I : Ideal R)
    [Module.Free R I] : I = ⊥ ∨ ∃ j ∈ nonZeroDivisors R, I = Ideal.span {j}

theorem

exists_nonZeroDivisor_map_eq_span_of_algEquiv

L128 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.exists_nonZeroDivisor_map_eq_span_of_algEquiv

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section Transport
variable {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S']
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.exists_nonZeroDivisor_map_eq_span_of_algEquiv (e : S ≃ₐ[R] S') (I : Ideal R)
    (h : ∃ g ∈ nonZeroDivisors S, I.map (algebraMap R S) = Ideal.span {g}) :
    ∃ g ∈ nonZeroDivisors S', I.map (algebraMap R S') = Ideal.span {g}

theorem

fg_of_localizationSpan'

L150 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Submodule.fg_of_localizationSpan'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section LocalAndDescent
variable {A : Type u} [CommRing A]
open scoped _root_.Submodule in

Lean source · statement

theorem Submodule.fg_of_localizationSpan' {M : Type*} [AddCommGroup M] [Module A M]
    {N : Submodule A M} (s : Set A) (hs : Ideal.span s = ⊤)
    {Mₚ : ∀ (_ : s), Type*} [∀ (g : s), AddCommGroup (Mₚ g)] [∀ (g : s), Module A (Mₚ g)]
    {Rₚ : ∀ (_ : s), Type u} [∀ (g : s), CommRing (Rₚ g)] [∀ (g : s), Algebra A (Rₚ g)]
    [∀ (g : s), IsLocalization.Away g.val (Rₚ g)]
    [∀ (g : s), Module (Rₚ g) (Mₚ g)] [∀ (g : s), IsScalarTower A (Rₚ g) (Mₚ g)]
    (ϕ : ∀ (g : s), M →ₗ[A] Mₚ g) [∀ (g : s), IsLocalizedModule (Submonoid.powers g.val) (ϕ g)]
    (H : ∀ (g : s), (N.localized' (Rₚ g) (Submonoid.powers g.1) (ϕ g)).FG) :
    N.FG

theorem

of_localizationSpan_of_isLocalizedModule

L169 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Module.FinitePresentation.of_localizationSpan_of_isLocalizedModule

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section LocalAndDescent
variable {A : Type u} [CommRing A]
open scoped _root_.Module _root_.Module.FinitePresentation in

Lean source · statement

theorem Module.FinitePresentation.of_localizationSpan_of_isLocalizedModule
    {M : Type*} [AddCommGroup M] [Module A M] (s : Set A) (hs : Ideal.span s = ⊤)
    {Mₚ : ∀ (_ : s), Type*} [∀ (g : s), AddCommGroup (Mₚ g)] [∀ (g : s), Module A (Mₚ g)]
    {Rₚ : ∀ (_ : s), Type u} [∀ (g : s), CommRing (Rₚ g)] [∀ (g : s), Algebra A (Rₚ g)]
    [∀ (g : s), IsLocalization.Away g.val (Rₚ g)]
    [∀ (g : s), Module (Rₚ g) (Mₚ g)] [∀ (g : s), IsScalarTower A (Rₚ g) (Mₚ g)]
    (ϕ : ∀ (g : s), M →ₗ[A] Mₚ g) [∀ (g : s), IsLocalizedModule (Submonoid.powers g.val) (ϕ g)]
    (h : ∀ (g : s), Module.FinitePresentation (Rₚ g) (Mₚ g)) :
    Module.FinitePresentation A M

theorem

of_finitePresentation_tensorProduct_of_faithfullyFlat'

L192 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Module.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section LocalAndDescent
variable {A : Type u} [CommRing A]
variable (B : Type*) [CommRing B] [Algebra A B]
open scoped _root_.Module _root_.Module.FinitePresentation in

Lean source · statement

theorem Module.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat'
    (M : Type*) [AddCommGroup M] [Module A M] [Module.FaithfullyFlat A B]
    [Module.FinitePresentation B (B ⊗[A] M)] : Module.FinitePresentation A M

theorem

nonempty_tensorProduct_linearEquiv_map

L216 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.nonempty_tensorProduct_linearEquiv_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section LocalAndDescent
variable {A : Type u} [CommRing A]
variable (B : Type*) [CommRing B] [Algebra A B]
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.nonempty_tensorProduct_linearEquiv_map [Module.Flat A B] (J : Ideal A) :
    Nonempty (B ⊗[A] J ≃ₗ[B] (J.map (algebraMap A B) : Ideal B))

theorem

free_map_of_free_localizedModule

L242 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.free_map_of_free_localizedModule

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section LocalAndDescent
variable {A : Type u} [CommRing A]
variable (B : Type*) [CommRing B] [Algebra A B]
variable {B}
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.free_map_of_free_localizedModule (J : Ideal A) (r : A)
    [Module.Free (Localization (.powers r)) (LocalizedModule (.powers r) J)]
    (Aᵣ : Type*) [CommRing Aᵣ] [Algebra A Aᵣ] [IsLocalization.Away r Aᵣ] :
    Module.Free Aᵣ (J.map (algebraMap A Aᵣ) : Ideal Aᵣ)

theorem

exists_span_singleton_nonZeroDivisor_of_faithfullyFlat

L272 ↗

Ideal.exists_span_singleton_nonZeroDivisor_of_faithfullyFlat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section Main
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
namespace Ideal
open scoped _root_.Ideal in

Lean source · statement

theorem _root_.Ideal.exists_span_singleton_nonZeroDivisor_of_faithfullyFlat
    [Module.FaithfullyFlat A B]
    (J : Ideal A)
    (hB : ∀ 𝔮 : PrimeSpectrum B, ∃ u ∉ 𝔮.asIdeal, ∃ g ∈ nonZeroDivisors (Localization.Away u),
      (J.map (algebraMap A B)).map (algebraMap B (Localization.Away u)) = Ideal.span {g})
    (𝔭 : PrimeSpectrum A) :
    ∃ s ∉ 𝔭.asIdeal, ∃ j ∈ nonZeroDivisors (Localization.Away s),
      J.map (algebraMap A (Localization.Away s)) = Ideal.span {j}

theorem

exists_span_singleton_nonZeroDivisor_of_faithfullyFlat'

L386 ↗

Ideal.exists_span_singleton_nonZeroDivisor_of_faithfullyFlat'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section Main
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
namespace Ideal
open scoped _root_.Ideal in

Lean source · statement

theorem _root_.Ideal.exists_span_singleton_nonZeroDivisor_of_faithfullyFlat'
    [Module.FaithfullyFlat A B] (J : Ideal A)
    (hB : ∀ 𝔮 : PrimeSpectrum B, ∃ u ∉ 𝔮.asIdeal, ∃ g ∈ nonZeroDivisors (Localization.Away u),
      (J.map (algebraMap A B)).map (algebraMap B (Localization.Away u)) = Ideal.span {g})
    (𝔭 : PrimeSpectrum A) :
    ∃ s ∉ 𝔭.asIdeal, ∀ (Aₛ : Type*) [CommRing Aₛ] [Algebra A Aₛ] [IsLocalization.Away s Aₛ],
      ∃ j ∈ nonZeroDivisors Aₛ, J.map (algebraMap A Aₛ) = Ideal.span {j}

theorem

exists_span_singleton_nonZeroDivisor_of_flat_of_surjective

L399 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Ideal.exists_span_singleton_nonZeroDivisor_of_flat_of_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
section Main
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
open scoped _root_.Ideal in

Lean source · statement

theorem Ideal.exists_span_singleton_nonZeroDivisor_of_flat_of_surjective [Module.Flat A B]
    (hsurj : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))) (J : Ideal A)
    (hB : ∀ 𝔮 : PrimeSpectrum B, ∃ u ∉ 𝔮.asIdeal, ∃ g ∈ nonZeroDivisors (Localization.Away u),
      (J.map (algebraMap A B)).map (algebraMap B (Localization.Away u)) = Ideal.span {g})
    (𝔭 : PrimeSpectrum A) :
    ∃ s ∉ 𝔭.asIdeal, ∃ j ∈ nonZeroDivisors (Localization.Away s),
      J.map (algebraMap A (Localization.Away s)) = Ideal.span {j}

theorem

ker_algebraMap_eq_map_ker

L420 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.Algebra.IsPushout.ker_algebraMap_eq_map_ker

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
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

L463 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.CommRingCat.ker_eq_map_ker_of_isPushout

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
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

L488 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_top

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L499 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
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

L533 ↗

AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isAffineHom

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.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

chart

L553 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.InvertibleIdealDescent.chart

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
section SchemeGlue
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace InvertibleIdealDescent

Lean source · statement

theorem chart {X Y : Scheme.{u}} (π : Y ⟶ X) [IsAffineHom π] [Flat π] [Surjective π]
    (I : X.IdealSheafData) (h : (I.comap π).IsInvertible) (U : X.affineOpens) (x : X)
    (hxU : x ∈ (U : X.Opens)) :
    ∃ s : Γ(X, U), x ∈ X.basicOpen s ∧
      ∃ g ∈ nonZeroDivisors Γ(X, X.affineBasicOpen s),
        I.ideal (X.affineBasicOpen s) = Ideal.span {g}

theorem

isInvertible_of_isInvertible_comap

L632 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_isInvertible_of_isInvertible_comap.InvertibleIdealDescent.isInvertible_of_isInvertible_comap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
section SchemeGlue
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace InvertibleIdealDescent

Lean source · statement

theorem isInvertible_of_isInvertible_comap {X Y : Scheme.{u}} (π : Y ⟶ X) [IsAffineHom π] [Flat π]
    [Surjective π] (I : X.IdealSheafData) (h : (I.comap π).IsInvertible) : I.IsInvertible

theorem

isInvertible_of_isInvertible_comap

L645 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_of_isInvertible_comap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_isInvertible_of_isInvertible_comap
universe u
open TensorProduct
open CategoryTheory CategoryTheory.Limits TensorProduct
open CategoryTheory _root_.AlgebraicGeometry AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_of_isInvertible_comap
    {X Y : Scheme.{u}} (π : Y ⟶ X) [IsFinite π] [Flat π] [Surjective π]
    (I : X.IdealSheafData) (h : (I.comap π).IsInvertible) : I.IsInvertible

Module documentation

Descent of invertible ideal sheaves

Declarations