LocalTrivialization.lean

abbrev toEtaleObject (Y : X.Etale) (V : Y.left.Etale) :
    (etalePostcompose Y.hom).obj V ⟶ Y

def restrictedLift (Y : X.Etale)
    (e : {b : S.X₂.obj.obj (op Y) // S.g.hom.app (op Y) b = t.app (op Y) PUnit.unit})
    (V : Y.left.Etaleᵒᵖ) :
    {b : S.X₂.obj.obj ((etalePostcompose Y.hom).op.obj V) //
      S.g.hom.app _ b = t.app _ PUnit.unit}

lemma restrictedLift_naturality (Y : X.Etale)
    (e : {b : S.X₂.obj.obj (op Y) // S.g.hom.app (op Y) b = t.app (op Y) PUnit.unit})
    {V W : Y.left.Etaleᵒᵖ} (k : V ⟶ W) :
    S.X₂.obj.map ((etalePostcompose Y.hom).op.map k) (restrictedLift S t Y e V).val =
      (restrictedLift S t Y e W).val

def translationHom (Y : X.Etale)
    (e : {b : S.X₂.obj.obj (op Y) // S.g.hom.app (op Y) b = t.app (op Y) PUnit.unit}) :
    (etaleRestriction Y.hom (Type u)).obj
        ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₁) ⟶
      (etaleRestriction Y.hom (Type u)).obj (extensionFiber S t) where
  hom :=
    { app V := ↾fun a =>
        (⟨S.f.hom.app _ a + (restrictedLift S t Y e V).val, by
          change S.g.hom.app _ (S.f.hom.app _ a + (restrictedLift S t Y e V).val) =
            t.app _ PUnit.unit
          rw [map_add]
          have hz := ConcreteCategory.congr_hom
            (congrArg (fun k : S.X₁ ⟶ S.X₃ => k.hom.app
              ((etalePostcompose Y.hom).op.obj V)) S.zero) a
          change S.g.hom.app _ (S.f.hom.app _ a) = 0 at hz
          rw [hz, zero_add]
          exact (restrictedLift S t Y e V).property⟩)
      naturality V W k := by
        apply ConcreteCategory.hom_ext
        intro a
        apply Subtype.ext
        change S.f.hom.app _ (S.X₁.obj.map _ a) + (restrictedLift S t Y e W).val =
          S.X₂.obj.map _ (S.f.hom.app _ a + (restrictedLift S t Y e V).val)
        rw [map_add, restrictedLift_naturality]
        exact congrArg (fun b => b + (restrictedLift S t Y e W).val)
          (ConcreteCategory.congr_hom
            (S.f.hom.naturality ((etalePostcompose Y.hom).op.map k)) a) }

def extensionFiberRestrictionIso (hS : S.ShortExact) (Y : X.Etale)
    (e : {b : S.X₂.obj.obj (op Y) // S.g.hom.app (op Y) b = t.app (op Y) PUnit.unit}) :
    (etaleRestriction Y.hom (Type u)).obj
        ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₁) ≅
      (etaleRestriction Y.hom (Type u)).obj (extensionFiber S t)

theorem extensionFiber_exists_lift_cover (hS : S.ShortExact) :
    ∃ 𝒰 : X.Cover.{u} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale)),
      ∀ a : 𝒰.I₀, ∃ e : S.X₂.obj.obj
        (op (MorphismProperty.Over.mk ⊤ (𝒰.f a) (𝒰.map_prop a))),
        S.g.hom.app _ e = t.app _ PUnit.unit := by
  classical
  let W := etaleBaseObject X
  have hlocal : ∀ x : X, ∃ (Y : X.Etale) (y : Y.left)
      (e : S.X₂.obj.obj (op Y)), Y.hom y = x ∧
        S.g.hom.app (op Y) e = t.app (op Y) PUnit.unit := by
    intro x
    obtain ⟨Y, g, y, hg, hy⟩ := exists_etale_neighborhood_in_sieve
      (Presheaf.imageSieve S.g.hom (t.app (op W) PUnit.unit))
      (extensionFiber_locally_nonempty S t hS (op W)) x
    obtain ⟨e, he⟩ := hg
    refine ⟨Y, y, e, ?_, ?_⟩
    · have hw : g.left ≫ W.hom = Y.hom := g.w
      exact (congrArg (fun k : Y.left ⟶ X => k y) hw).symm.trans hy
    · exact he.trans (ConcreteCategory.congr_hom (t.naturality g.op) PUnit.unit).symm
  choose Y y e hy he using hlocal
  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)
  exact ⟨𝒰, fun a => ⟨e a, he a⟩⟩

theorem extensionFiber_isFiniteLocallyConstant (hS : S.ShortExact)
    (hF : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₁)) :
    IsEtaleFiniteLocallyConstantSet (extensionFiber S t)

def constantAbelianUnderlyingIso (X : Scheme.{u}) :
    constantSheaf X.smallEtaleTopology AddCommGrpCat.{u} ⋙
        sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u}) ≅
      forget AddCommGrpCat.{u} ⋙ constantSheaf X.smallEtaleTopology (Type u)

theorem constantAbelian_isFiniteLocallyConstant (X : Scheme.{u})
    (A : AddCommGrpCat.{u}) [Finite A] :
    IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj A))