AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.comap_of_isOpenImmersion
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_comap_of_isOpenImmersion
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.comap_of_isOpenImmersion
{X Y : Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsInvertible) (j : Y ⟶ X) [IsOpenImmersion j]
:
(I.comap j).IsInvertible