NYLL
Module

IsDeformationClassMap_cechH1ToH1_germ_eq_of_two_covers.lean

Nyll.JacobianVarieties.Picard.IsDeformationClassMap_cechH1ToH1_germ_eq_of_two_covers
5 declarations indexed from sourceView source ↗

Module documentation

Independence of the affine cover for deformation classes

Imports21
Imported by2

Declarations

theorem

nonempty_inf

L86 ↗
JacobianVarieties.Picard.Proofs.DeformationCoverComparison.CoverGlue.nonempty_inf
Documentation

Two nonempty open subsets of an irreducible scheme intersect.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationCoverComparison
attribute [-instance]
  AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
  AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
  AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
  AlgebraicGeometry.IsProper.fiberToSpecResidueField SheafOfModules.isIso_ihomModelToIhom
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
universe u
open  CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace CoverGlue
Lean source · statement
theorem nonempty_inf {X : Scheme.{u}} [IrreducibleSpace X] (U V : X.Opens) [hU : Nonempty U]
    [hV : Nonempty V] :
    Nonempty (U ⊓ V : X.Opens)
theorem

nonempty_of_nonempty_inf_left

L93 ↗
JacobianVarieties.Picard.Proofs.DeformationCoverComparison.CoverGlue.nonempty_of_nonempty_inf_left
Documentation

A nonempty intersection implies the first open is nonempty.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationCoverComparison
attribute [-instance]
  AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
  AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
  AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
  AlgebraicGeometry.IsProper.fiberToSpecResidueField SheafOfModules.isIso_ihomModelToIhom
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
universe u
open  CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace CoverGlue
Lean source · statement
theorem nonempty_of_nonempty_inf_left {X : Scheme.{u}} (U V : X.Opens)
    [h : Nonempty (U ⊓ V : X.Opens)] :
    Nonempty U
theorem

nonempty_of_nonempty_inf_right

L100 ↗
JacobianVarieties.Picard.Proofs.DeformationCoverComparison.CoverGlue.nonempty_of_nonempty_inf_right
Documentation

A nonempty intersection implies the second open is nonempty.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationCoverComparison
attribute [-instance]
  AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
  AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
  AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
  AlgebraicGeometry.IsProper.fiberToSpecResidueField SheafOfModules.isIso_ihomModelToIhom
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
universe u
open  CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace CoverGlue
Lean source · statement
theorem nonempty_of_nonempty_inf_right {X : Scheme.{u}} (U V : X.Opens)
    [h : Nonempty (U ⊓ V : X.Opens)] :
    Nonempty V
theorem

germToFunctionField_map

L107 ↗
JacobianVarieties.Picard.Proofs.DeformationCoverComparison.CoverGlue.germToFunctionField_map
Documentation

Restriction preserves the germ of a section in the function field.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationCoverComparison
attribute [-instance]
  AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
  AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
  AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
  AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
  AlgebraicGeometry.IsProper.fiberToSpecResidueField SheafOfModules.isIso_ihomModelToIhom
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp]
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
universe u
open  CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace CoverGlue
Lean source · statement
theorem germToFunctionField_map {X : Scheme.{u}} [IrreducibleSpace X] {U V : X.Opens} [Nonempty U]
    [Nonempty V]
    (h : V ≤ U) (s : Γ(X, U)) :
    (X.germToFunctionField V).hom ((X.presheaf.map (homOfLE h).op).hom s)
      = (X.germToFunctionField U).hom s
theorem

cechH1ToH1_germ_eq_of_two_covers

L130 ↗
AlgebraicGeometry.RelPicard.IsDeformationClassMap.cechH1ToH1_germ_eq_of_two_covers
Documentation

The cohomology class of a deformation is independent of its two affine cover.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard.IsDeformationClassMap
open _root_.JacobianVarieties.Picard.Proofs.DeformationCoverComparison
universe u
open  _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
  _root_.AlgebraicGeometry.RelPicard
  _root_.NeronModelInfra _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.JacobianVarieties.Picard.Proofs.DeformationCoverComparison.CoverGlue in
