Naturality of the overlattice correspondence

The intermediate-carrier correspondence of TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Basic attaches to an integral lattice L the order isomorphism between carriers L ≤ P ≤ Lᵛ and subgroups of A_L = Lᵛ / L, and TauCeti.LinearAlgebra.IntegralLattice.Overlattice.Isotropic cuts out the integral and even carriers inside it. This file proves that the whole package is natural, in the two directions the theory uses it.

An isometry e : L ≃ M transports intermediate carriers along its ambient equivalence, and the resulting order isomorphism commutes with the discriminant-subgroup correspondence: the subgroup of A_M attached to e(P) is the image of the subgroup of A_L attached to P under the induced equivalence A_L ≃ A_M. Integrality and evenness of an intermediate carrier are invariants of the transport, so the two refined correspondences are natural as well. For nondegenerate lattices, orthogonal complements and isotropy transport directly through the generic finite-bilinear-module API applied to the induced discriminant bilinear isometry.

The ambient equivalence also restricts to an isometry between the lattice carried by an integral intermediate carrier and the lattice carried by its transport, which is what lets the discriminant constructions of the overlattices themselves be compared.

For an orthogonal direct sum, a pair of intermediate carriers assembles into the intermediate carrier P₁ ⊕ P₂ of L ⊥ M, order-embedding the pairs into the carriers of the sum. Its subgroup of A_(L ⊥ M) ≃ A_L × A_M is the product subgroup, and it is integral, respectively even, exactly when both components are.

Main declarations

• TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv: transport of intermediate carriers along a lattice isometry.
• TauCeti.IntegralLattice.Isometry.discriminantSubgroup_intermediateCarrierEquiv and IntegralLattice.Isometry.intermediateCarrierEquiv_intermediateCarrierOfDiscriminantSubgroup: the transport commutes with the discriminant-subgroup correspondence and with its inverse-image construction.
• Isometry.orthogonalComplement_discriminantSubgroup_intermediateCarrierEquiv: transport carries the orthogonal complements of corresponding discriminant subgroups to one another.
• TauCeti.IntegralLattice.Isometry.isIntegral_intermediateCarrierEquiv_iff and TauCeti.IntegralLattice.Isometry.isEven_intermediateCarrierEquiv_iff: integrality and evenness of an intermediate carrier are isometry invariants.
• TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv and TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv: the corresponding transports restricted to integral and even intermediate carriers.
• TauCeti.IntegralLattice.Isometry.toIntegralLatticeIsometry: the induced isometry between the integral lattices carried by an integral intermediate carrier and by its transport.
• TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier: the intermediate carrier of an orthogonal sum assembled from a pair of intermediate carriers.
• TauCeti.IntegralLattice.map_discriminantSubgroup_orthogonalSumIntermediateCarrier and IntegralLattice.orthogonalSumIntermediateCarrier_intermediateCarrierOfDiscriminantSubgroup: its subgroup of the discriminant group is the product subgroup, in both directions.
• TauCeti.IntegralLattice.isIntegral_orthogonalSumIntermediateCarrier_iff and TauCeti.IntegralLattice.isEven_orthogonalSumIntermediateCarrier_iff: integrality and evenness of an assembled carrier are componentwise.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 4.

Transport along a lattice isometry

def TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ↑L.IntermediateCarrier ≃o ↑M.IntermediateCarrier

An isometry transports intermediate carriers. The ambient equivalence of a lattice isometry maps the carrier onto the carrier and the dual carrier onto the dual carrier, so it restricts to an order isomorphism between the intervals of intermediate carriers.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_apply_coe {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) : ↑(e.intermediateCarrierEquiv P) = Submodule.map ↑e.ambientEquiv ↑P

The carrier transported along an isometry is the image of the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.mem_intermediateCarrierEquiv_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) (y : W) : y ∈ ↑(e.intermediateCarrierEquiv P) ↔ e.symm y ∈ ↑P

Membership in a transported carrier is membership of the preimage in the original carrier.

theorem TauCeti.IntegralLattice.Isometry.apply_mem_intermediateCarrierEquiv_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) (x : V) : e x ∈ ↑(e.intermediateCarrierEquiv P) ↔ x ∈ ↑P

The image of a vector lies in the transported carrier exactly when the vector lies in the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).intermediateCarrierEquiv = OrderIso.refl ↑L.IntermediateCarrier

The identity isometry transports every intermediate carrier to itself.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.intermediateCarrierEquiv = e.intermediateCarrierEquiv.symm

