Module

AbelianSchemePropertyBundle_bijective_specIso_inv_comp_appTop_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_bijective_specIso_inv_comp_appTop_of_isPullback

1 declaration indexed from sourceView source ↗

Module documentation

Abelian Scheme Property Bundle bijective spec Iso inv comp app Top of is Pullback

Imports6

Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.CategoryTheory.ConcreteCategory.Basic
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_bijective_algebraMap_sections_pullback

Imported by4

theorem

bijective_specIso_inv_comp_appTop_of_isPullback

L95 ↗

GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_specIso_inv_comp_appTop_of_isPullback

Source context 6 commands

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

section ProofImplementation
namespace GoodReductionJacobian.AbelianSchemePropertyBundle
universe u
open _root_.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs in
open AbelianSchemePropertyBundle_bijective_specIso_inv_comp_appTop_of_isPullback in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry GoodReductionJacobian in

Lean source · statement

theorem bijective_specIso_inv_comp_appTop_of_isPullback
    {S : Type u} [CommRing S] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of S)}
    (hA : AbelianSchemePropertyBundle S f)
    {T : Type u} [CommRing T] (φ : S →+* T)
    {A' : Scheme.{u}} (f' : A' ⟶ Spec (CommRingCat.of T)) (g : A' ⟶ A)
    (hg : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))) :
    Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of T)).inv ≫ f'.appTop).hom

Module documentation

Abelian Scheme Property Bundle bijective spec Iso inv comp app Top of is Pullback

Declarations

bijective_specIso_inv_comp_appTop_of_isPullback