NYLL
Module

AffineActionCoordinates.lean

Nyll.SchemeTheory.Descent.AffineActionCoordinates
20 declarations indexed from sourceView source ↗

Module documentation

Tensor coordinates for genuine descent actions

We transport an action across the equality between a composite structure map and its affine coordinate map. The resulting overlap isomorphism, its two base coordinates, and its diagonal restriction are expressed in tensor coordinates.

Imports7
Imported by3

Declarations

def

pullbackActionCongr

L36 ↗
AlgebraicGeometry.pullbackActionCongr
Documentation

Express an action using an equal composite structure map.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
Lean source · statement
def pullbackActionCongr : pullback f g ⟶ Z
lemma

pullbackActionCongr_invariant_iff

L40 ↗
AlgebraicGeometry.pullbackActionCongr_invariant_iff
Documentation

Invariance of a morphism under the action is unchanged by the coordinate transport.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
Lean source · statement
lemma pullbackActionCongr_invariant_iff {T : Scheme.{u}} (q : Z ⟶ T) :
    pullbackActionCongr f p g e a ≫ q = pullback.snd f g ≫ q ↔
      a ≫ q = pullback.snd f (p ≫ f) ≫ q
lemma

pullbackActionCongr_over

L50 ↗
AlgebraicGeometry.pullbackActionCongr_over
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
include ha in
Lean source · statement
lemma pullbackActionCongr_over : pullbackActionCongr f p g e a ≫ p = pullback.fst f g
lemma

pullbackActionCongr_base

L56 ↗
AlgebraicGeometry.pullbackActionCongr_base
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
include ha in
Lean source · statement
lemma pullbackActionCongr_base : pullbackActionCongr f p g e a ≫ g = pullback.fst f g ≫ f
def

pullbackActionOverlapCongrIso

L68 ↗
AlgebraicGeometry.pullbackActionOverlapCongrIso
Documentation

The geometric overlap isomorphism in the changed pullback coordinates.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 Z)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 Z)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
Lean source · statement
def pullbackActionOverlapCongrIso : pullback f g ≅ pullback g f
lemma

pullbackActionOverlapCongrIso_fst

L72 ↗
AlgebraicGeometry.pullbackActionOverlapCongrIso_fst
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 Z)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 Z)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
Lean source · statement
lemma pullbackActionOverlapCongrIso_fst :
    (pullbackActionOverlapCongrIso f p g e a ha hunit hassoc).hom ≫ pullback.fst g f =
      pullbackActionCongr f p g e a
lemma

pullbackActionOverlapCongrIso_snd

L81 ↗
AlgebraicGeometry.pullbackActionOverlapCongrIso_snd
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 Z)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 Z)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
Lean source · statement
lemma pullbackActionOverlapCongrIso_snd :
    (pullbackActionOverlapCongrIso f p g e a ha hunit hassoc).hom ≫ pullback.snd g f =
      pullback.snd f g ≫ p
lemma

pullbackActionOverlapCongrIso_diagonal

L90 ↗
AlgebraicGeometry.pullbackActionOverlapCongrIso_diagonal
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 Z)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 Z)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
Lean source · full declaration
lemma pullbackActionOverlapCongrIso_diagonal :
    pullback.lift (f := f) (g := g) p (𝟙 Z) (by rw [Category.id_comp, e]) ≫
        (pullbackActionOverlapCongrIso f p g e a ha hunit hassoc).hom =
      pullback.lift (f := g) (g := f) (𝟙 Z) p (by rw [Category.id_comp, e]) := by
  subst g
  simpa only [pullbackActionOverlapCongrIso, Iso.trans_hom, Iso.symm_hom,
    pullback.congrHom_hom, pullback.congrHom_inv, pullback.map_id,
    Category.id_comp, Category.comp_id] using
      pullbackActionOverlapIso_diagonal f p a ha hunit hassoc
lemma

pullbackActionCongr_assoc

L101 ↗
AlgebraicGeometry.pullbackActionCongr_assoc
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace AlgebraicGeometry
variable {X Y Z : Scheme.{u}} (f : Y ⟶ X) (p : Z ⟶ Y) (g : Z ⟶ X)
  (e : p ≫ f = g) (a : pullback f (p ≫ f) ⟶ Z)
