OAI/Algebra/Finitistic/Localization/PresentedQuotientAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.QuadraticEncoding.relationPolynomial line 13

   Source documentation

   The literal inhomogeneous relation polynomial.

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

2. def OAI.LittleFinitistic.QuadraticEncoding.presentationRelation line 17
3. abbrev OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra line 21

   Source documentation

   The algebra with exactly the displayed finite quadratic presentation.

   abbrev PresentedAlgebra := RingQuot (presentationRelation P)

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.presentationRelation

4. def OAI.LittleFinitistic.QuadraticEncoding.presentedGenerator line 22
5. theorem OAI.LittleFinitistic.QuadraticEncoding.presentedGenerator_satisfies line 25
6. def OAI.LittleFinitistic.QuadraticEncoding.presentationLift line 34

   Source documentation

   Descent through the actual presentation, with every relation checked.

   def presentationLift (x : Fin d → A) (hx : P.Satisfies x) : PresentedAlgebra P →ₐ[k] A :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra

7. theorem OAI.LittleFinitistic.QuadraticEncoding.presentationLift_generator line 40
8. def OAI.LittleFinitistic.QuadraticEncoding.quotientAction line 45

   Source documentation

   The manuscript's quotient action for its displayed presentation.

   def quotientAction : PresentedAlgebra P →ₐ[k] End (vertexQ P 0) :=
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.vertexQ

9. theorem OAI.LittleFinitistic.QuadraticEncoding.quotientAction_generator line 48
10. def OAI.LittleFinitistic.QuadraticEncoding.quotientActionOfPresentation line 53

    Source documentation

    Transport the action along a genuine presentation isomorphism for R.

    def quotientActionOfPresentation (e : PresentedAlgebra P ≃ₐ[k] A) :
        A →ₐ[k] End (vertexQ P 0) := (quotientAction P).comp e.symm.toAlgHom

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.PresentedAlgebra, OAI.LittleFinitistic.QuadraticEncoding.vertexQ, OAI.LittleFinitistic.QuadraticEncoding.quotientAction

11. theorem OAI.LittleFinitistic.QuadraticEncoding.quotientActionOfPresentation_generator line 56