Finite bilinear modules

A finite abelian group equipped with a symmetric biadditive pairing into ℚ/ℤ. The pairing is stored as its adjoint into Mathlib's CharacterModule; nondegeneracy asserts that this adjoint is bijective.

This file provides the basic constructions needed for discriminant forms: morphisms, isometries, restriction, form negation, orthogonal direct sums, radicals, orthogonal complements, isotropic elements, isotropic subgroups, and Lagrangians. Nondegeneracy remains a predicate because restriction to a subgroup can be degenerate.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.

Main definitions

• TauCeti.FiniteBilinearModule: a finite abelian group with a symmetric ℚ/ℤ-valued pairing.
• TauCeti.FiniteBilinearModule.toBilin: the pairing as a ℤ-bilinear map.
• TauCeti.FiniteBilinearModule.IsNondegenerate: bijectivity of the adjoint pairing.
• TauCeti.FiniteBilinearModule.Hom: a pairing-preserving additive homomorphism.
• TauCeti.FiniteBilinearModule.Isometry: a pairing-preserving additive equivalence.
• TauCeti.FiniteBilinearModule.Isometry.prod: the orthogonal direct sum of two isometries.
• TauCeti.FiniteBilinearModule.orthogonalComplement: the orthogonal complement of a subgroup.
• TauCeti.FiniteBilinearModule.IsIsotropicElem: vanishing of the self-pairing on an element.
• TauCeti.FiniteBilinearModule.IsIsotropic: vanishing of the pairing on a subgroup.
• TauCeti.FiniteBilinearModule.IsLagrangian: equality with the orthogonal complement.

Main results

• TauCeti.FiniteBilinearModule.radical_restrict: the radical of a restricted pairing is the part of the orthogonal complement lying in the subgroup.
• TauCeti.FiniteBilinearModule.Isometry.map_orthogonalComplement: an isometry carries orthogonal complements to orthogonal complements.
• TauCeti.FiniteBilinearModule.Isometry.comap_orthogonalComplement: the inverse image of an orthogonal complement under an isometry is the orthogonal complement of the inverse image.
• TauCeti.FiniteBilinearModule.Isometry.orthogonalComplementEquiv: the induced equivalence between corresponding orthogonal complements.
• TauCeti.FiniteBilinearModule.Hom.isIsotropic_map_iff: the image of a subgroup under a morphism is isotropic exactly when the subgroup is; Isometry.isIsotropic_map_iff is the form for an isometry's additive equivalence.
• TauCeti.FiniteBilinearModule.Isometry.isIsotropic_comap_iff: an isometry transports isotropic subgroups by inverse image.
• TauCeti.FiniteBilinearModule.Isometry.isLagrangian_map_iff: an isometry transports Lagrangian subgroups.
• TauCeti.FiniteBilinearModule.isIsotropic_prod_iff: isotropy of a product subgroup in an orthogonal direct sum is isotropy of each factor subgroup.

structure TauCeti.FiniteBilinearModule : Type (u + 1)

A finite abelian group equipped with a symmetric biadditive pairing into ℚ/ℤ.

The pairing is stored as its adjoint A →+ CharacterModule A, so biadditivity is part of its type.

• carrier : Type u

  The underlying finite abelian group.

• addCommGroup : AddCommGroup self.carrier
• finite : Finite self.carrier
• pairing : self.carrier →+ CharacterModule self.carrier

  The adjoint of the bilinear pairing.

• pairing_comm (x y : self.carrier) : (self.pairing x) y = (self.pairing y) x

  The pairing is symmetric.

@[instance_reducible]

instance TauCeti.FiniteBilinearModule.instCoeSortType : CoeSort FiniteBilinearModule (Type u)

A finite bilinear module coerces to its underlying type.

Equations

• TauCeti.FiniteBilinearModule.instCoeSortType = { coe := TauCeti.FiniteBilinearModule.carrier }

theorem TauCeti.FiniteBilinearModule.pairing_zero_left (A : FiniteBilinearModule) (x : A.carrier) : (A.pairing 0) x = 0

The pairing of 0 with any element is zero.

@[simp]

theorem TauCeti.FiniteBilinearModule.pairing_zero_right (A : FiniteBilinearModule) (x : A.carrier) : (A.pairing x) 0 = 0

The pairing of any element with 0 is zero.

theorem TauCeti.FiniteBilinearModule.pairing_add_left (A : FiniteBilinearModule) (x y z : A.carrier) : (A.pairing (x + y)) z = (A.pairing x) z + (A.pairing y) z