variable (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 Z)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 Z)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hassoc in
Lean source · statement
lemma pullbackActionCongr_assoc :
    pullbackActionStep f g (pullbackActionCongr f p g e a)
        (pullbackActionCongr_base f p g e a ha) ≫ pullbackActionCongr f p g e a =
      pullbackSkipMiddle f g ≫ pullbackActionCongr f p g e a
lemma

specMap_tower

L117 ↗
Algebra.Descent.specMap_tower
Documentation

The algebra tower identifies the two actual maps to the affine base.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
lemma specMap_tower :
    Spec.map (CommRingCat.ofHom (algebraMap B C)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap R B)) =
      Spec.map (CommRingCat.ofHom (algebraMap R C))
def

affinePullbackOverlapIso

L125 ↗
Algebra.Descent.affinePullbackOverlapIso
Documentation

Tensor coordinates of an actual geometric overlap isomorphism.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
def affinePullbackOverlapIso
    (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
      pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (Spec.map (CommRingCat.ofHom (algebraMap R B)))) :
    Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B))
lemma

affinePullbackOverlapIso_action

L134 ↗
Algebra.Descent.affinePullbackOverlapIso_action
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
omit [Algebra B C] [IsScalarTower R B C] in
Lean source · statement
lemma affinePullbackOverlapIso_action
    (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
      pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (Spec.map (CommRingCat.ofHom (algebraMap R B)))) :
    affineOverlapAction R B C (affinePullbackOverlapIso R B C β) =
      β.hom ≫ pullback.fst _ _
lemma

affineSourceBase_fst

L145 ↗
Algebra.Descent.affineSourceBase_fst
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
lemma affineSourceBase_fst :
    Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) ≫
        Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom :
          B →+* B ⊗[R] B)) =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom :
        C →+* C ⊗[R] B)) ≫ Spec.map (CommRingCat.ofHom (algebraMap B C))
lemma

affineSourceBase_snd

L154 ↗
Algebra.Descent.affineSourceBase_snd
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
lemma affineSourceBase_snd :
    Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) ≫
        Spec.map (CommRingCat.ofHom ((Algebra.TensorProduct.includeRight :
          B →ₐ[R] B ⊗[R] B) : B →+* B ⊗[R] B)) =
      Spec.map (CommRingCat.ofHom ((Algebra.TensorProduct.includeRight :
        B →ₐ[R] C ⊗[R] B) : B →+* C ⊗[R] B))
lemma

affineTargetBase_fst

L167 ↗
Algebra.Descent.affineTargetBase_fst
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
lemma affineTargetBase_fst :
    Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom) ≫
        Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom :
          B →+* B ⊗[R] B)) =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom :
        B →+* B ⊗[R] C))
lemma

affineTargetBase_snd

L180 ↗
Algebra.Descent.affineTargetBase_snd
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
lemma affineTargetBase_snd :
    Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom) ≫
        Spec.map (CommRingCat.ofHom ((Algebra.TensorProduct.includeRight :
          B →ₐ[R] B ⊗[R] B) : B →+* B ⊗[R] B)) =
      Spec.map (CommRingCat.ofHom ((Algebra.TensorProduct.includeRight :
        C →ₐ[R] B ⊗[R] C) : C →+* B ⊗[R] C)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap B C))
lemma

affinePullbackOverlapIso_base

L197 ↗
Algebra.Descent.affinePullbackOverlapIso_base
Documentation

Preservation of the two geometric cover coordinates gives the full tensor-square base compatibility, including its second coordinate.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
    (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
  pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
    (Spec.map (CommRingCat.ofHom (algebraMap R B))))
Lean source · statement
lemma affinePullbackOverlapIso_base
    (hfst : β.hom ≫ pullback.fst _ _ ≫ Spec.map (CommRingCat.ofHom (algebraMap B C)) =
      pullback.fst _ _)
    (hsnd : β.hom ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ Spec.map (CommRingCat.ofHom (algebraMap B C))) :
    (affinePullbackOverlapIso R B C β).hom ≫
        Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom)
lemma

affineTargetDiagonal_chart

L217 ↗
Algebra.Descent.affineTargetDiagonal_chart
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
    (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
  pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
    (Spec.map (CommRingCat.ofHom (algebraMap R B))))
