Documentation

Project.IntegralLattice.Equiv

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.

Instances For

    Lattice equivalence relation is reflexive.

    Equations
    Instances For
      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' := }
      Instances For
        def IntegralLatticeEquiv.trans {Λ₁ : Type u_1} {Λ₂ : Type u_2} {Λ₃ : Type u_3} [IntegralLattice Λ₁] [IntegralLattice Λ₂] [IntegralLattice Λ₃] (f : Λ₁ ≃ₗ Λ₂) (g : Λ₂ ≃ₗ Λ₃) :
        Λ₁ ≃ₗ Λ₃

        Lattice equivalence relation is transitive.

        Equations
        Instances For
          instance IntegralLatticeEquiv.instEquivLike {Λ₁ : Type u_1} {Λ₂ : Type u_2} [IntegralLattice Λ₁] [IntegralLattice Λ₂] :
          EquivLike (Λ₁ ≃ₗ Λ₂) Λ₁ Λ₂
          Equations
          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 Λ₁