The pairing is additive in its first argument.

@[simp]

theorem TauCeti.FiniteBilinearModule.pairing_add_right (A : FiniteBilinearModule) (x y z : A.carrier) : (A.pairing x) (y + z) = (A.pairing x) y + (A.pairing x) z

The pairing is additive in its second argument.

theorem TauCeti.FiniteBilinearModule.pairing_neg_left (A : FiniteBilinearModule) (x y : A.carrier) : (A.pairing (-x)) y = -(A.pairing x) y

Negating the first argument negates the pairing.

@[simp]

theorem TauCeti.FiniteBilinearModule.pairing_neg_right (A : FiniteBilinearModule) (x y : A.carrier) : (A.pairing x) (-y) = -(A.pairing x) y

Negating the second argument negates the pairing.

theorem TauCeti.FiniteBilinearModule.pairing_nsmul_left (A : FiniteBilinearModule) (n : ℕ) (x y : A.carrier) : (A.pairing (n • x)) y = n • (A.pairing x) y

The pairing is ℕ-linear in its first argument.

def TauCeti.FiniteBilinearModule.toBilin (A : FiniteBilinearModule) : A.carrier →ₗ[ℤ] A.carrier →ₗ[ℤ] AddCircle 1

The bilinear pairing associated to a finite bilinear module, viewed as a ℤ-bilinear map.

Equations

• A.toBilin = LinearMap.mk₂' ℤ ℤ (fun (x y : A.carrier) => (A.pairing x) y) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.FiniteBilinearModule.toBilin_apply (A : FiniteBilinearModule) (x y : A.carrier) : (A.toBilin x) y = (A.pairing x) y

The ℤ-bilinear map toBilin evaluates to the pairing.

theorem TauCeti.FiniteBilinearModule.isRefl_toBilin (A : FiniteBilinearModule) : A.toBilin.IsRefl

The bilinear map toBilin is reflexive: a pairing that vanishes in one order vanishes in the other.

def TauCeti.FiniteBilinearModule.IsNondegenerate (A : FiniteBilinearModule) : Prop

A finite bilinear module is nondegenerate when its adjoint pairing is bijective.

Equations

• A.IsNondegenerate = Function.Bijective ⇑A.pairing

theorem TauCeti.FiniteBilinearModule.isNondegenerate_of_injective (A : FiniteBilinearModule) (hA : Function.Injective ⇑A.pairing) : A.IsNondegenerate

An injective pairing on a finite module is nondegenerate by finite duality.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_iff_injective (A : FiniteBilinearModule) : A.IsNondegenerate ↔ Function.Injective ⇑A.pairing

