Displaying similar documents to “Existence of Gorenstein projective resolutions and Tate cohomology”

Finiteness aspects of Gorenstein homological dimensions

Samir Bouchiba (2013)

Colloquium Mathematicae

Similarity:

We present an alternative way of measuring the Gorenstein projective (resp., injective) dimension of modules via a new type of complete projective (resp., injective) resolutions. As an application, we easily recover well known theorems such as the Auslander-Bridger formula. Our approach allows us to relate the Gorenstein global dimension of a ring R to the cohomological invariants silp(R) and spli(R) introduced by Gedrich and Gruenberg by proving that leftG-gldim(R) = maxleftsilp(R),...

Homography in ℝℙ

Roland Coghetto (2016)

Formalized Mathematics

Similarity:

The real projective plane has been formalized in Isabelle/HOL by Timothy Makarios [13] and in Coq by Nicolas Magaud, Julien Narboux and Pascal Schreck [12]. Some definitions on the real projective spaces were introduced early in the Mizar Mathematical Library by Wojciech Leonczuk [9], Krzysztof Prazmowski [10] and by Wojciech Skaba [18]. In this article, we check with the Mizar system [4], some properties on the determinants and the Grassmann-Plücker relation in rank 3 [2], [1], [7],...

Pascal’s Theorem in Real Projective Plane

Roland Coghetto (2017)

Formalized Mathematics

Similarity:

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines. For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s...