Complex tori: varying lattices and logarithmic transforms

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe integral connecting class#

For the short exact sequence 0 → Λ → E → T → 0 of cyclic representations, let t be killed by the norm ∑ j < m, AT^j, lift it to s : E, and write the norm ∑ j < m, AE^j s as the image of a fixed point v of AΛ. Then the connecting homomorphism sends the degree-1 class of t to the degree-2 class of v.

TauCeti.δ_cyclicRepShortComplex_groupCohomologyπOdd_one {Λ E T : Type} [AddCommGroup Λ]
  [AddCommGroup E] [AddCommGroup T] {m : ℕ} [NeZero m] {AΛ : Λ ≃+ Λ} {AE : E ≃+ E} {AT : T ≃+ T}
  {i : Λ →+ E} {p : E →+ T} {hΛ : (⇑AΛ)^[m] = id} {hE : (⇑AE)^[m] = id} {hT : (⇑AT)^[m] = id}
  {hi : ∀ (x : Λ), i (AΛ x) = AE (i x)} {hp : ∀ (x : E), p (AE x) = AT (p x)}
  {hpi : ∀ (x : Λ), p (i x) = 0} (hS : (i.cyclicRepShortComplex p hΛ hE hT hi hp hpi).ShortExact)
  (t : ↥(Rep.Hom.hom (AT.cyclicRep hT).norm.asHom).ker) (s : E) (hs : p s = ↑t)
  (v :
    ↥(Rep.Hom.hom
          ((AΛ.cyclicRep hΛ).applyAsHom (Multiplicative.ofAdd 1) -
            CategoryTheory.CategoryStruct.id (AΛ.cyclicRep hΛ))).ker)
  (hv : i ↑v = ∑ j ∈ Finset.range m, (⇑AE)^[j] s) :
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hS 1 2 ⋯))
      ((CategoryTheory.ConcreteCategory.hom
          (Rep.FiniteCyclicGroup.groupCohomologyπOdd (AT.cyclicRep hT) (Multiplicative.ofAdd 1) ⋯ 1
            ⋯))
        t) =
    (CategoryTheory.ConcreteCategory.hom
        (Rep.FiniteCyclicGroup.groupCohomologyπEven (AΛ.cyclicRep hΛ) (Multiplicative.ofAdd 1) ⋯ 2
          ⋯))
      v

Lean

Formalized in Tau Ceti as TauCeti.δ_cyclicRepShortComplex_groupCohomologyπOdd_one.

Sources

• Tau Ceti documentation: TauCeti.δ_cyclicRepShortComplex_groupCohomologyπOdd_one
• Source of TauCeti.δ_cyclicRepShortComplex_groupCohomologyπOdd_one in TauCeti/RepresentationTheory/Homological/GroupCohomology/CyclicAutomorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.δ_cyclicRepShortComplex_groupCohomologyπOdd_one

Uses 1

Statement usesAddEquiv.cyclicRep

DefinitionThe connecting isomorphism H¹(C_m, T) ≃ H²(C_m, Λ)#

When multiplication by m is bijective on E, for instance when E is a real vector space, the cohomology of E vanishes in positive degrees and the connecting homomorphism of 0 → Λ → E → T → 0 is an isomorphism.

TauCeti.cyclicConnectingEquiv {Λ E T : Type} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup T]
  {m : ℕ} [NeZero m] {AΛ : Λ ≃+ Λ} {AE : E ≃+ E} {AT : T ≃+ T} {i : Λ →+ E} {p : E →+ T}
  {hΛ : (⇑AΛ)^[m] = id} {hE : (⇑AE)^[m] = id} {hT : (⇑AT)^[m] = id}
  {hi : ∀ (x : Λ), i (AΛ x) = AE (i x)} {hp : ∀ (x : E), p (AE x) = AT (p x)}
  {hpi : ∀ (x : Λ), p (i x) = 0} (hS : (i.cyclicRepShortComplex p hΛ hE hT hi hp hpi).ShortExact)
  (hm : Function.Bijective fun x => m • x) :
  ↑(groupCohomology (AT.cyclicRep hT) 1) ≃ₗ[ℤ] ↑(groupCohomology (AΛ.cyclicRep hΛ) 2)

Lean

Formalized in Tau Ceti as TauCeti.cyclicConnectingEquiv.

Sources

