Verifying the Lefschetz Conditions for crystalline cohomology

Question

For context, I am rather new to the whole business of abstract Weil cohomology theories and motives in general, so if I am not making sense somewhere, do let me know!

1. In many of the literature that I am consulting while trying to learn about Weil cohomology theories and motives, it is often said that these cohomology theories must, in particular, satisfy the Weak and Hard Leftschetz Conditions. However, The Stacks Project apparently does not impose this axiom upon Weil cohomology theories (see their Tag 0FHA). Am I misinterpreting The Stacks Project, or can the Lefschetz Conditions be deduced from the other Weil cohomology axioms ?
2. The other thing that I have come across is that the theory of crystalline cohomology is a Weil cohomology theory, but for some reason I can not find any source which confirms that the Lefschetz Conditions are satisfied here. Can anyone point me to such a source, or alternatively, does crystalline cohomology even satisfy the Lefschetz Conditions at all ? (I should note that I'm not yet too familiar with crystalline cohomology.)

Thank you!

Answer 1

The Hard Lefschetz theorem can certainly not be deduced formally from the axioms of a Weil cohomology theory given in the Stacks Project. The reason it is called "hard" Lefschetz is that it is a really hard theorem, and deeper than the other properties.

The situation is rather that the axiomatization of what it means to be a Weil cohomology theory is perhaps not completely standardized; it is sometimes sloppily used as a catch-all term for "a cohomology theory with cycle maps, duality, traces, and all of the usual things that go with such things". I believe that it is more standard to not include the hard and weak Lefschetz theorems as axioms for a Weil cohomology theory.

The Hard Lefschetz theorem holds in crystalline cohomology. This was first proven by Katz--Messing ("Some consequences of the Riemann hypothesis for varieties over finite fields"), who deduced it from the weak Lefschetz theorem in crystalline cohomology, the Hard Lefschetz in étale cohomology, and Deligne's proof of the Weil conjectures.