AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_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_Modules_isIso_baseChangeHom_of_isOpenImmersion
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_of_isOpenImmersion
{X T Y S : Scheme.{u}} {π : X ⟶ T} {j : S ⟶ T} [IsOpenImmersion j] {ρ : Y ⟶ S} {u : Y ⟶ X}
(hu : IsPullback u ρ π j) (F : X.Modules) :
IsIso (Scheme.Modules.baseChangeHom hu.w F)