• Tau Ceti documentation: TauCeti.cyclicConnectingEquiv
• Source of TauCeti.cyclicConnectingEquiv in TauCeti/RepresentationTheory/Homological/GroupCohomology/CyclicAutomorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.cyclicConnectingEquiv

Uses 3

Statement usesAddEquiv.cyclicRep

Proof usesCorestriction through Shapiro's lemma · Restriction through Shapiro's lemma

TheoremNaturality under homomorphisms of cyclic groups#

Suppose χ : C_l → C_m sends the selected generator to its d-th power. Maps of exact sequences intertwining the d-th iterates of the source automorphisms with the target automorphisms commute with the connecting homomorphisms. This includes restriction, inflation, and coefficient maps.

TauCeti.map_δ_cyclicRepShortComplex {Λ E T : Type} [AddCommGroup Λ] [AddCommGroup E]
  [AddCommGroup T] {m : ℕ} [NeZero m] {AΛ : Λ ≃+ Λ} {AE : E ≃+ E} {AT : T ≃+ T} {i : Λ →+ E}
  {p : E →+ T} {hΛ : (⇑AΛ)^[m] = id} {hE : (⇑AE)^[m] = id} {hT : (⇑AT)^[m] = id}
  {hi : ∀ (x : Λ), i (AΛ x) = AE (i x)} {hp : ∀ (x : E), p (AE x) = AT (p x)}
  {hpi : ∀ (x : Λ), p (i x) = 0} (hS : (i.cyclicRepShortComplex p hΛ hE hT hi hp hpi).ShortExact)
  {l : ℕ} [NeZero l] {Λ' E' T' : Type} [AddCommGroup Λ'] [AddCommGroup E'] [AddCommGroup T']
  {AΛ' : Λ' ≃+ Λ'} {AE' : E' ≃+ E'} {AT' : T' ≃+ T'} {i' : Λ' →+ E'} {p' : E' →+ T'}
  {hΛ' : (⇑AΛ')^[l] = id} {hE' : (⇑AE')^[l] = id} {hT' : (⇑AT')^[l] = id}
  {hi' : ∀ (x : Λ'), i' (AΛ' x) = AE' (i' x)} {hp' : ∀ (x : E'), p' (AE' x) = AT' (p' x)}
  {hpi' : ∀ (x : Λ'), p' (i' x) = 0}
  (hS' : (i'.cyclicRepShortComplex p' hΛ' hE' hT' hi' hp' hpi').ShortExact)
  (χ : Multiplicative (ZMod l) →* Multiplicative (ZMod m)) (d : ℕ)
  (hχ : χ (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1 ^ d) (fΛ : Λ →+ Λ') (fE : E →+ E')
  (fT : T →+ T') (hfΛ : ∀ (x : Λ), fΛ ((⇑AΛ)^[d] x) = AΛ' (fΛ x))
  (hfE : ∀ (x : E), fE ((⇑AE)^[d] x) = AE' (fE x)) (hfT : ∀ (x : T), fT ((⇑AT)^[d] x) = AT' (fT x))
  (hfi : ∀ (x : Λ), fE (i x) = i' (fΛ x)) (hfp : ∀ (x : E), fT (p x) = p' (fE x)) (n q : ℕ)
  (hnq : n + 1 = q) (x : ↑(groupCohomology (AT.cyclicRep hT) n)) :
  (CategoryTheory.ConcreteCategory.hom
        (groupCohomology.map χ (fΛ.cyclicRepResHom hΛ hΛ' χ d hχ hfΛ) q))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hS n q hnq)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hS' n q hnq))
      ((CategoryTheory.ConcreteCategory.hom
          (groupCohomology.map χ (fT.cyclicRepResHom hT hT' χ d hχ hfT) n))
        x)

Lean

Formalized in Tau Ceti as TauCeti.map_δ_cyclicRepShortComplex.

Sources

• Tau Ceti documentation: TauCeti.map_δ_cyclicRepShortComplex
• Source of TauCeti.map_δ_cyclicRepShortComplex in TauCeti/RepresentationTheory/Homological/GroupCohomology/CyclicAutomorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.map_δ_cyclicRepShortComplex

Uses 1

Statement usesAddEquiv.cyclicRep

TheoremOdd-degree classes of the cyclic representation#

Two norm-zero elements x and y have the same class in odd degree exactly when y = x + (b - A b) for some b : T.

AddEquiv.groupCohomologyπOdd_cyclicRep_eq_iff {T : Type} [AddCommGroup T] {m : ℕ} [NeZero m]
  (A : T ≃+ T) (hA : (⇑A)^[m] = id) (i : ℕ) (hi : Odd i)
  (x y : ↥(Rep.Hom.hom (A.cyclicRep hA).norm.asHom).ker) :
  (CategoryTheory.ConcreteCategory.hom
          (Rep.FiniteCyclicGroup.groupCohomologyπOdd (A.cyclicRep hA) (Multiplicative.ofAdd 1) ⋯ i
            hi))
        x =
      (CategoryTheory.ConcreteCategory.hom
          (Rep.FiniteCyclicGroup.groupCohomologyπOdd (A.cyclicRep hA) (Multiplicative.ofAdd 1) ⋯ i
            hi))
        y ↔
    ∃ b, ↑y = ↑x + (b - A b)

Lean

Formalized in Tau Ceti as AddEquiv.groupCohomologyπOdd_cyclicRep_eq_iff.

Sources

• Tau Ceti documentation: AddEquiv.groupCohomologyπOdd_cyclicRep_eq_iff
• Source of AddEquiv.groupCohomologyπOdd_cyclicRep_eq_iff in TauCeti/RepresentationTheory/Homological/GroupCohomology/CyclicAutomorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanAddEquiv.groupCohomologyπOdd_cyclicRep_eq_iff

Uses 1

Statement usesAddEquiv.cyclicRep

DefinitionOdd-degree cohomology of the trivial action#

When C_m acts trivially on T, its cohomology in odd degree is the m-torsion T[m]: the class of a norm-zero element x corresponds to x itself.

TauCeti.groupCohomologyOddEquivTorsionBy (T : Type) [AddCommGroup T] (m : ℕ) [NeZero m] (i : ℕ)
  (hi : Odd i) :
  ↑(groupCohomology ((AddEquiv.refl T).cyclicRep ⋯) i) ≃ₗ[ℤ] ↥(Submodule.torsionBy ℤ T ↑m)

Lean

Formalized in Tau Ceti as TauCeti.groupCohomologyOddEquivTorsionBy.

Sources

• Tau Ceti documentation: TauCeti.groupCohomologyOddEquivTorsionBy
• Source of TauCeti.groupCohomologyOddEquivTorsionBy in TauCeti/RepresentationTheory/Homological/GroupCohomology/CyclicAutomorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.groupCohomologyOddEquivTorsionBy

Uses 1

Statement usesAddEquiv.cyclicRep

TheoremUniform bound for inverse period maps#

For a basis b of Λ, the real linear maps x ↦ ∑ i, x i • P y (b i) are bounded below by one constant c > 0 as y ranges over a compact set: c * ‖x‖ ≤ ‖∑ i, x i • P y (b i)‖.

TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact.{u_1, u_2, u_3, u_4} {Y : Type u_1}
  [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E]
  [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {K : Set Y}
  {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℤ Λ)
  (hcont : ∀ (l : Λ), Continuous fun y => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y))
  (hK : IsCompact K) : ∃ c > 0, ∀ y ∈ K, ∀ (x : ι → ℝ), c * ‖x‖ ≤ ‖∑ i, x i • (P y) (b i)‖

Lean

Formalized in Tau Ceti as TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact.

Sources

• Tau Ceti documentation: TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact
• Source of TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact in TauCeti/Algebra/Module/ZLattice/Family/Basic.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact

Uses 1

Proof usesTauCeti.periodBasis

DefinitionThe global trivialization of a continuous family of full lattices#

For a ℤ-basis b of Λ indexed by ι, the map [y, v] ↦ (y, [F_y⁻¹ v]), with F_y⁻¹ the coordinate map of the period basis at y, is a homeomorphism from the orbit space of the period translation action to the product of Y with the fixed torus ℝ^ι/ℤ^ι. It lies over Y (TauCeti.fst_torusFamilyHomeomorphProd), and on each fibre it is induced by the real linear isomorphism F_y⁻¹.

TauCeti.torusFamilyHomeomorphProd.{u_1, u_2, u_3, u_4} {Y : Type u_1} {Λ : Type u_2}
  [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  (P : Y → Λ →ₗ[ℤ] E) [∀ (y : Y), DiscreteTopology ↥(P y).range]
  [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} [Finite ι] (b : Module.Basis ι ℤ Λ)
  (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) [TopologicalSpace Y]
  (hcont : ∀ (l : Λ), Continuous fun y => (P y) l) :
  AddAction.orbitRel.Quotient Λ (Y × E) ≃ₜ
    Y × (ι → ℝ) ⧸ Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

Lean

Formalized in Tau Ceti as TauCeti.torusFamilyHomeomorphProd.

Sources

• Tau Ceti documentation: TauCeti.torusFamilyHomeomorphProd
• Source of TauCeti.torusFamilyHomeomorphProd in TauCeti/Algebra/Module/ZLattice/Family/HomeomorphProd.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.torusFamilyHomeomorphProd

Uses 1

Statement usesTauCeti.periodBasis

AbbreviationAddEquiv.cyclicRep#

The cyclic representation of A as an object of Rep ℤ C_m.

AddEquiv.cyclicRep.{u_1} {T : Type u_1} [AddCommGroup T] {m : ℕ} [NeZero m] (A : T ≃+ T)
  (hA : (⇑A)^[m] = id) : Rep.{u_1, 0, 0} ℤ (Multiplicative (ZMod m))

Lean

Formalized in Tau Ceti as AddEquiv.cyclicRep.

Sources

• Tau Ceti documentation: AddEquiv.cyclicRep
• Source of AddEquiv.cyclicRep in TauCeti/RepresentationTheory/Cyclic/Automorphism.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanAddEquiv.cyclicRep

Used by 5

Used byNaturality under homomorphisms of cyclic groups · Odd-degree classes of the cyclic representation · Odd-degree cohomology of the trivial action · The connecting isomorphism H¹(C_m, T) ≃ H²(C_m, Λ) · The integral connecting class

DefinitionTauCeti.torusFamilyProjection#

The projection (Y × E)/Λ → Y of the family of tori to its parameter space, descended from Prod.fst along the period translation action.

TauCeti.torusFamilyProjection.{u_4, u_5, u_6} {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ]
  {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) : AddAction.orbitRel.Quotient Λ (Y × E) → Y

Lean

Formalized in Tau Ceti as TauCeti.torusFamilyProjection.

Sources

• Tau Ceti documentation: TauCeti.torusFamilyProjection
• Source of TauCeti.torusFamilyProjection in TauCeti/Algebra/Module/ZLattice/Family/Basic.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.torusFamilyProjection

Used by 1

Used byTauCeti.torusFamilyFiberHomeomorph

DefinitionTauCeti.torusFamilyFiberHomeomorph#

The canonical identification of the translation quotient at y with the literal fibre of the total period quotient. It sends [v] to [y, v] and needs no lattice basis.

TauCeti.torusFamilyFiberHomeomorph.{u_1, u_2, u_3} {Y : Type u_1} {Λ : Type u_2} {E : Type u_3}
  [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y]
  [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun y => (P y) l) :
  AddAction.orbitRel.Quotient (↥(P y).range) E ≃ₜ ↑{z | TauCeti.torusFamilyProjection P z = y}

Lean

Formalized in Tau Ceti as TauCeti.torusFamilyFiberHomeomorph.

Sources

• Tau Ceti documentation: TauCeti.torusFamilyFiberHomeomorph
• Source of TauCeti.torusFamilyFiberHomeomorph in TauCeti/Algebra/Module/ZLattice/Family/Fiber.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.torusFamilyFiberHomeomorph

Uses 1

Statement usesTauCeti.torusFamilyProjection

DefinitionTauCeti.periodBasis#

The period basis at y: the periods P y (b i) of a ℤ-basis b of Λ, viewed as a real basis of E. They form a ℤ-basis of the full lattice LinearMap.range (P y), hence a real basis of E. Its inverse coordinate map x ↦ ∑ i, x i • P y (b i) is the real linear isomorphism ℝ^ι ≃ E carrying the standard lattice ℤ^ι onto the periods at y.

TauCeti.periodBasis.{u_1, u_2, u_3, u_4} {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ]
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E)
  [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range]
  [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} (b : Module.Basis ι ℤ Λ)
  (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) : Module.Basis ι ℝ E

Lean

Formalized in Tau Ceti as TauCeti.periodBasis.

Sources

• Tau Ceti documentation: TauCeti.periodBasis
• Source of TauCeti.periodBasis in TauCeti/Algebra/Module/ZLattice/Family/Basic.lean
• Tau Ceti roadmap status: Complex tori: varying lattices and logarithmic transforms

LeanTauCeti.periodBasis

Used by 2

Used byThe global trivialization of a continuous family of full lattices · Uniform bound for inverse period maps

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.