Documentation

TauCeti.Geometry.Hodge.Decomposition

The Hodge decomposition #

This file proves the equivalence, due to Deligne, between the two descriptions of a pure Hodge structure: an n-opposed bounded filtration on one side, and a (p,q)-decomposition on the other.

In the forward direction the Hodge components of a pure Hodge structure form an internal direct sum: every step of the decreasing Hodge filtration is recovered as the supremum of the components in that step, and the full family of components is independent.

In the backward direction a family of subspaces that decomposes the space, is exchanged by the conjugation in complementary bidegrees, and is bounded below is packaged as TauCeti.Hodge.IsHodgeDecomposition, and the filtration F^p = ⨆_{q ≥ p} H^q it generates is a pure Hodge structure whose components are the given family. The two constructions are mutually inverse, which is TauCeti.Hodge.HodgeStructureOn.decompositionEquiv.

The key local calculation uses two adjacent opposedness decompositions. The component H^{p,n-p} is complementary to the sum of the conjugate step below it and the filtration step above it. Consequently every other component lies in this explicit complement. Boundedness then turns the one-step identity F p = H^{p,n-p} ⊔ F (p + 1) into filtration recovery by descending induction.

This is the opposed-filtration description of the Hodge decomposition in Deligne, Théorie de Hodge II, §1.2.1, and Voisin, Hodge Theory and Complex Algebraic Geometry I, §6.

Main declarations #

source
theorem TauCeti.Hodge.HodgeStructureOn.F_eq_piece_sup_succ {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
hs.F p = hs.piece p ⊔ hs.F (p + 1)

A filtration step is the sum of its Hodge component and the next filtration step.

source
theorem TauCeti.Hodge.HodgeStructureOn.isCompl_piece_conjF_sup_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
IsCompl (hs.piece p) (hs.conjF (n + 1 - p) ⊔ hs.F (p + 1))

The p-th Hodge component is complementary to the sum of the adjacent conjugate and ordinary filtration steps. This complement contains every Hodge component of degree different from p.

source
theorem TauCeti.Hodge.HodgeStructureOn.piece_le_conjF_of_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} (hqp : q < p) :
hs.piece q ≤ hs.conjF (n + 1 - p)

Every Hodge component whose degree is smaller than p lies in the conjugate filtration step complementary to F p.

source
theorem TauCeti.Hodge.HodgeStructureOn.piece_le_F_succ_of_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} (hpq : p < q) :
hs.piece q ≤ hs.F (p + 1)

Every Hodge component whose degree is larger than p lies in the filtration step complementary to conjF (n - p).

