map_final — Mathlib

English

Let the diagram commute up to isomorphism; the induced comma-map is final.

Русский

Диаграмма коммутирует до изоморфизма; индуцированная карта запятой финальная.

LaTeX

$$$\\\\operatorname{Final}(\\\\mathrm{Comma.map}(...))$$$

Lean4

/-- Let the following diagram commute up to isomorphism:

```
      L       R
  A  ---→ T  ←--- B
  |       |       |
  | F     | H     | G
  ↓       ↓       ↓
  A' ---→ T' ←--- B'
      L'      R'
```

Let `F`, `G`, `R` and `R'` be final and `B` be filtered. Then, the induced functor between the comma
categories of the first and second row of the diagram is final. -/
theorem map_final {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B] {T : Type u₃} [Category.{v₃} T]
    {L : A ⥤ T} {R : B ⥤ T} {A' : Type u₄} [Category.{v₄} A'] {B' : Type u₅} [Category.{v₅} B'] {T' : Type u₆}
    [Category.{v₆} T'] {L' : A' ⥤ T'} {R' : B' ⥤ T'} {F : A ⥤ A'} {G : B ⥤ B'} {H : T ⥤ T'} (iL : F ⋙ L' ≅ L ⋙ H)
    (iR : G ⋙ R' ≅ R ⋙ H) [IsFiltered B] [R.Final] [R'.Final] [F.Final] [G.Final] : (Comma.map iL.hom iR.inv).Final :=
  ⟨fun ⟨i₂, j₂, u₂⟩ => by
    haveI := final_of_natIso iR
    rw [isConnected_iff_of_equivalence (StructuredArrow.commaMapEquivalence iL.hom iR.inv _)]
    have :
      StructuredArrow.map₂ u₂ iR.hom ≅
        StructuredArrow.post j₂ G R' ⋙
          StructuredArrow.map₂ (G := 𝟭 _) (F := 𝟭 _) (R' := R ⋙ H) u₂ iR.hom ⋙ StructuredArrow.pre _ R H :=
      eqToIso
          (by
            congr
            · simp
            · ext; simp) ≪≫
        (StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
          isoWhiskerLeft _
              ((StructuredArrow.map₂CompMap₂Iso _ _ _ _).symm ≪≫
                isoWhiskerLeft _ (StructuredArrow.preIsoMap₂ _ _ _).symm) ≪≫
            isoWhiskerRight (StructuredArrow.postIsoMap₂ j₂ G R').symm _
    haveI := final_of_natIso this.symm
    rw [IsIso.Iso.inv_inv]
    infer_instance⟩

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