QuadraticModuleCat.Hom.ext

theorem QuadraticModuleCat.Hom.ext : ∀ {R : Type u} {inst : CommRing R} {V W : QuadraticModuleCat R} (x y : V.Hom W), x.toIsometry = y.toIsometry → x = y

This theorem states that for any commutative ring `R` and any two quadratic modules `V` and `W` over `R`, if we have two homomorphisms `x` and `y` from `V` to `W`, and the isometric part of `x` equals to the isometric part of `y`, then `x` is equal to `y`. Essentially, it means that a homomorphism in the category of quadratic modules is uniquely determined by its isometry part.

More concisely: Given any commutative ring `R` and quadratic modules `V` and `W` over `R`, if two homomorphisms `x` and `y` from `V` to `W` have equal isometric parts, then `x = y`.