AlgebraicGeometry.Polarisation.locIsoOnBase_iff_nonempty_iso_of_isLocalRing
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace Polarisation_locIsoOnBase_iff_nonempty_iso_of_isLocalRing
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.PolarisationLean source · statement
theorem _root_.AlgebraicGeometry.Polarisation.locIsoOnBase_iff_nonempty_iso_of_isLocalRing
{S : Type} [CommRing S] [IsLocalRing S] {X : Scheme.{0}} (g : X ⟶ Spec (CommRingCat.of S)) (M
M' : X.Modules) :
LocIsoOnBase g M M' ↔ Nonempty (M ≅ M')