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
Instances For
Notation for an IntegralLatticeEquiv
.
Equations
- «term_≃ₗ_» = Lean.ParserDescr.trailingNode `«term_≃ₗ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₗ ") (Lean.ParserDescr.cat `term 26))
Instances For
Lattice equivalence relation is reflexive.
Equations
- IntegralLatticeEquiv.refl Λ = { toAddEquiv := AddEquiv.refl Λ, preserves_inner' := ⋯ }
Instances For
def
IntegralLatticeEquiv.symm
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
(f : Λ₁ ≃ₗ Λ₂)
:
Lattice equivalence relation is symmetric.
Instances For
def
IntegralLatticeEquiv.trans
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
{Λ₃ : Type u_3}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
[IntegralLattice Λ₃]
(f : Λ₁ ≃ₗ Λ₂)
(g : Λ₂ ≃ₗ Λ₃)
:
Lattice equivalence relation is transitive.
Instances For
instance
IntegralLatticeEquiv.instEquivLike
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
:
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 : Λ₁)
:
theorem
IntegralLatticeEquiv.ext
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
{f g : Λ₁ ≃ₗ Λ₂}
(h : ∀ (x : Λ₁), f x = g x)
:
theorem
IntegralLatticeEquiv.ext_iff
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
{f g : Λ₁ ≃ₗ Λ₂}
:
@[simp]
theorem
IntegralLatticeEquiv.self_trans_symm
{Λ₁ : Type u_1}
{Λ₂ : Type u_2}
[IntegralLattice Λ₁]
[IntegralLattice Λ₂]
(f : Λ₁ ≃ₗ Λ₂)
: