AlgebraicGeometry.bijective_appTop_of_bijective_appTop_pullback_snd_of_faithfullyFlat
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_of_bijective_appTop_pullback_snd_of_faithfullyFlat
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProductLean source · statement
theorem _root_.AlgebraicGeometry.bijective_appTop_of_bijective_appTop_pullback_snd_of_faithfullyFlat
{k : Type u} [CommRing k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
[CompactSpace X] [QuasiSeparatedSpace X]
(A : Type u) [CommRing A] [Algebra k A] [Module.FaithfullyFlat k A]
(hA : Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
(pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k A)))).appTop).hom) :
Function.Bijective ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ fX.appTop).hom