The transport along an inverse isometry is the inverse transport.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.mem_intermediateCarrierEquiv_symm_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (Q : ↑M.IntermediateCarrier) (x : V) : x ∈ ↑(e.intermediateCarrierEquiv.symm Q) ↔ e x ∈ ↑Q

Membership in an inversely transported carrier is membership of the image in the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).intermediateCarrierEquiv = e.intermediateCarrierEquiv.trans f.intermediateCarrierEquiv

The transport along a composite isometry is the composite transport.

Naturality of the discriminant-subgroup correspondence

theorem TauCeti.IntegralLattice.Isometry.mem_discriminantSubgroup_intermediateCarrierEquiv_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) (y : M.DiscriminantGroup) : y ∈ M.discriminantSubgroup (e.intermediateCarrierEquiv P) ↔ e.discriminantGroupEquiv.symm y ∈ L.discriminantSubgroup P

A discriminant class of the target lattice lies in the subgroup of a transported carrier exactly when its preimage lies in the subgroup of the original carrier.

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_mem_discriminantSubgroup_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) (x : L.DiscriminantGroup) : e.discriminantGroupEquiv x ∈ M.discriminantSubgroup (e.intermediateCarrierEquiv P) ↔ x ∈ L.discriminantSubgroup P

A discriminant class lies in the subgroup of a transported carrier exactly when its image under the induced discriminant equivalence lies in that subgroup.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.discriminantSubgroup_intermediateCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) : M.discriminantSubgroup (e.intermediateCarrierEquiv P) = AddSubgroup.map (↑e.discriminantGroupEquiv.toAddEquiv) (L.discriminantSubgroup P)

The transport commutes with the discriminant-subgroup correspondence. The subgroup of A_M attached to a transported intermediate carrier is the image, under the induced equivalence of discriminant groups, of the subgroup of A_L attached to the original carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalComplement_discriminantSubgroup_intermediateCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] (e : L.Isometry M) (P : ↑L.IntermediateCarrier) : AddSubgroup.map (↑e.discriminantGroupEquiv.toAddEquiv) (L.discriminantBilinearModule.orthogonalComplement (L.discriminantSubgroup P)) = M.discriminantBilinearModule.orthogonalComplement (M.discriminantSubgroup (e.intermediateCarrierEquiv P))

An isometry carries the orthogonal complements of corresponding discriminant subgroups to one another.

theorem TauCeti.IntegralLattice.Isometry.discriminantGroupEquiv_mem_orthogonalComplement_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] (e : L.Isometry M) (P : ↑L.IntermediateCarrier) (x : L.DiscriminantGroup) : e.discriminantGroupEquiv x ∈ M.discriminantBilinearModule.orthogonalComplement (M.discriminantSubgroup (e.intermediateCarrierEquiv P)) ↔ x ∈ L.discriminantBilinearModule.orthogonalComplement (L.discriminantSubgroup P)

A discriminant class is orthogonal to the subgroup of an intermediate carrier exactly when its image is orthogonal to the subgroup of the transported carrier.

theorem TauCeti.IntegralLattice.Isometry.intermediateCarrierEquiv_intermediateCarrierOfDiscriminantSubgroup {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (H : AddSubgroup L.DiscriminantGroup) : e.intermediateCarrierEquiv (L.intermediateCarrierOfDiscriminantSubgroup H) = M.intermediateCarrierOfDiscriminantSubgroup (AddSubgroup.map (↑e.discriminantGroupEquiv.toAddEquiv) H)

The transport commutes with the inverse-image construction. Transporting the carrier L_H attached to a subgroup H ≤ A_L gives the carrier attached to the image of H in A_M.

Invariance of integrality and evenness

@[simp]

theorem TauCeti.IntegralLattice.Isometry.isIntegral_intermediateCarrierEquiv_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) : IntermediateCarrier.IsIntegral (e.intermediateCarrierEquiv P) ↔ IntermediateCarrier.IsIntegral P

Integrality of an intermediate carrier is an isometry invariant.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.isEven_intermediateCarrierEquiv_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : ↑L.IntermediateCarrier) : IntermediateCarrier.IsEven (e.intermediateCarrierEquiv P) ↔ IntermediateCarrier.IsEven P

Evenness of an intermediate carrier is an isometry invariant.

def TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsIntegral P } ≃o { Q : ↑M.IntermediateCarrier // IntermediateCarrier.IsIntegral Q }

An isometry transports integral intermediate carriers. This is the restriction of intermediateCarrierEquiv to the integral carriers on both sides.

Equations

• e.integralIntermediateCarrierEquiv = TauCeti.IntegralLattice.Isometry.intermediateCarrierEquivSubtype✝ e ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv_apply_coe {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsIntegral P }) : ↑(e.integralIntermediateCarrierEquiv P) = e.intermediateCarrierEquiv ↑P

The integral-carrier transport acts through intermediateCarrierEquiv on underlying intermediate carriers.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv_symm_apply_coe {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (Q : { Q : ↑M.IntermediateCarrier // IntermediateCarrier.IsIntegral Q }) : ↑(e.integralIntermediateCarrierEquiv.symm Q) = e.intermediateCarrierEquiv.symm ↑Q

The inverse integral-carrier transport acts through the inverse intermediate-carrier transport.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).integralIntermediateCarrierEquiv = OrderIso.refl { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsIntegral P }

The identity isometry acts identically on integral intermediate carriers.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.integralIntermediateCarrierEquiv = e.integralIntermediateCarrierEquiv.symm

Integral-carrier transport along an inverse isometry is inverse transport.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.integralIntermediateCarrierEquiv_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).integralIntermediateCarrierEquiv = e.integralIntermediateCarrierEquiv.trans f.integralIntermediateCarrierEquiv

Integral-carrier transport along a composite isometry is composite transport.

def TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven P } ≃o { Q : ↑M.IntermediateCarrier // IntermediateCarrier.IsEven Q }

An isometry transports even intermediate carriers. This is the restriction of intermediateCarrierEquiv to the even carriers on both sides.

Equations

• e.evenIntermediateCarrierEquiv = TauCeti.IntegralLattice.Isometry.intermediateCarrierEquivSubtype✝ e ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv_apply_coe {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (P : { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven P }) : ↑(e.evenIntermediateCarrierEquiv P) = e.intermediateCarrierEquiv ↑P

The even-carrier transport acts through intermediateCarrierEquiv on underlying intermediate carriers.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv_symm_apply_coe {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (Q : { Q : ↑M.IntermediateCarrier // IntermediateCarrier.IsEven Q }) : ↑(e.evenIntermediateCarrierEquiv.symm Q) = e.intermediateCarrierEquiv.symm ↑Q

The inverse even-carrier transport acts through the inverse intermediate-carrier transport.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).evenIntermediateCarrierEquiv = OrderIso.refl { P : ↑L.IntermediateCarrier // IntermediateCarrier.IsEven P }

The identity isometry acts identically on even intermediate carriers.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.evenIntermediateCarrierEquiv = e.evenIntermediateCarrierEquiv.symm

Even-carrier transport along an inverse isometry is inverse transport.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.evenIntermediateCarrierEquiv_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).evenIntermediateCarrierEquiv = e.evenIntermediateCarrierEquiv.trans f.evenIntermediateCarrierEquiv

Even-carrier transport along a composite isometry is composite transport.

Transport of the attached overlattice

def TauCeti.IntegralLattice.Isometry.toIntegralLatticeIsometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] (e : L.Isometry M) {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsIntegral P) : hP.toIntegralLattice.Isometry ⋯.toIntegralLattice

An isometry restricts to an isometry of integral overlattices. The lattice carried by an integral intermediate carrier and the lattice carried by its transport are isometric through the same ambient rational equivalence.

Equations

• e.toIntegralLatticeIsometry hP = { toLinearEquiv := e.toLinearEquiv, map_app' := ⋯, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.toIntegralLatticeIsometry_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] (e : L.Isometry M) {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsIntegral P) (x : V) : (e.toIntegralLatticeIsometry hP) x = e x

The restricted isometry of integral overlattices acts by the ambient equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.toIntegralLatticeIsometry_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} [L.IsNondegenerate] [M.IsNondegenerate] (e : L.Isometry M) {P : ↑L.IntermediateCarrier} (hP : IntermediateCarrier.IsIntegral P) (y : W) : (e.toIntegralLatticeIsometry hP).symm y = e.symm y

The inverse restricted isometry of integral overlattices acts by the inverse ambient equivalence.

Orthogonal direct sums

def TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) : ↑(L.orthogonalSum M).IntermediateCarrier

The intermediate carrier of an orthogonal sum assembled from a pair of intermediate carriers.

Equations

• L.orthogonalSumIntermediateCarrier M P Q = ⟨(↑P).prod ↑Q, ⋯⟩

@[simp]

theorem TauCeti.IntegralLattice.mem_orthogonalSumIntermediateCarrier_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) (p : V × W) : p ∈ ↑(L.orthogonalSumIntermediateCarrier M P Q) ↔ p.1 ∈ ↑P ∧ p.2 ∈ ↑Q

Membership in an assembled intermediate carrier is componentwise membership.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier_bot {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : L.orthogonalSumIntermediateCarrier M ⊥ ⊥ = ⊥

Assembling the two carriers gives the carrier of the orthogonal sum.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier_top {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : L.orthogonalSumIntermediateCarrier M ⊤ ⊤ = ⊤

Assembling the two dual carriers gives the dual carrier of the orthogonal sum.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier_le_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P P' : ↑L.IntermediateCarrier) (Q Q' : ↑M.IntermediateCarrier) : L.orthogonalSumIntermediateCarrier M P Q ≤ L.orthogonalSumIntermediateCarrier M P' Q' ↔ P ≤ P' ∧ Q ≤ Q'

Assembling intermediate carriers is an order embedding. One assembled carrier is contained in another exactly when both components are.

@[simp]

theorem TauCeti.IntegralLattice.mem_discriminantSubgroup_orthogonalSumIntermediateCarrier_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) (z : (L.orthogonalSum M).DiscriminantGroup) : z ∈ (L.orthogonalSum M).discriminantSubgroup (L.orthogonalSumIntermediateCarrier M P Q) ↔ ((L.discriminantGroupOrthogonalSumEquiv M) z).1 ∈ L.discriminantSubgroup P ∧ ((L.discriminantGroupOrthogonalSumEquiv M) z).2 ∈ M.discriminantSubgroup Q

The discriminant subgroup of an assembled carrier is the product subgroup. Under the canonical equivalence A_(L ⊥ M) ≃ A_L × A_M, a class lies in the subgroup of the assembled carrier exactly when each component lies in the subgroup of the corresponding component carrier.

@[simp]

theorem TauCeti.IntegralLattice.map_discriminantSubgroup_orthogonalSumIntermediateCarrier {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) : AddSubgroup.map (↑(L.discriminantGroupOrthogonalSumEquiv M).toAddEquiv) ((L.orthogonalSum M).discriminantSubgroup (L.orthogonalSumIntermediateCarrier M P Q)) = (L.discriminantSubgroup P).prod (M.discriminantSubgroup Q)

The discriminant subgroup of an assembled carrier is the product subgroup, as an equality of subgroups of A_L × A_M.

theorem TauCeti.IntegralLattice.orthogonalSumIntermediateCarrier_intermediateCarrierOfDiscriminantSubgroup {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (H : AddSubgroup L.DiscriminantGroup) (K : AddSubgroup M.DiscriminantGroup) : L.orthogonalSumIntermediateCarrier M (L.intermediateCarrierOfDiscriminantSubgroup H) (M.intermediateCarrierOfDiscriminantSubgroup K) = (L.orthogonalSum M).intermediateCarrierOfDiscriminantSubgroup (AddSubgroup.comap (↑(L.discriminantGroupOrthogonalSumEquiv M).toAddEquiv) (H.prod K))

Assembling commutes with the inverse-image construction. The carrier of L ⊥ M attached to the preimage of a product subgroup H × K ≤ A_L × A_M is assembled from the carriers attached to H and to K.

@[simp]

theorem TauCeti.IntegralLattice.isIntegral_orthogonalSumIntermediateCarrier_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) : IntermediateCarrier.IsIntegral (L.orthogonalSumIntermediateCarrier M P Q) ↔ IntermediateCarrier.IsIntegral P ∧ IntermediateCarrier.IsIntegral Q

Integrality of an assembled carrier is componentwise.

theorem TauCeti.IntegralLattice.IntermediateCarrier.IsIntegral.orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {P : ↑L.IntermediateCarrier} {Q : ↑M.IntermediateCarrier} (hP : IsIntegral P) (hQ : IsIntegral Q) : IsIntegral (L.orthogonalSumIntermediateCarrier M P Q)

The assembled carrier P ⊕ Q of two integral intermediate carriers is integral.

@[simp]

theorem TauCeti.IntegralLattice.isEven_orthogonalSumIntermediateCarrier_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (P : ↑L.IntermediateCarrier) (Q : ↑M.IntermediateCarrier) : IntermediateCarrier.IsEven (L.orthogonalSumIntermediateCarrier M P Q) ↔ IntermediateCarrier.IsEven P ∧ IntermediateCarrier.IsEven Q

Evenness of an assembled carrier is componentwise.