OAI/Algebra/Finitistic/Localization/QuotientAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.QuotientAction.normalized line 17
2. lemma OAI.LittleFinitistic.QuotientAction.normalized_product_comp line 21
3. lemma OAI.LittleFinitistic.QuotientAction.normalized_comp line 28
4. theorem OAI.LittleFinitistic.QuotientAction.normalized_relations line 37

   Source documentation

   Normalizing the invertible arrows recovers the original quadratic equations.

   theorem normalized_relations (j : Fin t) :
       (∑ h, ∑ l, P.quadratic j h l • (normalized s a h * normalized s a l)) +
       (∑ h, P.linear j h • normalized s a h) + P.constant j • (1 : End X₀) = 0 := by
   …

   Mentions: OAI.LittleFinitistic.QuotientAction.normalized

5. def OAI.LittleFinitistic.QuotientAction.polynomial line 46

   Source documentation

   The degree-at-most-two defining polynomial with the displayed coefficients.

   def polynomial (j : Fin t) : FreeAlgebra k (Fin d) :=
   …

6. def OAI.LittleFinitistic.QuotientAction.freeAction line 50
7. lemma OAI.LittleFinitistic.QuotientAction.freeAction_polynomial line 54
8. def OAI.LittleFinitistic.QuotientAction.quotientAction line 59

   Source documentation

   The genuine quotient action theta, obtained by descending the free action.

   noncomputable def quotientAction :
       QuadraticPresentation.Original k (Fin d) (polynomial P) →ₐ[k] End X₀ :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticPresentation.Original, OAI.LittleFinitistic.QuotientAction.polynomial

9. theorem OAI.LittleFinitistic.QuotientAction.quotientAction_generator line 67
10. def OAI.LittleFinitistic.QuotientAction.presentedAction line 74

    Source documentation

    Transport the descended action through the actual presentation equivalence.

    noncomputable def presentedAction {R : Type*} [Ring R] [Algebra k R]
        (E : QuadraticPresentation.Original k (Fin d) (polynomial P) ≃ₐ[k] R) :
        R →ₐ[k] End X₀ := (quotientAction P s s' a b hc hr).comp E.symm.toAlgHom
    …

    Mentions: OAI.LittleFinitistic.QuadraticPresentation.Original, OAI.LittleFinitistic.QuotientAction.polynomial, OAI.LittleFinitistic.QuotientAction.quotientAction

11. theorem OAI.LittleFinitistic.QuotientAction.normalized_evaluation line 80

    Source documentation

    Evaluation of normalized generators, with the natural vertex identifications.

    theorem normalized_evaluation {D : Type*} [Category D] (F : C ⥤ D)
        {Y : D} (e₀ : F.obj X₀ ≅ Y) (e₁ : F.obj X₁ ≅ Y)
        (x : Fin d → (Y ⟶ Y))
        (hs : F.map s ≫ e₁.hom = e₀.hom)
        (ha : ∀ h, F.map (a h) ≫ e₁.hom = e₀.hom ≫ x h) (h : Fin d) :
        F.map (normalized s a h) ≫ e₀.hom = e₀.hom ≫ x h := by
    …

    Mentions: OAI.LittleFinitistic.QuotientAction.normalized