compatiblePreservingOfFlat — Mathlib

English

If G is representably flat, then CompatiblePreserving K G holds.

Русский

Если G является представимо плоским, тогда выполняется совместимое сохранение.

LaTeX

$$$\text{CompatiblePreserving } K G$$$

Lean4

theorem compatiblePreservingOfFlat {C : Type u₁} [Category.{v₁} C] {D : Type u₁} [Category.{v₁} D]
    (K : GrothendieckTopology D) (G : C ⥤ D) [RepresentablyFlat G] : CompatiblePreserving K G :=
  by
  constructor
  intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ e
  let c : Cone (cospan g₁ g₂ ⋙ G) :=
    (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj
      (PullbackCone.mk f₁ f₂ e)
        /-
            This can then be viewed as a cospan of structured arrows, and we may obtain an arbitrary cone
            over it since `StructuredArrow W u` is cofiltered.
            Then, it suffices to prove that it is compatible when restricted onto `u(c'.X.right)`.
            -/

  let c' := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre _ _ _)
  have eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom (by simp) := by simp [c]
  have eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom (by simp) := by simp [c]
  conv_lhs => rw [eq₁]
  conv_rhs => rw [eq₂]
  simp only [c, op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map]
  apply congr_arg
  injection c'.π.naturality WalkingCospan.Hom.inl with _ e₁
  injection c'.π.naturality WalkingCospan.Hom.inr with _ e₂
  exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)

Похожие утверждения