structure IntegralLatticeEquiv (Λ₁ : Type u_1) (Λ₂ : Type u_2) [IntegralLattice Λ₁] [IntegralLattice Λ₂] extends Λ₁ ≃+ Λ₂ : Type (max u_1 u_2)

A lattice equivalence corresponds to structure preserving isometries fixing the origin, i.e. equivalence preserving vector additions and inner products.

• toFun : Λ₁ → Λ₂
• invFun : Λ₂ → Λ₁
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_add' (x y : Λ₁) : self.toFun (x + y) = self.toFun x + self.toFun y
• preserves_inner' (x y : Λ₁) : inner ℤ (self.toFun x) (self.toFun y) = inner ℤ x y

def «term_≃ₗ_» : Lean.TrailingParserDescr

Notation for an IntegralLatticeEquiv.

Equations

• «term_≃ₗ_» = Lean.ParserDescr.trailingNode `«term_≃ₗ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₗ ") (Lean.ParserDescr.cat `term 26))

def IntegralLatticeEquiv.refl (Λ : Type u_4) [IntegralLattice Λ] : Λ ≃ₗ Λ

Lattice equivalence relation is reflexive.

Equations

• IntegralLatticeEquiv.refl Λ = { toAddEquiv := AddEquiv.refl Λ, preserves_inner' := ⋯ }

def IntegralLatticeEquiv.symm {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] (f : Λ₁ ≃ₗ Λ₂) : Λ₂ ≃ₗ Λ₁

Lattice equivalence relation is symmetric.

Equations

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

def IntegralLatticeEquiv.trans {Λ₁ : Type u_1} {Λ₂ : Type u_2} {Λ₃ : Type u_3} [IntegralLattice Λ₁] [IntegralLattice Λ₂] [IntegralLattice Λ₃] (f : Λ₁ ≃ₗ Λ₂) (g : Λ₂ ≃ₗ Λ₃) : Λ₁ ≃ₗ Λ₃

Lattice equivalence relation is transitive.

Equations

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

instance IntegralLatticeEquiv.instEquivLike {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] : EquivLike (Λ₁ ≃ₗ Λ₂) Λ₁ Λ₂

Equations

• IntegralLatticeEquiv.instEquivLike = { coe := fun (x : Λ₁ ≃ₗ Λ₂) => x.toFun, inv := fun (x : Λ₁ ≃ₗ Λ₂) => x.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance IntegralLatticeEquiv.instAddEquivClass {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] : AddEquivClass (Λ₁ ≃ₗ Λ₂) Λ₁ Λ₂

theorem IntegralLatticeEquiv.preserves_inner {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] (f : Λ₁ ≃ₗ Λ₂) (x y : Λ₁) : inner ℤ (f x) (f y) = inner ℤ x y

theorem IntegralLatticeEquiv.ext {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] {f g : Λ₁ ≃ₗ Λ₂} (h : ∀ (x : Λ₁), f x = g x) : f = g

theorem IntegralLatticeEquiv.ext_iff {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] {f g : Λ₁ ≃ₗ Λ₂} : f = g ↔ ∀ (x : Λ₁), f x = g x

@[simp]

theorem IntegralLatticeEquiv.self_trans_symm {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] (f : Λ₁ ≃ₗ Λ₂) : f.trans f.symm = refl Λ₁