Module

Scheme_IdealSheafData_IsInvertible_isIso_pullbackModuleComparison.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isIso_pullbackModuleComparison

1 declaration indexed from sourceView source ↗

Module documentation

Invertible ideal-module pullback comparisons

For invertible ideal sheaves on both schemes, the pullback module comparison is an isomorphism.

Imports6

Imported by38

theorem

isIso_pullbackModuleComparison

L37 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isIso_pullbackModuleComparison

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isIso_pullbackModuleComparison
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isIso_pullbackModuleComparison
  {X X' : Scheme.{u}} (f : X' ⟶ X) {I : X.IdealSheafData} (hI : I.IsInvertible)
    (hI' : (I.comap f).IsInvertible) : IsIso (I.pullbackModuleComparison f)

Module documentation

Invertible ideal-module pullback comparisons

Declarations

isIso_pullbackModuleComparison