Nondegeneracy is equivalent to injectivity of the adjoint pairing for a finite module.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.injective (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : Function.Injective ⇑A.pairing

The adjoint pairing of a nondegenerate finite module is injective.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.surjective (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : Function.Surjective ⇑A.pairing

The adjoint pairing of a nondegenerate finite module is surjective.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.bijective (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : Function.Bijective ⇑A.pairing

The adjoint pairing of a nondegenerate finite module is bijective.

noncomputable def TauCeti.FiniteBilinearModule.adjointEquiv (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : A.carrier ≃+ CharacterModule A.carrier

A nondegenerate pairing identifies its group with the full character module.

Equations

• A.adjointEquiv hA = AddEquiv.ofBijective A.pairing ⋯

@[simp]

theorem TauCeti.FiniteBilinearModule.adjointEquiv_apply (A : FiniteBilinearModule) (hA : A.IsNondegenerate) (x : A.carrier) : (A.adjointEquiv hA) x = A.pairing x

The adjoint equivalence sends x to its character A.pairing x.

Morphisms and isometries

structure TauCeti.FiniteBilinearModule.Hom (A : FiniteBilinearModule) (B : FiniteBilinearModule) : Type (max u v)

A morphism of finite bilinear modules is a pairing-preserving additive homomorphism.

• toAddMonoidHom : A.carrier →+ B.carrier

  The underlying additive homomorphism.

• map_pairing' (x y : A.carrier) : (B.pairing (self.toAddMonoidHom x)) (self.toAddMonoidHom y) = (A.pairing x) y

  The homomorphism preserves the bilinear pairing.

@[instance_reducible]

instance TauCeti.FiniteBilinearModule.Hom.instFunLikeCarrier {A : FiniteBilinearModule} {B : FiniteBilinearModule} : FunLike (A.Hom B) A.carrier B.carrier

A morphism of finite bilinear modules coerces to a function between the underlying groups.

Equations

• TauCeti.FiniteBilinearModule.Hom.instFunLikeCarrier = { coe := fun (f : A.Hom B) => ⇑f.toAddMonoidHom, coe_injective := ⋯ }

instance TauCeti.FiniteBilinearModule.Hom.instAddMonoidHomClassCarrier {A : FiniteBilinearModule} {B : FiniteBilinearModule} : AddMonoidHomClass (A.Hom B) A.carrier B.carrier

A morphism of finite bilinear modules is an additive homomorphism.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.coe_toAddMonoidHom {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) : ⇑f.toAddMonoidHom = ⇑f

The underlying additive homomorphism of a morphism has the same underlying function.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.map_pairing {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) (x y : A.carrier) : (B.pairing (f x)) (f y) = (A.pairing x) y

A morphism of finite bilinear modules preserves the stored pairing.

theorem TauCeti.FiniteBilinearModule.Hom.ext {A : FiniteBilinearModule} {B : FiniteBilinearModule} {f g : A.Hom B} (h : ∀ (x : A.carrier), f x = g x) : f = g

Two morphisms are equal when they agree on every element.

theorem TauCeti.FiniteBilinearModule.Hom.ext_iff {A : FiniteBilinearModule} {B : FiniteBilinearModule} {f g : A.Hom B} : f = g ↔ ∀ (x : A.carrier), f x = g x

def TauCeti.FiniteBilinearModule.Hom.id (A : FiniteBilinearModule) : A.Hom A

The identity morphism of a finite bilinear module.

Equations

• TauCeti.FiniteBilinearModule.Hom.id A = { toAddMonoidHom := AddMonoidHom.id A.carrier, map_pairing' := ⋯ }

def TauCeti.FiniteBilinearModule.Hom.comp {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (g : B.Hom C) (f : A.Hom B) : A.Hom C

The composite of two finite bilinear module morphisms.

Equations

• g.comp f = { toAddMonoidHom := g.toAddMonoidHom.comp f.toAddMonoidHom, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.id_apply (A : FiniteBilinearModule) (x : A.carrier) : (id A) x = x

The identity morphism fixes every element.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.comp_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (g : B.Hom C) (f : A.Hom B) (x : A.carrier) : (g.comp f) x = g (f x)

A composite of morphisms applies the two morphisms in turn.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.id_comp {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) : (id B).comp f = f

The identity morphism is a left identity for composition.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.comp_id {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) : f.comp (id A) = f

The identity morphism is a right identity for composition.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.comp_assoc {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} {D : FiniteBilinearModule} (h : C.Hom D) (g : B.Hom C) (f : A.Hom B) : (h.comp g).comp f = h.comp (g.comp f)

Composition of morphisms is associative.

theorem TauCeti.FiniteBilinearModule.Hom.injective {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) (hA : A.IsNondegenerate) : Function.Injective ⇑f

A morphism out of a nondegenerate finite bilinear module is injective.

structure TauCeti.FiniteBilinearModule.Isometry (A : FiniteBilinearModule) (B : FiniteBilinearModule) : Type (max u v)

An isometry of finite bilinear modules is an additive equivalence preserving the pairing.

• toAddEquiv : A.carrier ≃+ B.carrier

  The underlying additive equivalence.

• map_pairing' (x y : A.carrier) : (B.pairing (self.toAddEquiv x)) (self.toAddEquiv y) = (A.pairing x) y

  The equivalence preserves the bilinear pairing.

theorem TauCeti.FiniteBilinearModule.Isometry.toAddEquiv_injective {A : FiniteBilinearModule} {B : FiniteBilinearModule} : Function.Injective toAddEquiv

An isometry is determined by its underlying additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.toAddEquiv_inj {A : FiniteBilinearModule} {B : FiniteBilinearModule} {f g : A.Isometry B} : f.toAddEquiv = g.toAddEquiv ↔ f = g

Two isometries are equal exactly when their underlying additive equivalences are.

@[instance_reducible]

instance TauCeti.FiniteBilinearModule.Isometry.instEquivLikeCarrier {A : FiniteBilinearModule} {B : FiniteBilinearModule} : EquivLike (A.Isometry B) A.carrier B.carrier

An isometry of finite bilinear modules coerces to an equivalence of the underlying groups.

Equations

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

instance TauCeti.FiniteBilinearModule.Isometry.instAddEquivClassCarrier {A : FiniteBilinearModule} {B : FiniteBilinearModule} : AddEquivClass (A.Isometry B) A.carrier B.carrier

An isometry of finite bilinear modules is an additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.coe_toAddEquiv {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : ⇑f.toAddEquiv = ⇑f

The underlying additive equivalence of an isometry has the same underlying function.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.map_pairing {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (x y : A.carrier) : (B.pairing (f x)) (f y) = (A.pairing x) y

An isometry preserves the pairing.

def TauCeti.FiniteBilinearModule.Isometry.toHom {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : A.Hom B

An isometry is, after forgetting bijectivity, a morphism of finite bilinear modules.

Equations

• f.toHom = { toAddMonoidHom := f.toAddEquiv.toAddMonoidHom, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.toHom_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (x : A.carrier) : f.toHom x = f x

The morphism underlying an isometry has the same underlying function.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.toHom_toAddMonoidHom {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : f.toHom.toAddMonoidHom = ↑f.toAddEquiv

The additive homomorphism underlying f.toHom is that of the additive equivalence of f.

theorem TauCeti.FiniteBilinearModule.Isometry.toHom_bijective {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : Function.Bijective ⇑f.toHom

The underlying morphism of an isometry is bijective.

theorem TauCeti.FiniteBilinearModule.Isometry.ext {A : FiniteBilinearModule} {B : FiniteBilinearModule} {f g : A.Isometry B} (h : ∀ (x : A.carrier), f x = g x) : f = g

Two isometries are equal when they agree on all elements.

theorem TauCeti.FiniteBilinearModule.Isometry.ext_iff {A : FiniteBilinearModule} {B : FiniteBilinearModule} {f g : A.Isometry B} : f = g ↔ ∀ (x : A.carrier), f x = g x

def TauCeti.FiniteBilinearModule.Isometry.refl (A : FiniteBilinearModule) : A.Isometry A

The identity isometry.

Equations

• TauCeti.FiniteBilinearModule.Isometry.refl A = { toAddEquiv := AddEquiv.refl A.carrier, map_pairing' := ⋯ }

def TauCeti.FiniteBilinearModule.Isometry.symm {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : B.Isometry A

The inverse of an isometry.

Equations

• f.symm = { toAddEquiv := f.toAddEquiv.symm, map_pairing' := ⋯ }

def TauCeti.FiniteBilinearModule.Isometry.trans {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (f : A.Isometry B) (g : B.Isometry C) : A.Isometry C

The composite of two isometries.

Equations

• f.trans g = { toAddEquiv := f.toAddEquiv.trans g.toAddEquiv, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.refl_toAddEquiv (A : FiniteBilinearModule) : (refl A).toAddEquiv = AddEquiv.refl A.carrier

The identity isometry has the identity additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.symm_toAddEquiv {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : f.symm.toAddEquiv = f.toAddEquiv.symm

The inverse isometry has the inverse additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.trans_toAddEquiv {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (f : A.Isometry B) (g : B.Isometry C) : (f.trans g).toAddEquiv = f.toAddEquiv.trans g.toAddEquiv

The composite isometry has the composite additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.refl_apply (A : FiniteBilinearModule) (x : A.carrier) : (refl A) x = x

The identity isometry fixes every element.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.symm_apply_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (x : A.carrier) : f.symm (f x) = x

The inverse of an isometry undoes it.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.apply_symm_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (x : B.carrier) : f (f.symm x) = x

An isometry undoes its inverse.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.trans_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (f : A.Isometry B) (g : B.Isometry C) (x : A.carrier) : (f.trans g) x = g (f x)

A composite of isometries applies the two isometries in turn.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.refl_toHom (A : FiniteBilinearModule) : (refl A).toHom = Hom.id A

Forgetting the identity isometry gives the identity morphism.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.trans_toHom {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} (f : A.Isometry B) (g : B.Isometry C) : (f.trans g).toHom = g.toHom.comp f.toHom

Forgetting a composite isometry gives the composite morphism.

theorem TauCeti.FiniteBilinearModule.Isometry.isNondegenerate {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) (hA : A.IsNondegenerate) : B.IsNondegenerate

Nondegeneracy transfers along an isometry.

theorem TauCeti.FiniteBilinearModule.Isometry.isNondegenerate_iff {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : A.IsNondegenerate ↔ B.IsNondegenerate

Nondegeneracy is invariant under isometry.

noncomputable def TauCeti.FiniteBilinearModule.Hom.toIsometry {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) (hf : Function.Bijective ⇑f) : A.Isometry B

A bijective morphism of finite bilinear modules is an isometry.

Equations

• f.toIsometry hf = { toAddEquiv := AddEquiv.ofBijective f.toAddMonoidHom hf, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.toIsometry_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) (hf : Function.Bijective ⇑f) (x : A.carrier) : (f.toIsometry hf) x = f x

The isometry packaged from a bijective morphism has the same underlying function.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.toIsometry_toHom {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Hom B) (hf : Function.Bijective ⇑f) : (f.toIsometry hf).toHom = f

Forgetting a bijective morphism after packaging it as an isometry recovers the morphism.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.toHom_toIsometry {A : FiniteBilinearModule} {B : FiniteBilinearModule} (f : A.Isometry B) : f.toHom.toIsometry ⋯ = f

Packaging the underlying morphism of an isometry recovers the isometry.

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.restrict (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : FiniteBilinearModule

Restrict a finite bilinear module to an additive subgroup.

No nondegeneracy conclusion is asserted: a subgroup of a nondegenerate module can have a degenerate restricted pairing.

Equations

• A.restrict H = { carrier := ↥H, addCommGroup := H.toAddCommGroup, finite := ⋯, pairing := (A.pairing.comp H.subtype).compl₂ H.subtype, pairing_comm := ⋯ }

theorem TauCeti.FiniteBilinearModule.restrict_pairing (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) (x y : ↥H) : ((A.restrict H).pairing x) y = (A.pairing ↑x) ↑y

The restricted pairing pairs elements of the subgroup as elements of the whole module.

def TauCeti.FiniteBilinearModule.restrictHom (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : (A.restrict H).Hom A

The inclusion of a restricted finite bilinear module into the original module.

Equations

• A.restrictHom H = { toAddMonoidHom := H.subtype, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.restrictHom_apply (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) (x : ↥H) : (A.restrictHom H) x = ↑x

The inclusion of a restricted module sends an element of the subgroup to itself.

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.neg (A : FiniteBilinearModule) : FiniteBilinearModule

Negate the pairing of a finite bilinear module.

Equations

• A.neg = { carrier := A.carrier, addCommGroup := A.addCommGroup, finite := ⋯, pairing := -A.pairing, pairing_comm := ⋯ }

theorem TauCeti.FiniteBilinearModule.neg_pairing (A : FiniteBilinearModule) (x y : A.carrier) : (A.neg.pairing x) y = -(A.pairing x) y

The negated module pairs elements by the negated pairing.

@[simp]

theorem TauCeti.FiniteBilinearModule.isNondegenerate_neg (A : FiniteBilinearModule) : A.neg.IsNondegenerate ↔ A.IsNondegenerate

Form negation preserves nondegeneracy of a finite bilinear module.

@[reducible, inline]

abbrev TauCeti.FiniteBilinearModule.prod (A : FiniteBilinearModule) (B : FiniteBilinearModule) : FiniteBilinearModule

The orthogonal direct sum of two finite bilinear modules.

Equations

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

theorem TauCeti.FiniteBilinearModule.prod_pairing (A : FiniteBilinearModule) (B : FiniteBilinearModule) (x y : A.carrier × B.carrier) : ((A.prod B).pairing x) y = (A.pairing x.1) y.1 + (B.pairing x.2) y.2

The orthogonal direct sum pairs componentwise and adds the two pairings.

def TauCeti.FiniteBilinearModule.Isometry.prod {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} {D : FiniteBilinearModule} (f : A.Isometry C) (g : B.Isometry D) : (A.prod B).Isometry (C.prod D)

The orthogonal direct sum of two isometries.

Equations

• f.prod g = { toAddEquiv := f.toAddEquiv.prodCongr g.toAddEquiv, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.prod_apply {A : FiniteBilinearModule} {B : FiniteBilinearModule} {C : FiniteBilinearModule} {D : FiniteBilinearModule} (f : A.Isometry C) (g : B.Isometry D) (z : A.carrier × B.carrier) : (f.prod g) z = (f z.1, g z.2)

An orthogonal direct sum of isometries acts componentwise.

def TauCeti.FiniteBilinearModule.radical (A : FiniteBilinearModule) : AddSubgroup A.carrier

The radical is the kernel of the adjoint pairing.

Equations

• A.radical = A.pairing.ker

@[simp]

theorem TauCeti.FiniteBilinearModule.mem_radical_iff (A : FiniteBilinearModule) (x : A.carrier) : x ∈ A.radical ↔ ∀ (y : A.carrier), (A.pairing x) y = 0

An element lies in the radical exactly when it pairs trivially with every element.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_iff_radical_eq_bot (A : FiniteBilinearModule) : A.IsNondegenerate ↔ A.radical = ⊥

A finite bilinear module is nondegenerate if and only if its radical is trivial.

@[simp]

theorem TauCeti.FiniteBilinearModule.radical_prod (A : FiniteBilinearModule) (B : FiniteBilinearModule) : (A.prod B).radical = A.radical.prod B.radical

The radical of an orthogonal direct sum is the product of the radicals.

@[simp]

theorem TauCeti.FiniteBilinearModule.isNondegenerate_prod (A : FiniteBilinearModule) (B : FiniteBilinearModule) : (A.prod B).IsNondegenerate ↔ A.IsNondegenerate ∧ B.IsNondegenerate

An orthogonal direct sum of finite bilinear modules is nondegenerate if and only if both factors are nondegenerate.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.eq_zero_of_forall_pairing_eq_zero (A : FiniteBilinearModule) (hA : A.IsNondegenerate) {x : A.carrier} (hx : ∀ (y : A.carrier), (A.pairing x) y = 0) : x = 0

An element pairing trivially with every element is zero in a nondegenerate module.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.radical_eq_bot (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : A.radical = ⊥

The radical of a nondegenerate finite bilinear module is trivial.

theorem TauCeti.FiniteBilinearModule.isNondegenerate_of_radical_eq_bot (A : FiniteBilinearModule) (h : A.radical = ⊥) : A.IsNondegenerate

A finite bilinear module with trivial radical is nondegenerate.

def TauCeti.FiniteBilinearModule.orthogonalComplement (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : AddSubgroup A.carrier

The orthogonal complement of a subgroup consists of the elements pairing trivially with it.

Equations

• A.orthogonalComplement H = (Submodule.orthogonalBilin A.toBilin (AddSubgroup.toIntSubmodule H)).toAddSubgroup

@[simp]

theorem TauCeti.FiniteBilinearModule.mem_orthogonalComplement_iff (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) (x : A.carrier) : x ∈ A.orthogonalComplement H ↔ ∀ y ∈ H, (A.pairing x) y = 0

An element lies in the orthogonal complement of H exactly when it pairs trivially with every element of H.

@[simp]

theorem TauCeti.FiniteBilinearModule.radical_restrict (A : FiniteBilinearModule) (S : AddSubgroup A.carrier) : (A.restrict S).radical = (A.orthogonalComplement S).addSubgroupOf S

The radical of a restricted pairing. Restricting the pairing of A to a subgroup S makes degenerate exactly the vectors of S which are orthogonal to all of S.

theorem TauCeti.FiniteBilinearModule.orthogonalComplement_anti (A : FiniteBilinearModule) {H K : AddSubgroup A.carrier} (h : H ≤ K) : A.orthogonalComplement K ≤ A.orthogonalComplement H

Orthogonal complements reverse inclusions.

@[simp]

theorem TauCeti.FiniteBilinearModule.orthogonalComplement_bot (A : FiniteBilinearModule) : A.orthogonalComplement ⊥ = ⊤

Every element is orthogonal to the trivial subgroup.

@[simp]

theorem TauCeti.FiniteBilinearModule.orthogonalComplement_top (A : FiniteBilinearModule) : A.orthogonalComplement ⊤ = A.radical

The orthogonal complement of the whole group is the radical.

theorem TauCeti.FiniteBilinearModule.IsNondegenerate.orthogonalComplement_top_eq_bot (A : FiniteBilinearModule) (hA : A.IsNondegenerate) : A.orthogonalComplement ⊤ = ⊥

The orthogonal complement of the whole group is trivial for a nondegenerate pairing.

theorem TauCeti.FiniteBilinearModule.le_orthogonalComplement_orthogonalComplement (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : H ≤ A.orthogonalComplement (A.orthogonalComplement H)

Every subgroup is contained in its double orthogonal complement.

def TauCeti.FiniteBilinearModule.IsIsotropicElem (A : FiniteBilinearModule) (x : A.carrier) : Prop

An element of a finite bilinear module is isotropic when its self-pairing vanishes.

Equations

• A.IsIsotropicElem x = ((A.pairing x) x = 0)

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_def (A : FiniteBilinearModule) (x : A.carrier) : A.IsIsotropicElem x ↔ (A.pairing x) x = 0

An element is isotropic exactly when its self-pairing vanishes.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_zero (A : FiniteBilinearModule) : A.IsIsotropicElem 0

The zero element is isotropic.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_neg (A : FiniteBilinearModule) (x : A.carrier) : A.IsIsotropicElem (-x) ↔ A.IsIsotropicElem x

The negative of an isotropic element is isotropic.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.isIsotropicElem_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Hom B) (x : A.carrier) : B.IsIsotropicElem (f x) ↔ A.IsIsotropicElem x

A morphism of finite bilinear modules preserves and reflects isotropic elements.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.isIsotropicElem_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (x : A.carrier) : B.IsIsotropicElem (f x) ↔ A.IsIsotropicElem x

An isometry preserves and reflects isotropic elements.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_neg_module (A : FiniteBilinearModule) (x : A.carrier) : A.neg.IsIsotropicElem x ↔ A.IsIsotropicElem x

Form negation preserves isotropic elements.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_prod (A : FiniteBilinearModule) (B : FiniteBilinearModule) (x : A.carrier) (y : B.carrier) : (A.prod B).IsIsotropicElem (x, y) ↔ (A.pairing x) x + (B.pairing y) y = 0

An element in an orthogonal product is isotropic if and only if the sum of its component pairings vanishes.

def TauCeti.FiniteBilinearModule.IsIsotropic (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : Prop

A subgroup is bilinearly isotropic when the pairing vanishes on the subgroup square.

Equations

• A.IsIsotropic H = ∀ x ∈ H, ∀ y ∈ H, (A.pairing x) y = 0

theorem TauCeti.FiniteBilinearModule.isIsotropic_def (A : FiniteBilinearModule) {H : AddSubgroup A.carrier} : A.IsIsotropic H ↔ ∀ x ∈ H, ∀ y ∈ H, (A.pairing x) y = 0

Bilinear isotropy of a subgroup, unfolded to its defining property.

theorem TauCeti.FiniteBilinearModule.isIsotropicElem_of_mem_isIsotropic (A : FiniteBilinearModule) {H : AddSubgroup A.carrier} (hH : A.IsIsotropic H) {x : A.carrier} (hx : x ∈ H) : A.IsIsotropicElem x

An element belonging to an isotropic subgroup is isotropic.

theorem TauCeti.FiniteBilinearModule.isIsotropic_zmultiples_iff (A : FiniteBilinearModule) (x : A.carrier) : A.IsIsotropic (AddSubgroup.zmultiples x) ↔ A.IsIsotropicElem x

The cyclic subgroup generated by x is isotropic if and only if x is isotropic.

theorem TauCeti.FiniteBilinearModule.isIsotropic_iff_le_orthogonalComplement (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : A.IsIsotropic H ↔ H ≤ A.orthogonalComplement H

Isotropy is equivalently inclusion in the orthogonal complement.

theorem TauCeti.FiniteBilinearModule.IsIsotropic.mono (A : FiniteBilinearModule) {H K : AddSubgroup A.carrier} (hK : A.IsIsotropic K) (h : H ≤ K) : A.IsIsotropic H

Isotropy passes to additive subgroups.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropic_bot (A : FiniteBilinearModule) : A.IsIsotropic ⊥

The trivial subgroup is isotropic.

@[simp]

theorem TauCeti.FiniteBilinearModule.isIsotropic_prod_iff (A : FiniteBilinearModule) (B : FiniteBilinearModule) (H : AddSubgroup A.carrier) (K : AddSubgroup B.carrier) : (A.prod B).IsIsotropic (H.prod K) ↔ A.IsIsotropic H ∧ B.IsIsotropic K

Isotropy of a product subgroup is componentwise.

def TauCeti.FiniteBilinearModule.IsLagrangian (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : Prop

A Lagrangian is a subgroup equal to its orthogonal complement.

Equations

• A.IsLagrangian H = (H = A.orthogonalComplement H)

theorem TauCeti.FiniteBilinearModule.isLagrangian_def (A : FiniteBilinearModule) (H : AddSubgroup A.carrier) : A.IsLagrangian H ↔ H = A.orthogonalComplement H

A subgroup is Lagrangian exactly when it equals its orthogonal complement.

theorem TauCeti.FiniteBilinearModule.IsLagrangian.isIsotropic (A : FiniteBilinearModule) {H : AddSubgroup A.carrier} (hH : A.IsLagrangian H) : A.IsIsotropic H

Every Lagrangian is isotropic.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.map_orthogonalComplement (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) : AddSubgroup.map (↑f.toAddEquiv) (A.orthogonalComplement H) = B.orthogonalComplement (AddSubgroup.map (↑f.toAddEquiv) H)

An isometry carries orthogonal complements to orthogonal complements.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.comap_orthogonalComplement (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (K : AddSubgroup B.carrier) : A.orthogonalComplement (AddSubgroup.comap (↑f.toAddEquiv) K) = AddSubgroup.comap (↑f.toAddEquiv) (B.orthogonalComplement K)

The inverse image of an orthogonal complement under an isometry is the orthogonal complement of the inverse image.

def TauCeti.FiniteBilinearModule.Isometry.orthogonalComplementEquiv (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) : ↥(A.orthogonalComplement H) ≃+ ↥(B.orthogonalComplement (AddSubgroup.map (↑f.toAddEquiv) H))

An isometry restricts to an additive equivalence from the orthogonal complement of a subgroup onto the orthogonal complement of its image.

Equations

• TauCeti.FiniteBilinearModule.Isometry.orthogonalComplementEquiv A f H = (f.toAddEquiv.addSubgroupMap (A.orthogonalComplement H)).trans (AddEquiv.addSubgroupCongr ⋯)

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.coe_orthogonalComplementEquiv_apply (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) (x : ↥(A.orthogonalComplement H)) : ↑((orthogonalComplementEquiv A f H) x) = f ↑x

The restricted equivalence of orthogonal complements acts by the isometry.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.coe_orthogonalComplementEquiv_symm_apply (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) (y : ↥(B.orthogonalComplement (AddSubgroup.map (↑f.toAddEquiv) H))) : ↑((orthogonalComplementEquiv A f H).symm y) = f.symm ↑y

The inverse restricted equivalence of orthogonal complements acts by the inverse isometry.

theorem TauCeti.FiniteBilinearModule.Isometry.map_mem_orthogonalComplement_of_forall_mem (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) {H : AddSubgroup A.carrier} {K : AddSubgroup B.carrier} (h : ∀ (x : A.carrier), f x ∈ K → x ∈ H) {x : A.carrier} (hx : x ∈ A.orthogonalComplement H) : f x ∈ B.orthogonalComplement K

An isometry carries an element of the orthogonal complement of H into the orthogonal complement of K whenever the preimage of K is contained in H.

theorem TauCeti.FiniteBilinearModule.Isometry.map_mem_orthogonalComplement_of_map_eq (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) {H : AddSubgroup A.carrier} {K : AddSubgroup B.carrier} (h : AddSubgroup.map (↑f.toAddEquiv) H = K) {x : A.carrier} (hx : x ∈ A.orthogonalComplement H) : f x ∈ B.orthogonalComplement K

An isometry carrying H onto K carries every element of H^⊥ into K^⊥.

@[simp]

theorem TauCeti.FiniteBilinearModule.Hom.isIsotropic_map_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Hom B) (H : AddSubgroup A.carrier) : B.IsIsotropic (AddSubgroup.map f.toAddMonoidHom H) ↔ A.IsIsotropic H

The image of a subgroup under a morphism of finite bilinear modules is isotropic exactly when the subgroup is.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.isIsotropic_map_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) : B.IsIsotropic (AddSubgroup.map (↑f.toAddEquiv) H) ↔ A.IsIsotropic H

An isometry transports isotropic subgroups, stated for the image under its additive equivalence.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.isIsotropic_comap_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (K : AddSubgroup B.carrier) : A.IsIsotropic (AddSubgroup.comap (↑f.toAddEquiv) K) ↔ B.IsIsotropic K

An isometry transports isotropic subgroups by inverse image.

@[simp]

theorem TauCeti.FiniteBilinearModule.Isometry.isLagrangian_map_iff (A : FiniteBilinearModule) {B : FiniteBilinearModule} (f : A.Isometry B) (H : AddSubgroup A.carrier) : B.IsLagrangian (AddSubgroup.map (↑f.toAddEquiv) H) ↔ A.IsLagrangian H

An isometry transports Lagrangian subgroups.