Lean source · full declaration
theorem cechH1ToH1_germ_eq_of_two_covers
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙 (Spec
      (.of R))) c)
    (K : Type u) [Field K] [Algebra R K]
    [IsIntegral (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K))]
    [IsSeparated (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))]
    [SmoothOfRelativeDimension 1 (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))]
    (𝒲 𝒲' : C.TwoAffineOpenCover)
    {δ : RigKerDualNumber c ε K → H1StructureSheaf c K 𝒲}
    {δ' : RigKerDualNumber c ε K → H1StructureSheaf c K 𝒲'}
    (hδ : IsDeformationClassMap c ε K 𝒲 δ) (hδ' : IsDeformationClassMap c ε K 𝒲' δ')
    (x : RigKerDualNumber c ε K)
    (s : ((𝒲.pullback c K).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))).A01)
    (s' : ((𝒲'.pullback c K).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))).A01)
    (hs : δ x = Submodule.Quotient.mk s) (hs' : δ' x = Submodule.Quotient.mk s') :
    let X' : Scheme.{u} := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)
    let c' : X' ⟶ Spec (.of K) := pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)
    let : Algebra K X'.functionField := (AlgebraicCurve.baseToFunctionField c').toAlgebra
    let W : X'.TwoAffineOpenCover := 𝒲.pullback c K
    let W' : X'.TwoAffineOpenCover := 𝒲'.pullback c K
    ∀ [Nonempty (W.U0 ⊓ W.U1 : X'.Opens)] [Nonempty (W'.U0 ⊓ W'.U1 : X'.Opens)]
      (hW : AlgebraicCurve.placesOf c' W.U0 ∪ AlgebraicCurve.placesOf c' W.U1 = Set.univ)
      (hW' : AlgebraicCurve.placesOf c' W'.U0 ∪ AlgebraicCurve.placesOf c' W'.U1 = Set.univ)
      (hsr : (X'.germToFunctionField (W.U0 ⊓ W.U1)).hom s ∈
        AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf c' W.U0 ∩ AlgebraicCurve.placesOf c' W.U1)
          (0 : AlgebraicCurve.Divisor K X'.functionField))
      (hsr' : (X'.germToFunctionField (W'.U0 ⊓ W'.U1)).hom s' ∈
        AlgebraicCurve.lSpaceOn (AlgebraicCurve.placesOf c' W'.U0 ∩ AlgebraicCurve.placesOf c'
          W'.U1)
          (0 : AlgebraicCurve.Divisor K X'.functionField)),
      AlgebraicCurve.cechH1ToH1 hW 0
          (Submodule.Quotient.mk ⟨(X'.germToFunctionField (W.U0 ⊓ W.U1)).hom s, hsr⟩) =
        AlgebraicCurve.cechH1ToH1 hW' 0
          (Submodule.Quotient.mk ⟨(X'.germToFunctionField (W'.U0 ⊓ W'.U1)).hom s', hsr'⟩) := by
  intro X' c' algKFunctionField W W' hne hne' hW hW' hsr hsr'
  have : Nonempty ((𝒲.pullback c K).U0 : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).Opens) :=
    nonempty_of_nonempty_inf_left _ (𝒲.pullback c K).U1
  have : Nonempty ((𝒲.pullback c K).U1 : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).Opens) :=
    nonempty_of_nonempty_inf_right (𝒲.pullback c K).U0 _
  have : Nonempty ((𝒲'.pullback c K).U0 : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).Opens) :=
    nonempty_of_nonempty_inf_left _ (𝒲'.pullback c K).U1
  have : Nonempty ((𝒲'.pullback c K).U1 : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).Opens) :=
    nonempty_of_nonempty_inf_right (𝒲'.pullback c K).U0 _
  have : Nonempty ((𝒲.pullback c K).U0 ⊓ (𝒲'.pullback c K).U0 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty ((𝒲.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty ((𝒲.pullback c K).U1 ⊓ (𝒲'.pullback c K).U0 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty ((𝒲.pullback c K).U1 ⊓ (𝒲'.pullback c K).U1 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty (((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U0 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty (((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U1 :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty ((𝒲.pullback c K).U0 ⊓ ((𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1) :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  have : Nonempty ((𝒲.pullback c K).U1 ⊓ ((𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1) :
      (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K)).Opens) := nonempty_inf _ _
  obtain ⟨g00, g01, g10, g11, h1, h2, h3, -⟩ :=
    IsDeformationClassMap.exists_crossSections c ε K 𝒲 𝒲' hδ hδ' x s s' hs hs'
  have m00 := AlgebraicCurve.germToFunctionField_inf_mem_lSpaceOn_inter_placesOf
    (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) (𝒲.pullback c K).U0 (𝒲'.pullback c
      K).U0 g00
  have m01 := AlgebraicCurve.germToFunctionField_inf_mem_lSpaceOn_inter_placesOf
    (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) (𝒲.pullback c K).U0 (𝒲'.pullback c
      K).U1 g01
  have m10 := AlgebraicCurve.germToFunctionField_inf_mem_lSpaceOn_inter_placesOf
    (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) (𝒲.pullback c K).U1 (𝒲'.pullback c
      K).U0 g10
  have m11 := AlgebraicCurve.germToFunctionField_inf_mem_lSpaceOn_inter_placesOf
    (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K)) (𝒲.pullback c K).U1 (𝒲'.pullback c
      K).U1 g11
  have e1 := congrArg ((Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).germToFunctionField
    (((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U0)).hom h1
  have e2 := congrArg ((Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).germToFunctionField
    (((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U1)).hom h2
  have e3 := congrArg ((Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R
    K)).germToFunctionField
    ((𝒲.pullback c K).U0 ⊓ ((𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1))).hom h3
  simp only [map_add, germToFunctionField_map] at e1 e2 e3
  rw [germToFunctionField_map (X := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K))
    (U := (𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1)
    (V := ((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U0)
    (inf_le_left : ((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U0 ≤ (𝒲.pullback
      c K).U0 ⊓ (𝒲.pullback c K).U1)
    (s : Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K), (𝒲.pullback c K).U0 ⊓
      (𝒲.pullback c K).U1))] at e1
  rw [germToFunctionField_map (X := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K))
    (U := (𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1)
    (V := ((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U1)
    (inf_le_left : ((𝒲.pullback c K).U0 ⊓ (𝒲.pullback c K).U1) ⊓ (𝒲'.pullback c K).U1 ≤ (𝒲.pullback
      c K).U0 ⊓ (𝒲.pullback c K).U1)
    (s : Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K), (𝒲.pullback c K).U0 ⊓
      (𝒲.pullback c K).U1))] at e2
  rw [germToFunctionField_map (X := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K))
    (U := (𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1)
    (V := (𝒲.pullback c K).U0 ⊓ ((𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1))
    (inf_le_right : (𝒲.pullback c K).U0 ⊓ ((𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1) ≤
      (𝒲'.pullback c K).U0 ⊓ (𝒲'.pullback c K).U1)
    (s' : Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R K), (𝒲'.pullback c K).U0 ⊓
      (𝒲'.pullback c K).U1))] at e3
  exact AlgebraicCurve.cechH1ToH1_mk_eq_cechH1ToH1_mk_of_crossSections hW hW' ⟨_, hsr⟩ ⟨_, hsr'⟩ _
    _ _ _
    m00 m01 m10 m11 e1 e2 e3

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