ConstantMorphism.lean

lemma restriction_factor {M N : ModuleCat.{u} R}
    {F : X.Etaleᵒᵖ ⥤ ModuleCat.{u} R}
    (α : (Functor.const X.Etaleᵒᵖ).obj M ⟶ F)
    (η : (Functor.const X.Etaleᵒᵖ).obj N ⟶ F)
    (Y : X.Etale) (l : M ⟶ N) (hl : α.app (op Y) = l ≫ η.app (op Y)) :
    whiskerLeft (etalePostcompose Y.hom).op α =
      (Functor.const Y.left.Etaleᵒᵖ).map l ≫ whiskerLeft (etalePostcompose Y.hom).op η

lemma restriction_constantMorphism_square
    (M N : ModuleCat.{u} R)
    (φ : (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M ⟶
      (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj N)
    (Y : X.Etale) (l : M ⟶ N)
    (hl : (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj M) ≫ φ.hom).app
        (op Y) = l ≫
          (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj N)).app (op Y)) :
    etaleRestrictionConstantHom Y.hom R M ≫
        (etaleRestriction Y.hom (ModuleCat.{u} R)).map φ =
      (constantSheaf Y.left.smallEtaleTopology (ModuleCat.{u} R)).map l ≫
        etaleRestrictionConstantHom Y.hom R N

theorem exists_constantMorphism_cover
    (M N : ModuleCat.{u} R) [Module.Finite R M]
    (φ : (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M ⟶
      (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj N) :
    ∃ 𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)),
      ∀ i : 𝒰.I₀, ∃ (l : M ⟶ N)
        (eM : (etalePullback (𝒰.f i) R).obj
            ((constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M) ≅
          (constantSheaf (𝒰.X i).smallEtaleTopology (ModuleCat.{u} R)).obj M)
        (eN : (etalePullback (𝒰.f i) R).obj
            ((constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj N) ≅
          (constantSheaf (𝒰.X i).smallEtaleTopology (ModuleCat.{u} R)).obj N),
        (etalePullback (𝒰.f i) R).map φ ≫ eN.hom =
          eM.hom ≫ (constantSheaf (𝒰.X i).smallEtaleTopology (ModuleCat.{u} R)).map l := by
  classical
  choose Y y l hy hl using fun x : X => exists_constantPresentation_factor (X := X) M N
    (F := sheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj N))
    (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj M) ≫ φ.hom)
    (toSheafify X.smallEtaleTopology ((Functor.const X.Etaleᵒᵖ).obj N)) x
  let 𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)) :=
    Scheme.Cover.mkOfCovers X (fun x => (Y x).left) (fun x => (Y x).hom)
      (fun x => ⟨x, y x, hy x⟩) (fun x => (Y x).prop)
  refine ⟨𝒰, fun i => ?_⟩
  let eP := etalePullbackRestrictionIso (Y i).hom R
  let eM := eP.app _ ≪≫ (etaleRestrictionConstantIso (Y i).hom R M).symm
  let eN := eP.app _ ≪≫ (etaleRestrictionConstantIso (Y i).hom R N).symm
  refine ⟨l i, eM, eN, ?_⟩
  change (etalePullback (Y i).hom R).map φ ≫
      (eP.app _).hom ≫ (etaleRestrictionConstantIso (Y i).hom R N).inv =
    (eP.app _).hom ≫ (etaleRestrictionConstantIso (Y i).hom R M).inv ≫
      (constantSheaf (Y i).left.smallEtaleTopology (ModuleCat.{u} R)).map (l i)
  erw [← Category.assoc, eP.hom.naturality, Category.assoc]
  apply congrArg ((eP.app _).hom ≫ ·)
  apply (cancel_mono (etaleRestrictionConstantIso (Y i).hom R N).hom).mp
  simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
  erw [← restriction_constantMorphism_square M N φ (Y i) (l i) (hl i)]
  exact (Iso.inv_hom_id_assoc (etaleRestrictionConstantIso (Y i).hom R M) _).symm