NYLL
Module

bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.lean

Nyll.AlgebraicCurves.Geometry.Schemes.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
8 declarations indexed from sourceView source ↗

Module documentation

Transfer bijectivity of algebra maps on affine base changes to sections of arbitrary base changes.

Imports2
Imported by2

Declarations

lemma

bijective_of_square

L39 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.bijective_of_square
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
Lean source · statement
lemma bijective_of_square {A B A' B' : CommRingCat.{u}} {f : A ⟶ B} {f' : A' ⟶ B'} (a : A ⟶ A')
    (b : B ⟶ B')
    [IsIso a] [IsIso b] (h : f ≫ b = a ≫ f') (hf : Function.Bijective f) : Function.Bijective f'
lemma

isIso_appTop

L50 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.isIso_appTop
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
Lean source · statement
lemma isIso_appTop {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] : IsIso f.appTop
lemma

isIso_of_bijective

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.isIso_of_bijective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
Lean source · statement
lemma isIso_of_bijective {A B : CommRingCat.{u}} (f : A ⟶ B) (hf : Function.Bijective f) : IsIso
    f
lemma

isIso_of_isIso_app_basis

L59 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.isIso_of_isIso_app_basis
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
Lean source · statement
lemma isIso_of_isIso_app_basis {X : TopCat.{u}} {ι : Type u} {B : ι → Opens X} (hB :
    Opens.IsBasis (Set.range B))
    (F G : TopCat.Sheaf CommRingCat.{u} X) (φ : F.1 ⟶ G.1) (h : ∀ i, IsIso (φ.app (op (B i)))) :
      IsIso φ
lemma

bijective_appTop_snd_of_iso

L84 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.bijective_appTop_snd_of_iso
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
lemma bijective_appTop_snd_of_iso {T₁ T₂ : Scheme.{u}} (t₁ : T₁ ⟶ Spec (CommRingCat.of R)) (e :
    T₂ ≅ T₁)
    (h : Function.Bijective (pullback.snd c t₁).appTop) :
    Function.Bijective (pullback.snd c (e.hom ≫ t₁)).appTop
lemma

bijective_app_of_bijective_appTop_restrict

L98 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.bijective_app_of_bijective_appTop_restrict
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
lemma bijective_app_of_bijective_appTop_restrict {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of
    R)) (U : T.Opens)
    (h : Function.Bijective (pullback.snd c (U.ι ≫ t)).appTop) :
    Function.Bijective ((pullback.snd c t).app U)
lemma

bijective_appTop_restrict_of_affine

L129 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections.AlgebraicGeometry.SectionsBaseChangeAux.bijective_appTop_restrict_of_affine
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SectionsBaseChangeAux
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
Lean source · full declaration
lemma bijective_appTop_restrict_of_affine {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (U
    : T.Opens)
    (hU : IsAffineOpen U)
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
        A), ⊤))) :
    Function.Bijective (pullback.snd c (U.ι ≫ t)).appTop := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom t U
  have h0 := hH0 Γ(T, U)
  set sA := Scheme.TwoAffineOpenCover.specMap R Γ(T, U) with hsA
  have h1 : Function.Bijective (pullback.snd c sA).appTop := by
    have h0' : Function.Bijective (((pullback.snd c sA).appLE ⊤ ⊤ le_top).hom ∘
        (Scheme.ΓSpecIso (.of Γ(T, U))).inv.hom) := h0
    have h0'' := (Function.Bijective.of_comp_iff _
      (ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso (.of Γ(T, U))).inv)).mp h0'
    have : (pullback.snd c sA).appLE ⊤ ⊤ le_top = (pullback.snd c sA).appTop :=
      (Scheme.Hom.app_eq_appLE _).symm
    rwa [this] at h0''
  have hE : hU.isoSpec.hom ≫ sA = U.ι ≫ t := by
    rw [← Iso.eq_inv_comp, hsA, Scheme.TwoAffineOpenCover.specMap]
    change Spec.map ((Scheme.ΓSpecIso (.of R)).inv ≫ t.appLE ⊤ U le_top) = _
    rw [Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ← IsAffineOpen.fromSpec_top,
      IsAffineOpen.SpecMap_appLE_fromSpec t (isAffineOpen_top _) hU le_top, ← Category.assoc,
      IsAffineOpen.isoSpec_inv_ι]
  rw [← hE]
  exact bijective_appTop_snd_of_iso c sA hU.isoSpec h1
theorem

bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections

L161 ↗
AlgebraicGeometry.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open AlgebraicGeometry.SectionsBaseChangeAux in
Lean source · full declaration
theorem
    _root_.AlgebraicGeometry.bijective_appTop_pullback_snd_of_forall_bijective_algebraMap_sections
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      letI := Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
        A), ⊤)))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Function.Bijective (pullback.snd c t).appTop := by
  set p := pullback.snd c t
  have hB : Opens.IsBasis (Set.range (Subtype.val : T.affineOpens → T.Opens)) := by
    rw [Subtype.range_coe]; exact T.isBasis_affineOpens
  have hiso : IsIso p.c := by
    refine isIso_of_isIso_app_basis hB T.sheaf ((TopCat.Sheaf.pushforward _ p.base).obj
      (pullback c t).sheaf) p.c
      (fun U => isIso_of_bijective _ ?_)
    exact bijective_app_of_bijective_appTop_restrict c t U.1
      (bijective_appTop_restrict_of_affine c t U.1 U.2 hH0)
  have : IsIso (p.c.app (op ⊤)) := @NatIso.isIso_app_of_isIso _ _ _ _ _ _ p.c hiso (op ⊤)
  exact ConcreteCategory.bijective_of_isIso (p.c.app (op ⊤))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.