source
theorem TauCeti.Hodge.HodgeStructureOn.piece_iSupIndep {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
iSupIndep hs.piece

The Hodge components of an opposed filtration are independent.

source
theorem TauCeti.Hodge.HodgeStructureOn.F_eq_iSup_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
hs.F p = ⨆ (q : ℤ), ⨆ (_ : p ≤ q), hs.piece q

Every Hodge filtration step is the supremum of the Hodge components in at least that degree: F p = ⨆ q ≥ p, H^{q,n-q}.

source
theorem TauCeti.Hodge.HodgeStructureOn.conjF_eq_iSup_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
hs.conjF p = ⨆ (q : ℤ), ⨆ (_ : q ≤ n - p), hs.piece q

Every conjugate Hodge filtration step is the supremum of the Hodge components in at most the complementary degree: conjF p = ⨆ q ≤ n - p, H^{q,n-q}.

source
theorem TauCeti.Hodge.HodgeStructureOn.iSup_piece_eq_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
⨆ (p : ℤ), hs.piece p = ⊤

The supremum of all Hodge components is the whole ambient complex vector space.

source
theorem TauCeti.Hodge.HodgeStructureOn.isInternal_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
DirectSum.IsInternal hs.piece

The Hodge decomposition. The Hodge components H^{p,n-p} form an internal direct sum of the ambient complex vector space.

source
noncomputable def TauCeti.Hodge.HodgeStructureOn.decomposition {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
W ≃ₗ[ℂ] DirectSum ℤ fun (p : ℤ) => ↥(hs.piece p)

The Hodge decomposition as a linear equivalence: the ambient complex vector space is the direct sum of its Hodge components.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.HodgeStructureOn.decomposition_symm_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (x : DirectSum ℤ fun (p : ℤ) => ↥(hs.piece p)) :
    hs.decomposition.symm x = (DirectSum.coeLinearMap hs.piece) x

    The inverse of the Hodge decomposition sums up the Hodge components.

    source
    theorem TauCeti.Hodge.HodgeStructureOn.decomposition_apply_of_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p : ℤ} {x : W} (hx : x ∈ hs.piece p) :
    hs.decomposition x = (DirectSum.lof ℂ ℤ (fun (q : ℤ) => ↥(hs.piece q)) p) ⟨x, hx⟩

    A vector lying in a single Hodge component decomposes as that one component.

    source
    theorem TauCeti.Hodge.HodgeStructureOn.piece_induction_on {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {motive : W → Prop} (x : W) (mem : ∀ (p : ℤ), ∀ y ∈ hs.piece p, motive y) (add : ∀ (y z : W), motive y → motive z → motive (y + z)) :
    motive x

    Induction along the Hodge decomposition: a property that is stable under addition and holds on every Hodge component holds everywhere.

    source
    theorem TauCeti.Hodge.HodgeStructureOn.addHom_ext_of_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {F : Type u_1} {N : Type u_2} [AddZero N] [FunLike F W N] [AddMonoidHomClass F W N] (hs : HodgeStructureOn W ω n) {f g : F} (h : ∀ (p : ℤ), ∀ x ∈ hs.piece p, f x = g x) :
    f = g

    Two additive maps out of the ambient space that agree on every Hodge component are equal. This applies to any additive homomorphism class, including linear and semilinear maps.

    The Hodge projections #

    source
    noncomputable def TauCeti.Hodge.HodgeStructureOn.proj {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
    W →ₗ[ℂ] W

    The projection of the ambient complex vector space onto the Hodge component H^{p, n-p} along the Hodge decomposition.

    Instances For
      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (x : W) :
      (hs.proj p) x = ↑((hs.decomposition x) p)
      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (x : W) :
      (hs.proj p) x ∈ hs.piece p

      A Hodge projection lands in the corresponding Hodge component.

      source
      @[simp]
      theorem TauCeti.Hodge.HodgeStructureOn.proj_apply_of_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p : ℤ} {x : W} (hx : x ∈ hs.piece p) :
      (hs.proj p) x = x

      The Hodge projection of degree p fixes the Hodge component of degree p.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_apply_eq_zero_of_mem_of_ne {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} {x : W} (hx : x ∈ hs.piece q) (hqp : q ≠ p) :
      (hs.proj p) x = 0

      The Hodge projection of degree p annihilates every other Hodge component.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.sum_proj_eq {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {S : Finset ℤ} (x : W) (hS : ∀ p ∉ S, (hs.proj p) x = 0) :
      ∑ p ∈ S, (hs.proj p) x = x

      A vector is the sum of its Hodge projections over any finite set outside which its projections vanish. The other Hodge components need not be zero subspaces.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.eq_zero_of_proj_eq_zero {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {x : W} (h : ∀ (p : ℤ), (hs.proj p) x = 0) :
      x = 0

      A vector all of whose Hodge projections vanish is zero.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.mem_iSup_of_proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {S : ℤ → Submodule ℂ W} {x : W} (h : ∀ (p : ℤ), (hs.proj p) x ∈ S p) :
      x ∈ ⨆ (p : ℤ), S p

      A vector lies in a supremum of submodules as soon as each of its Hodge projections does.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_mem_of_le_iSup_inf {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {S : Submodule ℂ W} (hS : S ≤ ⨆ (p : ℤ), S ⊓ hs.piece p) {x : W} (hx : x ∈ S) (p : ℤ) :
      (hs.proj p) x ∈ S

      A submodule spanned by its intersections with the Hodge components contains the Hodge projections of each of its vectors.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.mem_of_proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {S : Submodule ℂ W} {x : W} (h : ∀ (p : ℤ), (hs.proj p) x ∈ S) :
      x ∈ S

      A vector lies in a submodule as soon as every one of its Hodge projections does.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.disjoint_piece_F_of_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} (hpq : p < q) :
      Disjoint (hs.piece p) (hs.F q)

      A Hodge component is disjoint from every strictly later filtration step.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.F_le_iSup_inf_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) :
      hs.F p ≤ ⨆ (q : ℤ), hs.F p ⊓ hs.piece q

      A filtration step is spanned by its intersections with the Hodge components.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_mem_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p : ℤ} {x : W} (hx : x ∈ hs.F p) (q : ℤ) :
      (hs.proj q) x ∈ hs.F p

      The Hodge projections of a vector of a filtration step stay in that step.

      source
      theorem TauCeti.Hodge.HodgeStructureOn.proj_eq_zero_of_mem_F_of_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} {x : W} (hx : x ∈ hs.F p) (hqp : q < p) :
      (hs.proj q) x = 0

      The Hodge projections of a vector of F p vanish in every degree below p.

      Reconstructing a Hodge structure from its decomposition #

      The Hodge decomposition above is more than a consequence of opposedness: the two descriptions of a pure Hodge structure carry the same information. The rest of this file runs the equivalence backwards, generating an opposed filtration from a family of components and identifying the two constructions in both directions.

      source
      structure TauCeti.Hodge.IsHodgeDecomposition {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (n : ℤ) (H : ℤ → Submodule ℂ W) :
      Prop

      A Hodge decomposition of weight n on a complex vector space with conjugation ω: a family H of subspaces that decomposes the space as an internal direct sum, is exchanged by the conjugation in complementary bidegrees, and vanishes in all sufficiently small degrees.

      This is the data on the other side of Deligne's equivalence. The Hodge components of a pure Hodge structure form such a family, by TauCeti.Hodge.HodgeStructureOn.isHodgeDecomposition_piece, and every such family arises this way from exactly one Hodge structure, by TauCeti.Hodge.HodgeStructureOn.decompositionEquiv.

      Instances For
        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.iSupIndep {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
        _root_.iSupIndep H

        The components of a Hodge decomposition are independent.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.iSup_eq_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
        ⨆ (p : ℤ), H p = ⊤

        The components of a Hodge decomposition span the ambient complex vector space.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.conj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) {p : ℤ} {x : W} (hx : x ∈ H p) :
        ω.toEquiv x ∈ H (n - p)

        Elementwise form of the exchange of the components of a Hodge decomposition by conjugation.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.exists_forall_gt_eq_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
        ∃ (b : ℤ), ∀ (p : ℤ), b < p → H p = ⊥

        A Hodge decomposition is bounded above as well: its components vanish in all sufficiently large degrees. This is the mirror image of boundedness below under the conjugation symmetry.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.finite_setOf_ne_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
        {p : ℤ | H p ≠ ⊥}.Finite

        Only finitely many components of a Hodge decomposition are nonzero.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.iSup_ge_eq_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) {a : ℤ} (ha : ∀ p < a, H p = ⊥) :
        ⨆ (q : ℤ), ⨆ (_ : a ≤ q), H q = ⊤

        Beyond a degree below which all components of a Hodge decomposition vanish, the tail sum ⨆_{q ≥ a} H^q is already the whole space.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.map_iSup_ge {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
        Submodule.map (↑ω.toEquiv) (⨆ (q : ℤ), ⨆ (_ : p ≤ q), H q) = ⨆ (q : ℤ), ⨆ (_ : q < n + 1 - p), H q

        Conjugation carries the tail sum ⨆_{q ≥ p} H^q of a Hodge decomposition onto the head sum ⨆_{q < n + 1 - p} H^q.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.disjoint_iSup_ge_iSup_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
        Disjoint (⨆ (q : ℤ), ⨆ (_ : p ≤ q), H q) (⨆ (q : ℤ), ⨆ (_ : q < p), H q)

        The tail sum ⨆_{q ≥ p} H^q and the head sum ⨆_{q < p} H^q of a Hodge decomposition are disjoint, because the components are independent.

        source
        theorem TauCeti.Hodge.IsHodgeDecomposition.isCompl_iSup_ge_iSup_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
        IsCompl (⨆ (q : ℤ), ⨆ (_ : p ≤ q), H q) (⨆ (q : ℤ), ⨆ (_ : q < p), H q)

        The tail sum ⨆_{q ≥ p} H^q and the head sum ⨆_{q < p} H^q of a Hodge decomposition are complementary: this is the opposedness of the filtration the decomposition generates.

        source
        noncomputable def TauCeti.Hodge.HodgeStructureOn.ofDecomposition {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
        HodgeStructureOn W ω n

        The pure Hodge structure of weight n generated by a Hodge decomposition: its filtration step F^p is the sum ⨆_{q ≥ p} H^q of the components of degree at least p.

        This is the converse half of Deligne's equivalence between n-opposed filtrations and (p,q)-decompositions, TauCeti.Hodge.HodgeStructureOn.isInternal_piece being the forward half.

        Instances For
          source
          @[simp]
          theorem TauCeti.Hodge.HodgeStructureOn.ofDecomposition_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
          (ofDecomposition h).F p = ⨆ (q : ℤ), ⨆ (_ : p ≤ q), H q

          The filtration generated by a Hodge decomposition is the sum of the components of degree at least the filtration index.

          source
          @[simp]
          theorem TauCeti.Hodge.HodgeStructureOn.ofDecomposition_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
          (ofDecomposition h).conjF p = ⨆ (q : ℤ), ⨆ (_ : q < n + 1 - p), H q

          The conjugate of the filtration generated by a Hodge decomposition is the sum of the components of degree below the complementary index.

          source
          @[simp]
          theorem TauCeti.Hodge.HodgeStructureOn.ofDecomposition_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) (p : ℤ) :
          (ofDecomposition h).piece p = H p

          The components are recovered. The Hodge components of the Hodge structure generated by a Hodge decomposition are the members of that decomposition.

          source
          theorem TauCeti.Hodge.HodgeStructureOn.ofDecomposition_isEffective_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {H : ℤ → Submodule ℂ W} (h : IsHodgeDecomposition ω n H) :
          (ofDecomposition h).IsEffective ↔ ∀ p < 0, H p = ⊥

          The Hodge structure generated by a Hodge decomposition is effective exactly when the decomposition has no components in negative degrees.

          source
          theorem TauCeti.Hodge.HodgeStructureOn.isHodgeDecomposition_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
          IsHodgeDecomposition ω n hs.piece

          The decomposition of a pure Hodge structure. The Hodge components of a pure Hodge structure of weight n form a Hodge decomposition of weight n.

          source
          @[simp]
          theorem TauCeti.Hodge.HodgeStructureOn.ofDecomposition_isHodgeDecomposition_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
          ofDecomposition ⋯ = hs

          The filtration is recovered. Regenerating a pure Hodge structure from its own Hodge components returns it unchanged.

          source
          theorem TauCeti.Hodge.HodgeStructureOn.isEffective_iff_piece_eq_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
          hs.IsEffective ↔ ∀ p < 0, hs.piece p = ⊥

          A pure Hodge structure is effective exactly when it has no Hodge components in negative degrees.

          source
          theorem TauCeti.Hodge.HodgeStructureOn.isEffective_iff_piece_ne_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
          hs.IsEffective ↔ ∀ (p : ℤ), hs.piece p ≠ ⊥ → p ∈ Set.Icc 0 n

          Effectivity is a support condition on the Hodge components. A pure Hodge structure of weight n is effective exactly when each of its nonzero Hodge components H^{p,n-p} has 0 ≤ p ≤ n.

          source
          theorem TauCeti.Hodge.HodgeStructureOn.piece_injective {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} :
          Function.Injective piece

          A pure Hodge structure is determined by its Hodge components.

          source
          noncomputable def TauCeti.Hodge.HodgeStructureOn.decompositionEquiv {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (n : ℤ) :
          HodgeStructureOn W ω n ≃ { H : ℤ → Submodule ℂ W // IsHodgeDecomposition ω n H }

          Deligne's equivalence. A pure Hodge structure of weight n on a complex vector space with conjugation is the same thing as a Hodge decomposition of weight n: the filtration is generated by the components as F^p = ⨆_{q ≥ p} H^q, and the components are cut out of the filtration as H^p = F^p ⊓ conj F^{n-p}.

          Instances For
            source
            @[simp]
            theorem TauCeti.Hodge.HodgeStructureOn.coe_decompositionEquiv_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) :
            ↑((decompositionEquiv ω n) hs) = hs.piece
            source
            @[simp]
            theorem TauCeti.Hodge.HodgeStructureOn.decompositionEquiv_symm_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (H' : { H : ℤ → Submodule ℂ W // IsHodgeDecomposition ω n H }) :
            (decompositionEquiv ω n).symm H' = ofDecomposition ⋯