DiagramLifting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.DiagramLifting.finite_roof line 13

Source documentation

Finitely many localized arrows admit one common source denominator.

theorem finite_roof (n : ℕ) (X : C) (Y : Fin n → C)
    (f : ∀ i, L.obj X ⟶ L.obj (Y i)) :
    ∃ (Z : C) (u : Z ⟶ X), W u ∧
      ∃ (g : ∀ i, Z ⟶ Y i), ∀ i, L.map u ≫ f i = L.map (g i) := by
…

theorem OAI.LittleFinitistic.DiagramLifting.finite_zero_refinement line 33

Source documentation

A finite family vanishing after localization is annihilated by one source denominator.

theorem finite_zero_refinement (n : ℕ) (X : C) (Y : Fin n → C)
    (f : ∀ i, X ⟶ Y i) (hf : ∀ i, L.map (f i) = 0) :
    ∃ (Z : C) (u : Z ⟶ X), W u ∧ ∀ i, u ≫ f i = 0 := by
…

theorem OAI.LittleFinitistic.DiagramLifting.quadratic_diagram_lift line 59

Source documentation

A finite three-vertex diagram with arbitrary homogeneous quadratic relations lifts along a right-fraction localization. The displayed denominator maps give an isomorphism from the localized lift to the original entire diagram.

theorem quadratic_diagram_lift (na nb nr : ℕ) (X₀ X₁ X₂ : C)
    (a : Fin na → (L.obj X₀ ⟶ L.obj X₁))
    (b : Fin nb → (L.obj X₁ ⟶ L.obj X₂))
    (r : Fin nr → Fin na → Fin nb → k)
    (hr : ∀ ρ, ∑ i, ∑ j, r ρ i j • (a i ≫ b j) = 0) :
    ∃ (D₀ D₁ : C) (u₀ : D₀ ⟶ X₀) (u₁ : D₁ ⟶ X₁), W u₀ ∧ W u₁ ∧
    ∃ (f : Fin na → (D₀ ⟶ D₁)) (g : Fin nb → (D₁ ⟶ X₂)),
      (∀ i, L.map u₀ ≫ a i = L.map (f i) ≫ L.map u₁) ∧
      (∀ j, L.map u₁ ≫ b j = L.map (g j)) ∧
      (∀ ρ, ∑ i, ∑ j, r ρ i j • (f i ≫ g j) = 0) := by
…

theorem OAI.LittleFinitistic.DiagramLifting.finite_quadratic_diagram_lifting line 100

Source documentation

Every finite three-level quadratic diagram in the localized category, including objects not literally presented as functor images, has an isomorphic lift.

theorem finite_quadratic_diagram_lifting (na nb nr : ℕ) (Y₀ Y₁ Y₂ : D)
    (a : Fin na → (Y₀ ⟶ Y₁)) (b : Fin nb → (Y₁ ⟶ Y₂))
    (r : Fin nr → Fin na → Fin nb → k)
    (hr : ∀ ρ, ∑ i, ∑ j, r ρ i j • (a i ≫ b j) = 0) :
    ∃ (X₀ X₁ X₂ : C) (e₀ : L.obj X₀ ≅ Y₀) (e₁ : L.obj X₁ ≅ Y₁)
      (e₂ : L.obj X₂ ≅ Y₂) (f : Fin na → (X₀ ⟶ X₁)) (g : Fin nb → (X₁ ⟶ X₂)),
      (∀ i, L.map (f i) ≫ e₁.hom = e₀.hom ≫ a i) ∧
      (∀ j, L.map (g j) ≫ e₂.hom = e₁.hom ≫ b j) ∧
      (∀ ρ, ∑ i, ∑ j, r ρ i j • (f i ≫ g j) = 0) := by
…