Lean source · full declaration
lemma affineTargetDiagonal_chart :
    Spec.map (CommRingCat.ofHom (tensorTargetDiagonal R B C).toRingHom) ≫
        (pullbackSpecIso R B C).inv =
      pullback.lift (f := Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (g := Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (Spec.map (CommRingCat.ofHom (algebraMap B C))) (𝟙 _) (by
          rw [Category.id_comp, specMap_tower R B C]) := by
  apply pullback.hom_ext
  · rw [Category.assoc, pullbackSpecIso_inv_fst, pullback.lift_fst, ← Spec.map_comp]
    congr 1
    ext b
    change tensorTargetDiagonal R B C (b ⊗ₜ[R] 1) = algebraMap B C b
    simp only [tensorTargetDiagonal, Algebra.TensorProduct.lift_tmul,
      Algebra.ofId_apply, AlgHom.id_apply, mul_one]
  · rw [Category.assoc, pullbackSpecIso_inv_snd, pullback.lift_snd,
      ← Spec.map_comp, ← Spec.map_id]
    congr 1
    ext c
    change tensorTargetDiagonal R B C (1 ⊗ₜ[R] c) = c
    simp only [tensorTargetDiagonal, Algebra.TensorProduct.lift_tmul,
      map_one, AlgHom.id_apply, one_mul]
lemma

affineSourceDiagonal_chart

L239 ↗
Algebra.Descent.affineSourceDiagonal_chart
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
    (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
  pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
    (Spec.map (CommRingCat.ofHom (algebraMap R B))))
Lean source · full declaration
lemma affineSourceDiagonal_chart :
    Spec.map (CommRingCat.ofHom (tensorSourceDiagonal R B C).toRingHom) ≫
        (pullbackSpecIso R C B).inv =
      pullback.lift (f := Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (g := Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (𝟙 _) (Spec.map (CommRingCat.ofHom (algebraMap B C))) (by
          rw [Category.id_comp, specMap_tower R B C]) := by
  apply pullback.hom_ext
  · rw [Category.assoc, pullbackSpecIso_inv_fst, pullback.lift_fst,
      ← Spec.map_comp, ← Spec.map_id]
    congr 1
    ext c
    change tensorSourceDiagonal R B C (c ⊗ₜ[R] 1) = c
    simp only [tensorSourceDiagonal, Algebra.TensorProduct.lift_tmul,
      map_one, AlgHom.id_apply, mul_one]
  · rw [Category.assoc, pullbackSpecIso_inv_snd, pullback.lift_snd, ← Spec.map_comp]
    congr 1
    ext b
    change tensorSourceDiagonal R B C (1 ⊗ₜ[R] b) = algebraMap B C b
    simp only [tensorSourceDiagonal, Algebra.TensorProduct.lift_tmul,
      map_one, IsScalarTower.toAlgHom_apply, one_mul]
lemma

affinePullbackOverlapIso_diagonal

L263 ↗
Algebra.Descent.affinePullbackOverlapIso_diagonal
Documentation

The ordinary geometric diagonal equality gives the literal tensor diagonal equality used by affine algebra descent.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable (β : pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
    (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≅
  pullback (Spec.map (CommRingCat.ofHom (algebraMap R C)))
    (Spec.map (CommRingCat.ofHom (algebraMap R B))))
Lean source · full declaration
lemma affinePullbackOverlapIso_diagonal
    (hdiag :
      pullback.lift (f := Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (g := Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (Spec.map (CommRingCat.ofHom (algebraMap B C))) (𝟙 _) (by
          rw [Category.id_comp, specMap_tower R B C]) ≫ β.hom =
      pullback.lift (f := Spec.map (CommRingCat.ofHom (algebraMap R C)))
        (g := Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (𝟙 _) (Spec.map (CommRingCat.ofHom (algebraMap B C))) (by
          rw [Category.id_comp, specMap_tower R B C])) :
    Spec.map (CommRingCat.ofHom (tensorTargetDiagonal R B C).toRingHom) ≫
        (affinePullbackOverlapIso R B C β).hom =
      Spec.map (CommRingCat.ofHom (tensorSourceDiagonal R B C).toRingHom) := by
  apply (cancel_mono (pullbackSpecIso R C B).inv).mp
  simp only [affinePullbackOverlapIso, Iso.trans_hom, Iso.symm_hom, Category.assoc,
    Iso.hom_inv_id, Category.comp_id]
  rw [← Category.assoc, affineTargetDiagonal_chart, affineSourceDiagonal_chart]
  exact hdiag

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